refactor(topology/metric_space/lipschitz): generalize to pseudo_emetric_space (#6831)

This is part of a series of PR to introduce `semi_normed_group` in mathlib.

We introduce here Lipschitz maps for `pseudo_emetric_space` (I also improve some theorem name in `topology/metric_space/emetric_space`).

Author: riccardobrasca

src/analysis/normed_space/add_torsor.lean

@@ -226,10 +226,10 @@ calc edist (f x -ᵥ g x) (f y -ᵥ g y) ≤ edist (f x) (f y) + edist (g x) (g
   (add_mul _ _ _).symm
 
 lemma uniform_continuous_vadd : uniform_continuous (λ x : V × P, x.1 +ᵥ x.2) :=
-(lipschitz_with.prod_fst.vadd lipschitz_with.prod_snd).uniform_continuous
+((@lipschitz_with.prod_fst V P _ _).vadd lipschitz_with.prod_snd).uniform_continuous
 
 lemma uniform_continuous_vsub : uniform_continuous (λ x : P × P, x.1 -ᵥ x.2) :=
-(lipschitz_with.prod_fst.vsub lipschitz_with.prod_snd).uniform_continuous
+((@lipschitz_with.prod_fst P P _ _).vsub lipschitz_with.prod_snd).uniform_continuous
 
 lemma continuous_vadd : continuous (λ x : V × P, x.1 +ᵥ x.2) :=
 uniform_continuous_vadd.continuous

src/analysis/normed_space/basic.lean

@@ -583,7 +583,7 @@ end
 continuous. -/
 @[priority 100] -- see Note [lower instance priority]
 instance normed_uniform_group : uniform_add_group α :=
-⟨(lipschitz_with.prod_fst.sub lipschitz_with.prod_snd).uniform_continuous⟩
+⟨((@lipschitz_with.prod_fst α α _ _).sub lipschitz_with.prod_snd).uniform_continuous⟩
 
 @[priority 100] -- see Note [lower instance priority]
 instance normed_top_monoid : has_continuous_add α :=

src/topology/metric_space/basic.lean

@@ -1174,7 +1174,7 @@ begin
   { assume x y,
     rw ← lt_top_iff_ne_top,
     have : (⊥ : ℝ≥0∞) < ⊤ := ennreal.coe_lt_top,
-    simp [pseudo_edist_pi_def, finset.sup_lt_iff this, edist_lt_top] },
+    simp [edist_pi_def, finset.sup_lt_iff this, edist_lt_top] },
   show ∀ (x y : Π (b : β), π b), ↑(sup univ (λ (b : β), nndist (x b) (y b))) =
     ennreal.to_real (sup univ (λ (b : β), edist (x b) (y b))),
   { assume x y,

src/topology/metric_space/emetric_space.lean

@@ -418,7 +418,7 @@ instance prod.pseudo_emetric_space_max [pseudo_emetric_space β] : pseudo_emetri
   end,
   to_uniform_space := prod.uniform_space }
 
-lemma prod.pesudoedist_eq [pseudo_emetric_space β] (x y : α × β) :
+lemma prod.edist_eq [pseudo_emetric_space β] (x y : α × β) :
   edist x y = max (edist x.1 y.1) (edist x.2 y.2) :=
 rfl
 
@@ -452,11 +452,11 @@ instance pseudo_emetric_space_pi [∀b, pseudo_emetric_space (π b)] :
     simp [set.ext_iff, εpos]
   end }
 
-lemma pseudo_edist_pi_def [Π b, pseudo_emetric_space (π b)] (f g : Π b, π b) :
+lemma 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 pseudo_edist_pi_const [nonempty β] (a b : α) :
+@[simp]
+lemma edist_pi_const [nonempty β] (a b : α) :
   edist (λ x : β, a) (λ _, b) = edist a b := finset.sup_const univ_nonempty (edist a b)
 
 end pi
@@ -971,10 +971,6 @@ instance prod.emetric_space_max [emetric_space β] : emetric_space (γ × β) :=
   end,
   ..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) :=
-rfl
-
 /-- Reformulation of the uniform structure in terms of the extended distance -/
 theorem uniformity_edist :
   𝓤 γ = ⨅ ε>0, 𝓟 {p:γ×γ | edist p.1 p.2 < ε} :=
