mathlib

dcd452de - feat(analysis/locally_convex/with_seminorms): characterization of the topology induced by seminorms in terms of `𝓝 0` (#13547)

feat(analysis/locally_convex/with_seminorms): characterization of the topology induced by seminorms in terms of `𝓝 0` (#13547) This shows that a topology is induced by the family of seminorms `p` iff `𝓝 0 = ⨅ i, (𝓝 0).comap (p i)`, which allows to use the extensive filter and topology library (see e.g. #13549).