Commit 2022-06-11 11:06 d1a6dd23
View on Github →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.