mathlib3

c705d414 - feat(analysis/locally_convex): characterize the natural bornology in terms of seminorms (#12721)

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.