feat(topology/metric_space): define a pseudo metrizable space (#14053)

* define `topological_space.pseudo_metrizable_space`;
* copy API from `topological_space.metrizable_space`;
* add `pi` instances;
* use `X`, `Y` instead of `α`, `β`.

src/topology/metric_space/basic.lean

@@ -1044,6 +1044,20 @@ lemma pseudo_metric_space.replace_uniformity_eq {α} [U : uniform_space α]
   m.replace_uniformity H = m :=
 by { ext, refl }
 
+/-- Build a new pseudo metric space from an old one where the bundled topological structure is
+provably (but typically non-definitionaly) equal to some given topological structure.
+See Note [forgetful inheritance].
+-/
+@[reducible] def pseudo_metric_space.replace_topology {γ} [U : topological_space γ]
+  (m : pseudo_metric_space γ) (H : U = m.to_uniform_space.to_topological_space) :
+  pseudo_metric_space γ :=
+@pseudo_metric_space.replace_uniformity γ (m.to_uniform_space.replace_topology H) m rfl
+
+lemma pseudo_metric_space.replace_topology_eq {γ} [U : topological_space γ]
+  (m : pseudo_metric_space γ) (H : U = m.to_uniform_space.to_topological_space) :
+  m.replace_topology H = m :=
+by { ext, refl }
+
 /-- One gets a pseudometric space from an emetric space if the edistance
 is everywhere finite, by pushing the edistance to reals. We set it up so that the edist and the
 uniformity are defeq in the pseudometric space and the pseudoemetric space. In this definition, the
@@ -1330,6 +1344,13 @@ def pseudo_metric_space.induced {α β} (f : α → β)
       exact ⟨_, dist_mem_uniformity ε0, λ ⟨a, b⟩, hε⟩ }
   end }
 
+/-- Pull back a pseudometric space structure by an inducing map. This is a version of
+`pseudo_metric_space.induced` useful in case if the domain already has a `topological_space`
+structure. -/
+def inducing.comap_pseudo_metric_space {α β} [topological_space α] [pseudo_metric_space β]
+  {f : α → β} (hf : inducing f) : pseudo_metric_space α :=
+(pseudo_metric_space.induced f ‹_›).replace_topology hf.induced
+
 /-- Pull back a pseudometric space structure by a uniform inducing map. This is a version of
 `pseudo_metric_space.induced` useful in case if the domain already has a `uniform_space`
 structure. -/
@@ -2500,12 +2521,7 @@ See Note [forgetful inheritance].
 @[reducible] def metric_space.replace_topology {γ} [U : topological_space γ] (m : metric_space γ)
   (H : U = m.to_pseudo_metric_space.to_uniform_space.to_topological_space) :
   metric_space γ :=
-begin
-  let t := m.to_pseudo_metric_space.to_uniform_space.replace_topology H,
-  letI : uniform_space γ := t,
-  have : @uniformity _ t = @uniformity _ m.to_pseudo_metric_space.to_uniform_space := rfl,
-  exact m.replace_uniformity this
-end
+@metric_space.replace_uniformity γ (m.to_uniform_space.replace_topology H) m rfl
 
 lemma metric_space.replace_topology_eq {γ} [U : topological_space γ] (m : metric_space γ)
   (H : U = m.to_pseudo_metric_space.to_uniform_space.to_topological_space) :

src/topology/metric_space/metrizable.lean

@@ -23,52 +23,103 @@ open_locale bounded_continuous_function filter topological_space
 
 namespace topological_space
 
+variables {ι X Y : Type*} {π : ι → Type*} [topological_space X] [topological_space Y]
+  [fintype ι] [Π i, topological_space (π i)]
+
+/-- A topological space is *pseudo metrizable* if there exists a pseudo metric space structure
+compatible with the topology. To endow such a space with a compatible distance, use
+`letI : pseudo_metric_space X := topological_space.pseudo_metrizable_space_pseudo_metric X`. -/
+class pseudo_metrizable_space (X : Type*) [t : topological_space X] : Prop :=
+(exists_pseudo_metric : ∃ (m : pseudo_metric_space X), m.to_uniform_space.to_topological_space = t)
+
+@[priority 100]
+instance _root_.pseudo_metric_space.to_pseudo_metrizable_space {X : Type*}
+  [m : pseudo_metric_space X] :
+  pseudo_metrizable_space X :=
+⟨⟨m, rfl⟩⟩
+
+/-- Construct on a metrizable space a metric compatible with the topology. -/
+noncomputable def pseudo_metrizable_space_pseudo_metric
+  (X : Type*) [topological_space X] [h : pseudo_metrizable_space X] :
+  pseudo_metric_space X :=
+h.exists_pseudo_metric.some.replace_topology h.exists_pseudo_metric.some_spec.symm
+
+instance pseudo_metrizable_space_prod [pseudo_metrizable_space X] [pseudo_metrizable_space Y] :
+  pseudo_metrizable_space (X × Y) :=
+begin
+  letI : pseudo_metric_space X := pseudo_metrizable_space_pseudo_metric X,
+  letI : pseudo_metric_space Y := pseudo_metrizable_space_pseudo_metric Y,
+  apply_instance
+end
+
+/-- Given an inducing map of a topological space into a pseudo metrizable space, the source space
+is also pseudo metrizable. -/
+lemma _root_.inducing.pseudo_metrizable_space [pseudo_metrizable_space Y] {f : X → Y}
+  (hf : inducing f) :
+  pseudo_metrizable_space X :=
+begin
+  letI : pseudo_metric_space Y := pseudo_metrizable_space_pseudo_metric Y,
+  exact ⟨⟨hf.comap_pseudo_metric_space, rfl⟩⟩
+end
+
+instance pseudo_metrizable_space.subtype [pseudo_metrizable_space X]
+  (s : set X) : pseudo_metrizable_space s :=
+inducing_coe.pseudo_metrizable_space
+
+instance pseudo_metrizable_space_pi [Π i, pseudo_metrizable_space (π i)] :
+  pseudo_metrizable_space (Π i, π i) :=
+by { letI := λ i, pseudo_metrizable_space_pseudo_metric (π i), apply_instance }
+
 /-- A topological space is metrizable if there exists a metric space structure compatible with the
 topology. To endow such a space with a compatible distance, use