@@ -998,12 +994,6 @@ instance emetric_space_pi [∀b, emetric_space (π b)] : emetric_space (Πb, π
   end,
   ..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
-
-@[simp] lemma edist_pi_const [nonempty β] (a b : α) : edist (λ x : β, a) (λ _, b) = edist a b :=
-finset.sup_const univ_nonempty (edist a b)
-
 end pi
 
 namespace emetric

src/topology/metric_space/lipschitz.lean

@@ -45,48 +45,51 @@ variables {α : Type u} {β : Type v} {γ : Type w} {ι : Type x}
 
 /-- A function `f` is Lipschitz continuous with constant `K ≥ 0` if for all `x, y`
 we have `dist (f x) (f y) ≤ K * dist x y` -/
-def lipschitz_with [emetric_space α] [emetric_space β] (K : ℝ≥0) (f : α → β) :=
+def lipschitz_with [pseudo_emetric_space α] [pseudo_emetric_space β] (K : ℝ≥0) (f : α → β) :=
 ∀x y, edist (f x) (f y) ≤ K * edist x y
 
-lemma lipschitz_with_iff_dist_le_mul [metric_space α] [metric_space β] {K : ℝ≥0} {f : α → β} :
-  lipschitz_with K f ↔ ∀ x y, dist (f x) (f y) ≤ K * dist x y :=
+lemma lipschitz_with_iff_dist_le_mul [pseudo_metric_space α] [pseudo_metric_space β] {K : ℝ≥0}
+  {f : α → β} : lipschitz_with K f ↔ ∀ x y, dist (f x) (f y) ≤ K * dist x y :=
 by { simp only [lipschitz_with, edist_nndist, dist_nndist], norm_cast }
 
 alias lipschitz_with_iff_dist_le_mul ↔ lipschitz_with.dist_le_mul lipschitz_with.of_dist_le_mul
 
 /-- A function `f` is Lipschitz continuous with constant `K ≥ 0` on `s` if for all `x, y` in `s`
 we have `dist (f x) (f y) ≤ K * dist x y` -/
-def lipschitz_on_with [emetric_space α] [emetric_space β] (K : ℝ≥0) (f : α → β) (s : set α) :=
+def lipschitz_on_with [pseudo_emetric_space α] [pseudo_emetric_space β] (K : ℝ≥0) (f : α → β)
+  (s : set α) :=
 ∀ ⦃x⦄ (hx : x ∈ s) ⦃y⦄ (hy : y ∈ s), edist (f x) (f y) ≤ K * edist x y
 
-@[simp] lemma lipschitz_on_with_empty [emetric_space α] [emetric_space β] (K : ℝ≥0) (f : α → β) :
-  lipschitz_on_with K f ∅ :=
+@[simp] lemma lipschitz_on_with_empty [pseudo_emetric_space α] [pseudo_emetric_space β] (K : ℝ≥0)
+  (f : α → β) : lipschitz_on_with K f ∅ :=
 λ x x_in y y_in, false.elim x_in
 
-lemma lipschitz_on_with.mono [emetric_space α] [emetric_space β] {K : ℝ≥0} {s t : set α} {f : α → β}
-  (hf : lipschitz_on_with K f t) (h : s ⊆ t) : lipschitz_on_with K f s :=
+lemma lipschitz_on_with.mono [pseudo_emetric_space α] [pseudo_emetric_space β] {K : ℝ≥0}
+  {s t : set α} {f : α → β} (hf : lipschitz_on_with K f t) (h : s ⊆ t) : lipschitz_on_with K f s :=
 λ x x_in y y_in, hf (h x_in) (h y_in)
 
-lemma lipschitz_on_with_iff_dist_le_mul [metric_space α] [metric_space β] {K : ℝ≥0} {s : set α}
-  {f : α → β} : lipschitz_on_with K f s ↔ ∀ (x ∈ s) (y ∈ s), dist (f x) (f y) ≤ K * dist x y :=
+lemma lipschitz_on_with_iff_dist_le_mul [pseudo_metric_space α] [pseudo_metric_space β] {K : ℝ≥0}
+  {s : set α} {f : α → β} :
+  lipschitz_on_with K f s ↔ ∀ (x ∈ s) (y ∈ s), dist (f x) (f y) ≤ K * dist x y :=
 by { simp only [lipschitz_on_with, edist_nndist, dist_nndist], norm_cast }
 
 alias lipschitz_on_with_iff_dist_le_mul ↔
   lipschitz_on_with.dist_le_mul lipschitz_on_with.of_dist_le_mul
 
-@[simp] lemma lipschitz_on_univ [emetric_space α] [emetric_space β] {K : ℝ≥0} {f : α → β} :
-  lipschitz_on_with K f univ ↔ lipschitz_with K f :=
+@[simp] lemma lipschitz_on_univ [pseudo_emetric_space α] [pseudo_emetric_space β] {K : ℝ≥0}
+  {f : α → β} : lipschitz_on_with K f univ ↔ lipschitz_with K f :=
 by simp [lipschitz_on_with, lipschitz_with]
 
-lemma lipschitz_on_with_iff_restrict [emetric_space α] [emetric_space β] {K : ℝ≥0}
+lemma lipschitz_on_with_iff_restrict [pseudo_emetric_space α] [pseudo_emetric_space β] {K : ℝ≥0}
   {f : α → β} {s : set α} : lipschitz_on_with K f s ↔ lipschitz_with K (s.restrict f) :=
 by simp only [lipschitz_on_with, lipschitz_with, set_coe.forall', restrict, subtype.edist_eq]
 
 namespace lipschitz_with
 
 section emetric
 
-variables [emetric_space α] [emetric_space β] [emetric_space γ] {K : ℝ≥0} {f : α → β}
+variables [pseudo_emetric_space α] [pseudo_emetric_space β] [pseudo_emetric_space γ]
+variables {K : ℝ≥0} {f : α → β}
 
 lemma edist_le_mul (h : lipschitz_with K f) (x y : α) : edist (f x) (f y) ≤ K * edist x y := h x y
 
@@ -221,7 +224,7 @@ end emetric
 
 section metric
 
-variables [metric_space α] [metric_space β] [metric_space γ] {K : ℝ≥0}
+variables [pseudo_metric_space α] [pseudo_metric_space β] [pseudo_metric_space γ] {K : ℝ≥0}
 
 protected lemma of_dist_le' {f : α → β} {K : ℝ} (h : ∀ x y, dist (f x) (f y) ≤ K * dist x y) :
   lipschitz_with (nnreal.of_real K) f :=
@@ -296,7 +299,8 @@ end lipschitz_with
 
 namespace lipschitz_on_with
 
-variables [emetric_space α] [emetric_space β] [emetric_space γ] {K : ℝ≥0} {s : set α} {f : α → β}
+variables [pseudo_emetric_space α] [pseudo_emetric_space β] [pseudo_emetric_space γ]
+variables {K : ℝ≥0} {s : set α} {f : α → β}
 
 protected lemma uniform_continuous_on (hf : lipschitz_on_with K f s) : uniform_continuous_on f s :=
 uniform_continuous_on_iff_restrict.mpr (lipschitz_on_with_iff_restrict.mp hf).uniform_continuous