mathlib3

d1a6dd23 - feat(topology/algebra/module/locally_convex): local convexity is preserved by `Inf` and `induced` (#12118)

feat(topology/algebra/module/locally_convex): local convexity is preserved by `Inf` and `induced` (#12118) I also generalized slightly `locally_convex_space.of_bases` and changed a `Sort*` to `Type*` in `filter.has_basis_infi` to correctly reflect the universe constraints.