feat: the extension of a Lipschitz function is Lipschitz (leanprover-community#34438)

Cherry picked from leanprover-community#34055.

Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

Author: sgouezel

Mathlib/MeasureTheory/Constructions/BorelSpace/Order.lean

@@ -427,6 +427,17 @@ theorem borel_eq_generateFrom_Ioc (α : Type*) [TopologicalSpace α] [SecondCoun
     (@dense_univ α _).borel_eq_generateFrom_Ioc_mem_aux (fun _ _ => mem_univ _) fun _ _ _ _ =>
       mem_univ _
 
+theorem borel_eq_generateFrom_Ioc_le (α : Type*) [TopologicalSpace α] [SecondCountableTopology α]
+    [LinearOrder α] [OrderTopology α] :
+    borel α = .generateFrom { S : Set α | ∃ l u, l ≤ u ∧ Ioc l u = S } := by
+  apply le_antisymm
+  · rw [borel_eq_generateFrom_Ioc]
+    apply generateFrom_mono (by grind)
+  · apply generateFrom_le
+    rintro - ⟨u, v, -, rfl⟩
+    borelize α
+    exact measurableSet_Ioc
+
 namespace MeasureTheory.Measure
 
 /-- Two finite measures on a Borel space are equal if they agree on all closed-open intervals.  If

Mathlib/Topology/Instances/ENNReal/Lemmas.lean

@@ -910,3 +910,20 @@ theorem limsup_add_of_left_tendsto_zero {u : Filter ι} {f : ι → ℝ≥0∞}
 end LimsupLiminf
 
 end ENNReal -- namespace
+
+lemma Dense.lipschitzWith_extend {α β : Type*}
+    [PseudoEMetricSpace α] [EMetricSpace β] [CompleteSpace β]
+    {s : Set α} (hs : Dense s) {f : s → β} {K : ℝ≥0} (hf : LipschitzWith K f) :
+    LipschitzWith K (hs.extend f) := by
+  have : IsClosed {p : α × α | edist (hs.extend f p.1) (hs.extend f p.2) ≤ K * edist p.1 p.2} := by
+    have : Continuous (hs.extend f) := (hs.uniformContinuous_extend hf.uniformContinuous).continuous
+    apply isClosed_le (by fun_prop)
+    exact (ENNReal.continuous_const_mul (by simp)).comp (by fun_prop)
+  have : Dense {p : α × α | edist (hs.extend f p.1) (hs.extend f p.2) ≤ K * edist p.1 p.2} := by
+    apply (hs.prod hs).mono
+    rintro ⟨x, y⟩ ⟨hx, hy⟩
+    have Ax : hs.extend f x = f ⟨x, hx⟩ := hs.extend_eq hf.continuous ⟨x, hx⟩
+    have Ay : hs.extend f y = f ⟨y, hy⟩ := hs.extend_eq hf.continuous ⟨y, hy⟩
+    simp only [Set.mem_setOf_eq, Ax, Ay]
+    exact hf ⟨x, hx⟩ ⟨y, hy⟩
+  simpa only [Dense, IsClosed.closure_eq, Set.mem_setOf_eq, Prod.forall] using this