feat(topology/metric_space): metrizable spaces (#8759)

Define (pseudo)-metric space constructors for metrizable topological spaces.

Author: PatrickMassot

src/topology/metric_space/basic.lean

@@ -54,14 +54,15 @@ open_locale uniformity topological_space big_operators filter nnreal ennreal
 universes u v w
 variables {α : Type u} {β : Type v}
 
-/-- Construct a uniform structure from a distance function and metric space axioms -/
-def uniform_space_of_dist
-  (dist : α → α → ℝ)
+/-- Construct a uniform structure core from a distance function and metric space axioms.
+This is a technical construction that can be immediately used to construct a uniform structure
+from a distance function and metric space axioms but is also useful when discussing
+metrizable topologies, see `pseudo_metric_space.of_metrizable`. -/
+def uniform_space.core_of_dist {α : Type*} (dist : α → α → ℝ)
   (dist_self : ∀ x : α, dist x x = 0)
   (dist_comm : ∀ x y : α, dist x y = dist y x)
-  (dist_triangle : ∀ x y z : α, dist x z ≤ dist x y + dist y z) : uniform_space α :=
-uniform_space.of_core {
-  uniformity := (⨅ ε>0, 𝓟 {p:α×α | dist p.1 p.2 < ε}),
+  (dist_triangle : ∀ x y z : α, dist x z ≤ dist x y + dist y z) : uniform_space.core α :=
+{ uniformity := (⨅ ε>0, 𝓟 {p:α×α | dist p.1 p.2 < ε}),
   refl       := le_infi $ assume ε, le_infi $
     by simp [set.subset_def, id_rel, dist_self, (>)] {contextual := tt},
   comp       := le_infi $ assume ε, le_infi $ assume h, lift'_le
@@ -75,6 +76,14 @@ uniform_space.of_core {
   symm       := tendsto_infi.2 $ assume ε, tendsto_infi.2 $ assume h,
     tendsto_infi' ε $ tendsto_infi' h $ tendsto_principal_principal.2 $ by simp [dist_comm] }
 
+/-- Construct a uniform structure from a distance function and metric space axioms -/
+def uniform_space_of_dist
+  (dist : α → α → ℝ)
+  (dist_self : ∀ x : α, dist x x = 0)
+  (dist_comm : ∀ x y : α, dist x y = dist y x)
+  (dist_triangle : ∀ x y z : α, dist x z ≤ dist x y + dist y z) : uniform_space α :=
+uniform_space.of_core (uniform_space.core_of_dist dist dist_self dist_comm dist_triangle)
+
 /-- The distance function (given an ambient metric space on `α`), which returns
   a nonnegative real number `dist x y` given `x y : α`. -/
 class has_dist (α : Type*) := (dist : α → α → ℝ)
@@ -110,6 +119,43 @@ pseudo_metric_space.to_uniform_space
 @[priority 200] -- see Note [lower instance priority]
 instance pseudo_metric_space.to_has_edist : has_edist α := ⟨pseudo_metric_space.edist⟩
 
+/-- Construct a pseudo-metric space structure whose underlying topological space structure
+(definitionally) agrees which a pre-existing topology which is compatible with a given distance
+function. -/
+def pseudo_metric_space.of_metrizable {α : Type*} [topological_space α] (dist : α → α → ℝ)
+  (dist_self : ∀ x : α, dist x x = 0)
+  (dist_comm : ∀ x y : α, dist x y = dist y x)
+  (dist_triangle : ∀ x y z : α, dist x z ≤ dist x y + dist y z)
+  (H : ∀ s : set α, is_open s ↔ ∀ x ∈ s, ∃ ε > 0, ∀ y, dist x y < ε → y ∈ s) :
+pseudo_metric_space α :=
+{ dist := dist,
+  dist_self := dist_self,
+  dist_comm := dist_comm,
+  dist_triangle := dist_triangle,
+  to_uniform_space := { is_open_uniformity := begin
+    dsimp only [uniform_space.core_of_dist],
+    intros s,
+    change is_open s ↔ _,
+    rw H s,
+    apply forall_congr, intro x,
+    apply forall_congr, intro x_in,
+    erw (has_basis_binfi_principal _ nonempty_Ioi).mem_iff,
+    { apply exists_congr, intros ε,
+      apply exists_congr, intros ε_pos,
+      simp only [prod.forall, set_of_subset_set_of],
+      split,
+      { rintros h _ y H rfl,
+        exact h y H },
+      { intros h y hxy,
+        exact h _ _ hxy rfl } },
+      { exact λ r (hr : 0 < r) p (hp : 0 < p), ⟨min r p, lt_min hr hp,
+        λ x (hx : dist _ _ < _), lt_of_lt_of_le hx (min_le_left r p),
+        λ x (hx : dist _ _ < _), lt_of_lt_of_le hx (min_le_right r p)⟩ },
+      { apply_instance }
+    end,
+    ..uniform_space.core_of_dist dist dist_self dist_comm dist_triangle },
+  uniformity_dist := rfl }
+
 @[simp] theorem dist_self (x : α) : dist x x = 0 := pseudo_metric_space.dist_self x
 
 theorem dist_comm (x y : α) : dist x y = dist y x := pseudo_metric_space.dist_comm x y
@@ -704,8 +750,8 @@ theorem tendsto_at_top' [nonempty β] [semilattice_sup β] [no_top_order β] {u
 (at_top_basis_Ioi.tendsto_iff nhds_basis_ball).trans $
   by { simp only [exists_prop, true_and], refl }
 
-lemma is_open_singleton_iff {X : Type*} [pseudo_metric_space X] {x : X} :
-  is_open ({x} : set X) ↔ ∃ ε > 0, ∀ y, dist y x < ε → y = x :=
+lemma is_open_singleton_iff {α : Type*} [pseudo_metric_space α] {x : α} :
+  is_open ({x} : set α) ↔ ∃ ε > 0, ∀ y, dist y x < ε → y = x :=
 by simp [is_open_iff, subset_singleton_iff, mem_ball]
 
 /-- Given a point `x` in a discrete subset `s` of a pseudometric space, there is an open ball
@@ -1793,6 +1839,18 @@ end int
 class metric_space (α : Type u) extends pseudo_metric_space α : Type u :=
 (eq_of_dist_eq_zero : ∀ {x y : α}, dist x y = 0 → x = y)
 
+/-- Construct a metric space structure whose underlying topological space structure
+(definitionally) agrees which a pre-existing topology which is compatible with a given distance
+function. -/
+def metric_space.of_metrizable {α : Type*} [topological_space α] (dist : α → α → ℝ)
+  (dist_self : ∀ x : α, dist x x = 0)
+  (dist_comm : ∀ x y : α, dist x y = dist y x)
+  (dist_triangle : ∀ x y z : α, dist x z ≤ dist x y + dist y z)
+  (H : ∀ s : set α, is_open s ↔ ∀ x ∈ s, ∃ ε > 0, ∀ y, dist x y < ε → y ∈ s)
+  (eq_of_dist_eq_zero : ∀ x y : α, dist x y = 0 → x = y) : metric_space α :=
+{ eq_of_dist_eq_zero := eq_of_dist_eq_zero,
+  ..pseudo_metric_space.of_metrizable dist dist_self dist_comm dist_triangle H }
+
 variables {γ : Type w} [metric_space γ]
 
 theorem eq_of_dist_eq_zero {x y : γ} : dist x y = 0 → x = y :=