mathlib3

73d05c46 - feat(analysis/locally_convex): first countable topologies from countable families of seminorms (#16595)

feat(analysis/locally_convex): first countable topologies from countable families of seminorms (#16595) This PR proves that if the topology is induced by a countable family of seminorms, then it is first countable.