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>

src/topology/algebra/uniform_group.lean

@@ -205,6 +205,13 @@ end
   𝓤 α = comap (λx:α×α, x.1 / x.2) (𝓝 (1:α)) :=
 by { rw [← comap_swap_uniformity, uniformity_eq_comap_nhds_one, comap_comap, (∘)], refl }
 
+variables {α}
+
+@[to_additive] theorem uniform_group.uniformity_countably_generated
+  [(𝓝 (1 : α)).is_countably_generated] :
+  (𝓤 α).is_countably_generated :=
+by { rw uniformity_eq_comap_nhds_one, exact filter.comap.is_countably_generated _ _ }
+
 open mul_opposite
 
 @[to_additive]

src/topology/metric_space/closeds.lean

@@ -377,7 +377,7 @@ begin
       -- we have proved that `d` is a good approximation of `t` as requested
       exact ⟨d, ‹d ∈ v›, Dtc⟩ },
   end,
-  apply uniform_space.second_countable_of_separable,
+  exact uniform_space.second_countable_of_separable (nonempty_compacts α),
 end
 
 end --section

src/topology/metric_space/metrizable.lean

@@ -5,6 +5,7 @@ Authors: Yury Kudryashov
 -/
 import topology.urysohns_lemma
 import topology.continuous_function.bounded
+import topology.uniform_space.cauchy
 
 /-!
 # Metrizability of a T₃ topological space with second countable topology
@@ -62,6 +63,16 @@ begin
   exact ⟨⟨hf.comap_pseudo_metric_space, rfl⟩⟩
 end
 
+/-- Every pseudo-metrizable space is first countable. -/
+@[priority 100]
+instance pseudo_metrizable_space.first_countable_topology [h : pseudo_metrizable_space X] :
+  topological_space.first_countable_topology X :=
+begin
+  unfreezingI { rcases h with ⟨_, hm⟩, rw ←hm },
+  exact @uniform_space.first_countable_topology X pseudo_metric_space.to_uniform_space
+    emetric.uniformity.filter.is_countably_generated,
+end
+
 instance pseudo_metrizable_space.subtype [pseudo_metrizable_space X]
   (s : set X) : pseudo_metrizable_space s :=
 inducing_coe.pseudo_metrizable_space