mathlib
e71a12cd - feat(analysis/seminorm): closed balls for a seminorm (#16676)

Commit
3 years ago
feat(analysis/seminorm): closed balls for a seminorm (#16676) This introduces the closed ball version of `seminorm.ball` and duplicates a bunch of API. My motivation is the general Banach-Steinhaus theorem in barreled space (one characterization of barrels is that they are exactly closed unit balls of lower semicontinuous seminorms), and I didn't see any reason not do go full duplication here. Co-authored-by: Patrick Massot <patrickmassot@free.fr>
Author
Parents
Loading