feat(topology/metric_space/lipschitz): add several lemmas (#15634)

Some of these lemmas come from the sphere eversion project, with
slightly different names.

src/topology/metric_space/lipschitz.lean

@@ -84,6 +84,15 @@ lemma lipschitz_on_with_iff_restrict [pseudo_emetric_space α] [pseudo_emetric_s
   {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]
 
+alias lipschitz_on_with_iff_restrict ↔ lipschitz_on_with.to_restrict _
+
+lemma maps_to.lipschitz_on_with_iff_restrict [pseudo_emetric_space α] [pseudo_emetric_space β]
+  {K : ℝ≥0} {f : α → β} {s : set α} {t : set β} (h : maps_to f s t) :
+  lipschitz_on_with K f s ↔ lipschitz_with K (h.restrict f s t) :=
+lipschitz_on_with_iff_restrict
+
+alias maps_to.lipschitz_on_with_iff_restrict ↔ lipschitz_on_with.to_restrict_maps_to _
+
 namespace lipschitz_with
 
 section emetric
@@ -194,10 +203,7 @@ calc edist (f (g x)) (f (g y)) ≤ Kf * edist (g x) (g y) : hf _ _
 lemma comp_lipschitz_on_with {Kf Kg : ℝ≥0} {f : β → γ} {g : α → β} {s : set α}
   (hf : lipschitz_with Kf f) (hg : lipschitz_on_with Kg g s) :
   lipschitz_on_with (Kf * Kg) (f ∘ g) s :=
-assume x hx y hy,
-calc edist (f (g x)) (f (g y)) ≤ Kf * edist (g x) (g y) : hf _ _
-... ≤ Kf * (Kg * edist x y) : ennreal.mul_left_mono (hg hx hy)
-... = (Kf * Kg : ℝ≥0) * edist x y : by rw [← mul_assoc, ennreal.coe_mul]
+lipschitz_on_with_iff_restrict.mpr $ hf.comp hg.to_restrict
 
 protected lemma prod_fst : lipschitz_with 1 (@prod.fst α β) :=
 lipschitz_with.of_edist_le $ assume x y, le_max_left _ _
@@ -214,6 +220,12 @@ begin
   exact max_le_max (hf x y) (hg x y)
 end
 
+protected lemma prod_mk_left (a : α) : lipschitz_with 1 (prod.mk a : β → α × β) :=
+by simpa only [max_eq_right zero_le_one] using (lipschitz_with.const a).prod lipschitz_with.id
+
+protected lemma prod_mk_right (b : α) : lipschitz_with 1 (λ a : α, (a, b)) :=
+by simpa only [max_eq_left zero_le_one] using lipschitz_with.id.prod (lipschitz_with.const b)
+
 protected lemma uncurry {f : α → β → γ} {Kα Kβ : ℝ≥0} (hα : ∀ b, lipschitz_with Kα (λ a, f a b))
   (hβ : ∀ a, lipschitz_with Kβ (f a)) :
   lipschitz_with (Kα + Kβ) (function.uncurry f) :=
@@ -444,6 +456,11 @@ lemma edist_lt_of_edist_lt_div (hf : lipschitz_on_with K f s) {x y : α} (hx : x
 (lipschitz_on_with_iff_restrict.mp hf).edist_lt_of_edist_lt_div $
   show edist (⟨x, hx⟩ : s) ⟨y, hy⟩ < d / K, from hd
 
+protected lemma comp {g : β → γ} {t : set β} {Kg : ℝ≥0} (hg : lipschitz_on_with Kg g t)
+  (hf : lipschitz_on_with K f s) (hmaps : maps_to f s t) :
+  lipschitz_on_with (Kg * K) (g ∘ f) s :=
+lipschitz_on_with_iff_restrict.mpr $ hg.to_restrict.comp (hf.to_restrict_maps_to hmaps)
+
 end emetric
 
 section metric