mathlib

cf9eb049 - feat(topology/metric_space): Add first countability instances (#15942)

feat(topology/metric_space): Add first countability instances (#15942) This PR proves the following two facts: - pseudo-metric/metrizable spaces are first countable - uniform groups that have a countably generated neighborhood at the origin have a countably generated uniformity The instance for uniform groups allows for an easy way to prove that a topological group is metrizable, since the neighborhood filter is a more common object than the uniformity. In total this PR gives the proof that a topological group is metrizable iff it the neighborhood filter at the origin is countably generated. Co-authored-by: Moritz Doll <doll@uni-bremen.de>