-`letI : metric_space α := metrizable_space_metric α` -/
-class metrizable_space (α : Type*) [t : topological_space α] : Prop :=
-(exists_metric : ∃ (m : metric_space α), m.to_uniform_space.to_topological_space = t)
+`letI : metric_space X := topological_space.metrizable_space_metric X` -/
+class metrizable_space (X : Type*) [t : topological_space X] : Prop :=
+(exists_metric : ∃ (m : metric_space X), m.to_uniform_space.to_topological_space = t)
 
 @[priority 100]
-instance _root_.metric_space.to_metrizable_space {α : Type*} [m : metric_space α] :
-  metrizable_space α :=
+instance _root_.metric_space.to_metrizable_space {X : Type*} [m : metric_space X] :
+  metrizable_space X :=
 ⟨⟨m, rfl⟩⟩
 
+@[priority 100]
+instance metrizable_space.to_pseudo_metrizable_space [h : metrizable_space X] :
+  pseudo_metrizable_space X :=
+⟨let ⟨m, hm⟩ := h.1 in ⟨m.to_pseudo_metric_space, hm⟩⟩
+
 /-- Construct on a metrizable space a metric compatible with the topology. -/
-noncomputable def metrizable_space_metric
-  (α : Type*) [topological_space α] [h : metrizable_space α] :
-  metric_space α :=
+noncomputable def metrizable_space_metric (X : Type*) [topological_space X]
+  [h : metrizable_space X] :
+  metric_space X :=
 h.exists_metric.some.replace_topology h.exists_metric.some_spec.symm
 
 @[priority 100]
-instance t2_space_of_metrizable_space
-  (α : Type*) [topological_space α] [metrizable_space α] : t2_space α :=
-by { letI : metric_space α := metrizable_space_metric α, apply_instance }
+instance t2_space_of_metrizable_space [metrizable_space X] : t2_space X :=
+by { letI : metric_space X := metrizable_space_metric X, apply_instance }
 
-instance metrizable_space_prod (α : Type*) [topological_space α] [metrizable_space α]
-  (β : Type*) [topological_space β] [metrizable_space β] :
-  metrizable_space (α × β) :=
+instance metrizable_space_prod [metrizable_space X] [metrizable_space Y] :
+  metrizable_space (X × Y) :=
 begin
-  letI : metric_space α := metrizable_space_metric α,
-  letI : metric_space β := metrizable_space_metric β,
+  letI : metric_space X := metrizable_space_metric X,
+  letI : metric_space Y := metrizable_space_metric Y,
   apply_instance
 end
 
-instance metrizable_space.subtype {α : Type*} [topological_space α] [metrizable_space α]
-  (s : set α) : metrizable_space s :=
-by { letI := metrizable_space_metric α, apply_instance }
-
 /-- Given an embedding of a topological space into a metrizable space, the source space is also
 metrizable. -/
-lemma _root_.embedding.metrizable_space {α β : Type*} [topological_space α] [topological_space β]
-  [metrizable_space β] {f : α → β} (hf : embedding f) :
-  metrizable_space α :=
+lemma _root_.embedding.metrizable_space [metrizable_space Y] {f : X → Y} (hf : embedding f) :
+  metrizable_space X :=
 begin
-  letI : metric_space β := metrizable_space_metric β,
+  letI : metric_space Y := metrizable_space_metric Y,
   exact ⟨⟨hf.comap_metric_space f, rfl⟩⟩
 end
 
-variables (X : Type*) [topological_space X] [normal_space X] [second_countable_topology X]
+instance metrizable_space.subtype [metrizable_space X] (s : set X) : metrizable_space s :=
+embedding_subtype_coe.metrizable_space
+
+instance metrizable_space_pi [Π i, metrizable_space (π i)] : metrizable_space (Π i, π i) :=
+by { letI := λ i, metrizable_space_metric (π i), apply_instance }
+
+variables (X) [normal_space X] [second_countable_topology X]
 
 /-- A normal topological space with second countable topology can be embedded into `l^∞ = ℕ →ᵇ ℝ`.
 -/