Commit 2022-03-24 05:18 c705d414

feat(analysis/locally_convex): characterize the natural bornology in terms of seminorms (#12721) Add four lemmas:

• is_vonN_bounded_basis_iff: it suffices to check boundedness for a basis
• seminorm_family.has_basis: the basis sets form a basis of the topology
• is_bounded_iff_finset_seminorm_bounded: a set is von Neumann bounded iff it is bounded for all finite suprema of seminorms
• is_bounded_iff_seminorm_bounded: a set is von Neumann bounded iff it is bounded for each seminorm Also make the set argument in seminorm_family.basis_sets_iff implicit.