refactor(topology/metric_space/basic): add pseudo_metric (#6716)

This is the natural continuation of #6694: we introduce here `pseudo_metric_space`.

Note that I didn't do anything fancy, I only generalize the results that work out of the box for pseudometric spaces (quite a lot indeed).

It's possible that there is some duplicate code, especially in the section about products.

Author: riccardobrasca

src/geometry/euclidean/basic.lean

@@ -726,7 +726,7 @@ lemma dist_square_eq_dist_orthogonal_projection_square_add_dist_orthogonal_proje
     dist p1 (orthogonal_projection s p2) * dist p1 (orthogonal_projection s p2) +
     dist p2 (orthogonal_projection s p2) * dist p2 (orthogonal_projection s p2) :=
 begin
-  rw [metric_space.dist_comm p2 _, dist_eq_norm_vsub V p1 _, dist_eq_norm_vsub V p1 _,
+  rw [pseudo_metric_space.dist_comm p2 _, dist_eq_norm_vsub V p1 _, dist_eq_norm_vsub V p1 _,
     dist_eq_norm_vsub V _ p2, ← vsub_add_vsub_cancel p1 (orthogonal_projection s p2) p2,
     norm_add_square_eq_norm_square_add_norm_square_iff_real_inner_eq_zero],
   exact submodule.inner_right_of_mem_orthogonal

src/geometry/euclidean/triangle.lean

@@ -295,7 +295,7 @@ include V
 lemma dist_square_eq_dist_square_add_dist_square_iff_angle_eq_pi_div_two (p1 p2 p3 : P) :
   dist p1 p3 * dist p1 p3 = dist p1 p2 * dist p1 p2 + dist p3 p2 * dist p3 p2 ↔
     ∠ p1 p2 p3 = π / 2 :=
-by erw [metric_space.dist_comm p3 p2, dist_eq_norm_vsub V p1 p3, dist_eq_norm_vsub V p1 p2,
+by erw [pseudo_metric_space.dist_comm p3 p2, dist_eq_norm_vsub V p1 p3, dist_eq_norm_vsub V p1 p2,
         dist_eq_norm_vsub V p2 p3,
         ←norm_sub_square_eq_norm_square_add_norm_square_iff_angle_eq_pi_div_two,
         vsub_sub_vsub_cancel_right p1, ←neg_vsub_eq_vsub_rev p2 p3, norm_neg]

src/topology/metric_space/basic.lean

@@ -106,7 +106,7 @@ namespace, while notions associated to metric spaces are mostly in the root name
 variables [pseudo_emetric_space α]
 
 @[priority 100] -- see Note [lower instance priority]
-instance pseudoe_emetric_space.to_uniform_space' : uniform_space α :=
+instance pseudo_emetric_space.to_uniform_space' : uniform_space α :=
 pseudo_emetric_space.to_uniform_space
 
 export pseudo_emetric_space (edist_self edist_comm edist_triangle)
@@ -362,7 +362,7 @@ This is useful if one wants to construct a pseudoemetric space with a
 specified uniformity. See Note [forgetful inheritance] explaining why having definitionally
 the right uniformity is often important.
 -/
-def pseudoemetric_space.replace_uniformity {α} [U : uniform_space α] (m : pseudo_emetric_space α)
+def pseudo_emetric_space.replace_uniformity {α} [U : uniform_space α] (m : pseudo_emetric_space α)
   (H : @uniformity _ U = @uniformity _ pseudo_emetric_space.to_uniform_space) :
   pseudo_emetric_space α :=
 { edist               := @edist _ m.to_has_edist,
@@ -372,8 +372,7 @@ def pseudoemetric_space.replace_uniformity {α} [U : uniform_space α] (m : pseu
   to_uniform_space    := U,
   uniformity_edist    := H.trans (@pseudo_emetric_space.uniformity_edist α _) }
 
-/-- The extended pseudometric induced by an injective function taking values in a
-pseudoemetric space. -/
+/-- The extended pseudometric induced by a function taking values in a pseudoemetric space. -/
 def pseudo_emetric_space.induced {α β} (f : α → β)
   (m : pseudo_emetric_space β) : pseudo_emetric_space α :=
 { edist               := λ x y, edist (f x) (f y),
@@ -403,7 +402,7 @@ theorem subtype.edist_eq {p : α → Prop} (x y : subtype p) : edist x y = edist
 /-- The product of two pseudoemetric spaces, with the max distance, is an extended
 pseudometric spaces. We make sure that the uniform structure thus constructed is the one
 corresponding to the product of uniform spaces, to avoid diamond problems. -/
-instance prod.pseudoemetric_space_max [pseudo_emetric_space β] : pseudo_emetric_space (α × β) :=
+instance prod.pseudo_emetric_space_max [pseudo_emetric_space β] : pseudo_emetric_space (α × β) :=
 { edist := λ x y, max (edist x.1 y.1) (edist x.2 y.2),
   edist_self := λ x, by simp,
   edist_comm := λ x y, by simp [edist_comm],
@@ -432,7 +431,8 @@ a pseudoemetric space.
 This construction would also work for infinite products, but it would not give rise
 to the product topology. Hence, we only formalize it in the good situation of finitely many
 spaces. -/
-instance pseudoemetric_space_pi [∀b, pseudo_emetric_space (π b)] : pseudo_emetric_space (Πb, π b) :=
+instance pseudo_emetric_space_pi [∀b, pseudo_emetric_space (π b)] :
+  pseudo_emetric_space (Πb, π b) :=
 { edist := λ f g, finset.sup univ (λb, edist (f b) (g b)),
   edist_self := assume f, bot_unique $ finset.sup_le $ by simp,
   edist_comm := assume f g, by unfold edist; congr; funext a; exact edist_comm _ _,
@@ -452,11 +452,11 @@ instance pseudoemetric_space_pi [∀b, pseudo_emetric_space (π b)] : pseudo_eme
     simp [set.ext_iff, εpos]
   end }
 
-lemma pseudoedist_pi_def [Π b, pseudo_emetric_space (π b)] (f g : Π b, π b) :
+lemma pseudo_edist_pi_def [Π b, pseudo_emetric_space (π b)] (f g : Π b, π b) :
   edist f g = finset.sup univ (λb, edist (f b) (g b)) := rfl
 
 @[priority 1100]
-lemma pseudoedist_pi_const [nonempty β] (a b : α) :
+lemma pseudo_edist_pi_const [nonempty β] (a b : α) :
   edist (λ x : β, a) (λ _, b) = edist a b := finset.sup_const univ_nonempty (edist a b)
 
 end pi
@@ -907,6 +907,17 @@ instance to_separated : separated_space γ :=
 separated_def.2 $ λ x y h, eq_of_forall_edist_le $
 λ ε ε0, le_of_lt (h _ (edist_mem_uniformity ε0))
 
+/-- If a  `pseudo_emetric_space` is separated, then it is an `emetric_space`. -/
+def emetric_of_t2_pseudo_emetric_space {α : Type*} [pseudo_emetric_space α]
+  (h : separated_space α) : emetric_space α :=
+{ eq_of_edist_eq_zero := λ x y hdist,
+  begin
+    refine separated_def.1 h x y (λ s hs, _),
+    obtain ⟨ε, hε, H⟩ := mem_uniformity_edist.1 hs,
+    exact H (show edist x y < ε, by rwa [hdist])
+  end
+  ..‹pseudo_emetric_space α› }
+
 /-- Auxiliary function to replace the uniformity on an emetric space with
 a uniformity which is equal to the original one, but maybe not defeq.
 This is useful if one wants to construct an emetric space with a
@@ -958,7 +969,7 @@ instance prod.emetric_space_max [emetric_space β] : emetric_space (γ × β) :=
     have B : x.snd = y.snd := edist_le_zero.1 h₂,
     exact prod.ext_iff.2 ⟨A, B⟩
   end,
-  ..prod.pseudoemetric_space_max }
+  ..prod.pseudo_emetric_space_max }
 
   lemma prod.edist_eq [emetric_space β] (x y : α × β) :
   edist x y = max (edist x.1 y.1) (edist x.2 y.2) :=
@@ -985,7 +996,7 @@ instance emetric_space_pi [∀b, emetric_space (π b)] : emetric_space (Πb, π
     simp only [finset.sup_le_iff] at eq1,
     exact (funext $ assume b, edist_le_zero.1 $ eq1 b $ mem_univ b),
   end,
-  ..pseudoemetric_space_pi }
+  ..pseudo_emetric_space_pi }
 
 lemma edist_pi_def [Π b, emetric_space (π b)] (f g : Π b, π b) :
   edist f g = finset.sup univ (λb, edist (f b) (g b)) := rfl

src/topology/metric_space/emetric_space.lean

@@ -5,7 +5,6 @@ Gluing metric spaces
 Authors: Sébastien Gouëzel
 -/
 import topology.metric_space.isometry
-import topology.metric_space.premetric_space
 
 /-!
 # Metric space gluing
@@ -52,7 +51,7 @@ noncomputable theory
 universes u v w
 variables {α : Type u} {β : Type v} {γ : Type w}
 
-open function set premetric
+open function set
 open_locale uniformity
 
 namespace metric
@@ -325,26 +324,26 @@ section gluing
 variables [nonempty γ] [metric_space γ] [metric_space α] [metric_space β]
           {Φ : γ → α} {Ψ : γ → β} {ε : ℝ}
 open sum (inl inr)
-local attribute [instance] premetric.dist_setoid
+local attribute [instance] pseudo_metric.dist_setoid
 
-def glue_premetric (hΦ : isometry Φ) (hΨ : isometry Ψ) : premetric_space (α ⊕ β) :=
+def glue_premetric (hΦ : isometry Φ) (hΨ : isometry Ψ) : pseudo_metric_space (α ⊕ β) :=
 { dist          := glue_dist Φ Ψ 0,
   dist_self     := glue_dist_self Φ Ψ 0,
   dist_comm     := glue_dist_comm Φ Ψ 0,
   dist_triangle := glue_dist_triangle Φ Ψ 0 $ λp q, by rw [hΦ.dist_eq, hΨ.dist_eq]; simp }
 
 def glue_space (hΦ : isometry Φ) (hΨ : isometry Ψ) : Type* :=
-@metric_quot _ (glue_premetric hΦ hΨ)
+@pseudo_metric_quot _ (glue_premetric hΦ hΨ)
 
 instance metric_space_glue_space (hΦ : isometry Φ) (hΨ : isometry Ψ) :
   metric_space (glue_space hΦ hΨ) :=
-@premetric.metric_space_quot _ (glue_premetric hΦ hΨ)
+@metric_space_quot _ (glue_premetric hΦ hΨ)
 
 def to_glue_l (hΦ : isometry Φ) (hΨ : isometry Ψ) (x : α) : glue_space hΦ hΨ :=
-by letI : premetric_space (α ⊕ β) := glue_premetric hΦ hΨ; exact ⟦inl x⟧
+by letI : pseudo_metric_space (α ⊕ β) := glue_premetric hΦ hΨ; exact ⟦inl x⟧
 
 def to_glue_r (hΦ : isometry Φ) (hΨ : isometry Ψ) (y : β) : glue_space hΦ hΨ :=
-by letI : premetric_space (α ⊕ β) := glue_premetric hΦ hΨ; exact ⟦inr y⟧
+by letI : pseudo_metric_space (α ⊕ β) := glue_premetric hΦ hΨ; exact ⟦inr y⟧
 
 instance inhabited_left (hΦ : isometry Φ) (hΨ : isometry Ψ) [inhabited α] :
   inhabited (glue_space hΦ hΨ) :=
@@ -357,7 +356,7 @@ instance inhabited_right (hΦ : isometry Φ) (hΨ : isometry Ψ) [inhabited β]
 lemma to_glue_commute (hΦ : isometry Φ) (hΨ : isometry Ψ) :
   (to_glue_l hΦ hΨ) ∘ Φ = (to_glue_r hΦ hΨ) ∘ Ψ :=
 begin
-  letI : premetric_space (α ⊕ β) := glue_premetric hΦ hΨ,
+  letI : pseudo_metric_space (α ⊕ β) := glue_premetric hΦ hΨ,
   funext,
   simp only [comp, to_glue_l, to_glue_r, quotient.eq],
   exact glue_dist_glued_points Φ Ψ 0 x
@@ -413,7 +412,7 @@ end
 
 /-- Premetric space structure on Σn, X n.-/
 def inductive_premetric (I : ∀n, isometry (f n)) :
-  premetric_space (Σn, X n) :=
+  pseudo_metric_space (Σn, X n) :=
 { dist          := inductive_limit_dist f,
   dist_self     := λx, by simp [dist, inductive_limit_dist],
   dist_comm     := λx y, begin
@@ -440,20 +439,20 @@ def inductive_premetric (I : ∀n, isometry (f n)) :
                 inductive_limit_dist_eq_dist I y z m hy hz]
   end }
 
-local attribute [instance] inductive_premetric premetric.dist_setoid
+local attribute [instance] inductive_premetric pseudo_metric.dist_setoid
 
 /-- The type giving the inductive limit in a metric space context. -/
 def inductive_limit (I : ∀n, isometry (f n)) : Type* :=
-@metric_quot _ (inductive_premetric I)
+@pseudo_metric_quot _ (inductive_premetric I)
 
 /-- Metric space structure on the inductive limit. -/
 instance metric_space_inductive_limit (I : ∀n, isometry (f n)) :
   metric_space (inductive_limit I) :=
-@premetric.metric_space_quot _ (inductive_premetric I)
+@metric_space_quot _ (inductive_premetric I)
 
 /-- Mapping each `X n` to the inductive limit. -/
 def to_inductive_limit (I : ∀n, isometry (f n)) (n : ℕ) (x : X n) : metric.inductive_limit I :=
-by letI : premetric_space (Σn, X n) := inductive_premetric I; exact ⟦sigma.mk n x⟧
+by letI : pseudo_metric_space (Σn, X n) := inductive_premetric I; exact ⟦sigma.mk n x⟧
 
 instance (I : ∀ n, isometry (f n)) [inhabited (X 0)] : inhabited (inductive_limit I) :=
 ⟨to_inductive_limit _ 0 (default _)⟩

src/topology/metric_space/gluing.lean

@@ -418,17 +418,17 @@ let ⟨Z1, Z2⟩ := classical.some_spec (exists_minimizer α β) in Z2 g hg
 /-- With the optimal candidate, construct a premetric space structure on α ⊕ β, on which the
 predistance is given by the candidate. Then, we will identify points at 0 predistance
 to obtain a genuine metric space -/
-def premetric_optimal_GH_dist : premetric_space (α ⊕ β) :=
+def premetric_optimal_GH_dist : pseudo_metric_space (α ⊕ β) :=
 { dist := λp q, optimal_GH_dist α β (p, q),
   dist_self := λx, candidates_refl (optimal_GH_dist_mem_candidates_b α β),
   dist_comm := λx y, candidates_symm (optimal_GH_dist_mem_candidates_b α β),
   dist_triangle := λx y z, candidates_triangle (optimal_GH_dist_mem_candidates_b α β) }
 
-local attribute [instance] premetric_optimal_GH_dist premetric.dist_setoid
+local attribute [instance] premetric_optimal_GH_dist pseudo_metric.dist_setoid
 
 /-- A metric space which realizes the optimal coupling between α and β -/
 @[derive [metric_space]] definition optimal_GH_coupling : Type* :=
-premetric.metric_quot (α ⊕ β)
+pseudo_metric_quot (α ⊕ β)
 
 /-- Injection of α in the optimal coupling between α and β -/
 def optimal_GH_injl (x : α) : optimal_GH_coupling α β := ⟦inl x⟧