doc-next-gen

Mathlib.Topology.MetricSpace.Lipschitz

Module docstring

{"# Lipschitz continuous functions

A map f : α → β between two (extended) metric spaces is called Lipschitz continuous with constant K ≥ 0 if for all x, y we have edist (f x) (f y) ≤ K * edist x y. For a metric space, the latter inequality is equivalent to dist (f x) (f y) ≤ K * dist x y. There is also a version asserting this inequality only for x and y in some set s. Finally, f : α → β is called locally Lipschitz continuous if each x : α has a neighbourhood on which f is Lipschitz continuous (with some constant).

In this file we specialize various facts about Lipschitz continuous maps to the case of (pseudo) metric spaces.

Implementation notes

The parameter K has type ℝ≥0. This way we avoid conjunction in the definition and have coercions both to ℝ and ℝ≥0∞. Constructors whose names end with ' take K : ℝ as an argument, and return LipschitzWith (Real.toNNReal K) f. "}

lipschitzWith_iff_dist_le_mul theorem
[PseudoMetricSpace α] [PseudoMetricSpace β] {K : ℝ≥0} {f : α → β} : LipschitzWith K f ↔ ∀ x y, dist (f x) (f y) ≤ K * dist x y
Full source 
theorem lipschitzWith_iff_dist_le_mul [PseudoMetricSpace α] [PseudoMetricSpace β] {K : ℝ≥0}
    {f : α → β} : LipschitzWithLipschitzWith K f ↔ ∀ x y, dist (f x) (f y) ≤ K * dist x y := by
  simp only [LipschitzWith, edist_nndist, dist_nndist]
  norm_cast
Characterization of Lipschitz Continuity via Distance Inequality
Informal description
Let $\alpha$ and $\beta$ be pseudometric spaces, and let $f : \alpha \to \beta$ be a function. For any nonnegative real number $K \geq 0$, the function $f$ is Lipschitz continuous with constant $K$ if and only if for all $x, y \in \alpha$, the distance between $f(x)$ and $f(y)$ satisfies $\text{dist}(f(x), f(y)) \leq K \cdot \text{dist}(x, y)$.
lipschitzOnWith_iff_dist_le_mul theorem
[PseudoMetricSpace α] [PseudoMetricSpace β] {K : ℝ≥0} {s : Set α} {f : α → β} : LipschitzOnWith K f s ↔ ∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ K * dist x y
Full source 
theorem lipschitzOnWith_iff_dist_le_mul [PseudoMetricSpace α] [PseudoMetricSpace β] {K : ℝ≥0}
    {s : Set α} {f : α → β} :
    LipschitzOnWithLipschitzOnWith K f s ↔ ∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ K * dist x y := by
  simp only [LipschitzOnWith, edist_nndist, dist_nndist]
  norm_cast
Characterization of Lipschitz Continuity on a Subset via Distance Inequality
Informal description
Let $\alpha$ and $\beta$ be pseudometric spaces, $K \geq 0$ a nonnegative real number, $s \subseteq \alpha$ a subset, and $f: \alpha \to \beta$ a function. Then $f$ is Lipschitz continuous on $s$ with constant $K$ if and only if for all $x, y \in s$, the distance between $f(x)$ and $f(y)$ satisfies $\text{dist}(f(x), f(y)) \leq K \cdot \text{dist}(x, y)$.
LipschitzWith.of_dist_le' theorem
{K : ℝ} (h : ∀ x y, dist (f x) (f y) ≤ K * dist x y) : LipschitzWith (Real.toNNReal K) f
Full source 
protected theorem of_dist_le' {K : ℝ} (h : ∀ x y, dist (f x) (f y) ≤ K * dist x y) :
    LipschitzWith (Real.toNNReal K) f :=
  of_dist_le_mul fun x y =>
    le_trans (h x y) <| by gcongr; apply Real.le_coe_toNNReal
Lipschitz Continuity from Distance Inequality with Real Constant
Informal description
Let $f : \alpha \to \beta$ be a function between pseudometric spaces $\alpha$ and $\beta$. If there exists a real number $K$ such that for all $x, y \in \alpha$, the distance $\text{dist}(f(x), f(y)) \leq K \cdot \text{dist}(x, y)$, then $f$ is Lipschitz continuous with constant $\text{Real.toNNReal}(K)$.
LipschitzWith.mk_one theorem
(h : ∀ x y, dist (f x) (f y) ≤ dist x y) : LipschitzWith 1 f
Full source 
protected theorem mk_one (h : ∀ x y, dist (f x) (f y) ≤ dist x y) : LipschitzWith 1 f :=
  of_dist_le_mul <| by simpa only [NNReal.coe_one, one_mul] using h
Lipschitz Constant One from Distance Inequality
Informal description
Let $\alpha$ and $\beta$ be pseudometric spaces and $f: \alpha \to \beta$ a function. If for all $x, y \in \alpha$ the distance inequality $\text{dist}(f(x), f(y)) \leq \text{dist}(x, y)$ holds, then $f$ is Lipschitz continuous with constant $1$.
LipschitzWith.of_le_add_mul' theorem
{f : α → ℝ} (K : ℝ) (h : ∀ x y, f x ≤ f y + K * dist x y) : LipschitzWith (Real.toNNReal K) f
Full source 
/-- For functions to `ℝ`, it suffices to prove `f x ≤ f y + K * dist x y`; this version
doesn't assume `0≤K`. -/
protected theorem of_le_add_mul' {f : α → ℝ} (K : ℝ) (h : ∀ x y, f x ≤ f y + K * dist x y) :
    LipschitzWith (Real.toNNReal K) f :=
  have I : ∀ x y, f x - f y ≤ K * dist x y := fun x y => sub_le_iff_le_add'.2 (h x y)
  LipschitzWith.of_dist_le' fun x y => abs_sub_le_iff.2 ⟨I x y, dist_comm y x ▸ I y x⟩
Lipschitz Continuity from One-Sided Distance Inequality with Real Constant
Informal description
Let $f : \alpha \to \mathbb{R}$ be a function from a pseudometric space $\alpha$ to the real numbers. If there exists a real constant $K$ such that for all $x, y \in \alpha$, the inequality $f(x) \leq f(y) + K \cdot \text{dist}(x, y)$ holds, then $f$ is Lipschitz continuous with constant $\text{Real.toNNReal}(K)$.
LipschitzWith.of_le_add_mul theorem
{f : α → ℝ} (K : ℝ≥0) (h : ∀ x y, f x ≤ f y + K * dist x y) : LipschitzWith K f
Full source 
/-- For functions to `ℝ`, it suffices to prove `f x ≤ f y + K * dist x y`; this version
assumes `0≤K`. -/
protected theorem of_le_add_mul {f : α → ℝ} (K : ℝ≥0) (h : ∀ x y, f x ≤ f y + K * dist x y) :
    LipschitzWith K f := by simpa only [Real.toNNReal_coe] using LipschitzWith.of_le_add_mul' K h
Lipschitz continuity from one-sided distance inequality
Informal description
Let $f \colon \alpha \to \mathbb{R}$ be a function from a pseudometric space $\alpha$ to the real numbers. If there exists a nonnegative real constant $K$ such that for all $x, y \in \alpha$, the inequality $f(x) \leq f(y) + K \cdot \text{dist}(x, y)$ holds, then $f$ is Lipschitz continuous with constant $K$.
LipschitzWith.of_le_add theorem
{f : α → ℝ} (h : ∀ x y, f x ≤ f y + dist x y) : LipschitzWith 1 f
Full source 
protected theorem of_le_add {f : α → ℝ} (h : ∀ x y, f x ≤ f y + dist x y) : LipschitzWith 1 f :=
  LipschitzWith.of_le_add_mul 1 <| by simpa only [NNReal.coe_one, one_mul]
Lipschitz continuity from one-sided distance inequality with constant 1
Informal description
Let $f \colon \alpha \to \mathbb{R}$ be a function from a pseudometric space $\alpha$ to the real numbers. If for all $x, y \in \alpha$, the inequality $f(x) \leq f(y) + \text{dist}(x, y)$ holds, then $f$ is Lipschitz continuous with constant $1$.
LipschitzWith.le_add_mul theorem
{f : α → ℝ} {K : ℝ≥0} (h : LipschitzWith K f) (x y) : f x ≤ f y + K * dist x y
Full source 
protected theorem le_add_mul {f : α → ℝ} {K : ℝ≥0} (h : LipschitzWith K f) (x y) :
    f x ≤ f y + K * dist x y :=
  sub_le_iff_le_add'.1 <| le_trans (le_abs_self _) <| h.dist_le_mul x y
Lipschitz Function Bound: $f(x) \leq f(y) + K \cdot \text{dist}(x, y)$
Informal description
Let $f \colon \alpha \to \mathbb{R}$ be a Lipschitz continuous function with constant $K \geq 0$ between a pseudometric space $\alpha$ and the real numbers. Then for any two points $x, y \in \alpha$, we have the inequality: \[ f(x) \leq f(y) + K \cdot \text{dist}(x, y). \]
LipschitzWith.iff_le_add_mul theorem
{f : α → ℝ} {K : ℝ≥0} : LipschitzWith K f ↔ ∀ x y, f x ≤ f y + K * dist x y
Full source 
protected theorem iff_le_add_mul {f : α → ℝ} {K : ℝ≥0} :
    LipschitzWithLipschitzWith K f ↔ ∀ x y, f x ≤ f y + K * dist x y :=
  ⟨LipschitzWith.le_add_mul, LipschitzWith.of_le_add_mul K⟩
Lipschitz Continuity Criterion: $f$ is $K$-Lipschitz $\iff$ $f(x) \leq f(y) + K \cdot \text{dist}(x, y)$ for all $x, y$
Informal description
Let $f \colon \alpha \to \mathbb{R}$ be a function from a pseudometric space $\alpha$ to the real numbers, and let $K \geq 0$ be a nonnegative real constant. Then $f$ is Lipschitz continuous with constant $K$ if and only if for all $x, y \in \alpha$, the following inequality holds: \[ f(x) \leq f(y) + K \cdot \text{dist}(x, y). \]
LipschitzWith.nndist_le theorem
(hf : LipschitzWith K f) (x y : α) : nndist (f x) (f y) ≤ K * nndist x y
Full source 
theorem nndist_le (hf : LipschitzWith K f) (x y : α) : nndist (f x) (f y) ≤ K * nndist x y :=
  hf.dist_le_mul x y
Non-negative distance bound for Lipschitz continuous functions
Informal description
Let $f : \alpha \to \beta$ be a Lipschitz continuous function between pseudometric spaces with constant $K \geq 0$. Then for any two points $x, y \in \alpha$, the non-negative distance between $f(x)$ and $f(y)$ is bounded by $K$ times the non-negative distance between $x$ and $y$, i.e., \[ \text{nndist}(f(x), f(y)) \leq K \cdot \text{nndist}(x, y). \]
LipschitzWith.dist_le_mul_of_le theorem
(hf : LipschitzWith K f) (hr : dist x y ≤ r) : dist (f x) (f y) ≤ K * r
Full source 
theorem dist_le_mul_of_le (hf : LipschitzWith K f) (hr : dist x y ≤ r) : dist (f x) (f y) ≤ K * r :=
  (hf.dist_le_mul x y).trans <| by gcongr
Lipschitz Estimate: $\text{dist}(f(x), f(y)) \leq K \cdot r$ when $\text{dist}(x, y) \leq r$
Informal description
Let $f : \alpha \to \beta$ be a Lipschitz continuous map between pseudometric spaces with constant $K \geq 0$. For any points $x, y \in \alpha$ and any real number $r \geq 0$, if the distance between $x$ and $y$ satisfies $\text{dist}(x, y) \leq r$, then the distance between their images satisfies $\text{dist}(f(x), f(y)) \leq K \cdot r$.
LipschitzWith.mapsTo_closedBall theorem
(hf : LipschitzWith K f) (x : α) (r : ℝ) : MapsTo f (Metric.closedBall x r) (Metric.closedBall (f x) (K * r))
Full source 
theorem mapsTo_closedBall (hf : LipschitzWith K f) (x : α) (r : ℝ) :
    MapsTo f (Metric.closedBall x r) (Metric.closedBall (f x) (K * r)) := fun _y hy =>
  hf.dist_le_mul_of_le hy
Lipschitz continuous functions map closed balls to closed balls
Informal description
Let $f : \alpha \to \beta$ be a Lipschitz continuous function between pseudometric spaces with constant $K \geq 0$. For any point $x \in \alpha$ and any radius $r \geq 0$, the function $f$ maps the closed ball $\overline{B}(x, r)$ into the closed ball $\overline{B}(f(x), K \cdot r)$. In other words, for every $y \in \overline{B}(x, r)$, we have $f(y) \in \overline{B}(f(x), K \cdot r)$.
LipschitzWith.dist_lt_mul_of_lt theorem
(hf : LipschitzWith K f) (hK : K ≠ 0) (hr : dist x y < r) : dist (f x) (f y) < K * r
Full source 
theorem dist_lt_mul_of_lt (hf : LipschitzWith K f) (hK : K ≠ 0) (hr : dist x y < r) :
    dist (f x) (f y) < K * r :=
  (hf.dist_le_mul x y).trans_lt <| (mul_lt_mul_left <| NNReal.coe_pos.2 hK.bot_lt).2 hr
Lipschitz continuity preserves strict distance inequalities: $\text{dist}(x,y) < r \implies \text{dist}(f(x),f(y)) < K r$
Informal description
Let $f : \alpha \to \beta$ be a Lipschitz continuous function between pseudometric spaces with constant $K > 0$. For any $x, y \in \alpha$ and $r > 0$, if $\text{dist}(x, y) < r$, then $\text{dist}(f(x), f(y)) < K \cdot r$.
LipschitzWith.mapsTo_ball theorem
(hf : LipschitzWith K f) (hK : K ≠ 0) (x : α) (r : ℝ) : MapsTo f (Metric.ball x r) (Metric.ball (f x) (K * r))
Full source 
theorem mapsTo_ball (hf : LipschitzWith K f) (hK : K ≠ 0) (x : α) (r : ℝ) :
    MapsTo f (Metric.ball x r) (Metric.ball (f x) (K * r)) := fun _y hy =>
  hf.dist_lt_mul_of_lt hK hy
Lipschitz continuous functions preserve open balls
Informal description
Let $f \colon \alpha \to \beta$ be a Lipschitz continuous function between pseudometric spaces with constant $K > 0$. For any point $x \in \alpha$ and radius $r > 0$, the function $f$ maps the open ball $\text{ball}(x, r)$ into the open ball $\text{ball}(f(x), K \cdot r)$.
LipschitzWith.toLocallyBoundedMap definition
(f : α → β) (hf : LipschitzWith K f) : LocallyBoundedMap α β
Full source 
/-- A Lipschitz continuous map is a locally bounded map. -/
def toLocallyBoundedMap (f : α → β) (hf : LipschitzWith K f) : LocallyBoundedMap α β :=
  LocallyBoundedMap.ofMapBounded f fun _s hs =>
    let ⟨C, hC⟩ := Metric.isBounded_iff.1 hs
    Metric.isBounded_iff.2 ⟨K * C, forall_mem_image.2 fun _x hx => forall_mem_image.2 fun _y hy =>
      hf.dist_le_mul_of_le (hC hx hy)⟩
Locally bounded map induced by a Lipschitz function
Informal description
Given a Lipschitz continuous function $f : \alpha \to \beta$ with constant $K$, the function $f$ induces a locally bounded map between the pseudometric spaces $\alpha$ and $\beta$. Specifically, for any bounded subset $s \subseteq \alpha$, the image $f(s)$ is bounded in $\beta$ with a bound proportional to $K$ times the bound of $s$.
LipschitzWith.coe_toLocallyBoundedMap theorem
(hf : LipschitzWith K f) : ⇑(hf.toLocallyBoundedMap f) = f
Full source 
@[simp]
theorem coe_toLocallyBoundedMap (hf : LipschitzWith K f) : ⇑(hf.toLocallyBoundedMap f) = f :=
  rfl
Underlying Function of Induced Locally Bounded Map from Lipschitz Function
Informal description
For any Lipschitz continuous function $f \colon \alpha \to \beta$ with constant $K$, the underlying function of the induced locally bounded map is equal to $f$ itself.
LipschitzWith.comap_cobounded_le theorem
(hf : LipschitzWith K f) : comap f (Bornology.cobounded β) ≤ Bornology.cobounded α
Full source 
theorem comap_cobounded_le (hf : LipschitzWith K f) :
    comap f (Bornology.cobounded β) ≤ Bornology.cobounded α :=
  (hf.toLocallyBoundedMap f).2
Lipschitz Functions Preserve Cofiltered Boundedness
Informal description
Let $f : \alpha \to \beta$ be a Lipschitz continuous function between pseudometric spaces with constant $K \geq 0$. Then the preimage under $f$ of the cobounded filter on $\beta$ is contained in the cobounded filter on $\alpha$. In other words, if a subset $S \subseteq \beta$ has bounded complement, then $f^{-1}(S)$ has bounded complement in $\alpha$.
LipschitzWith.isBounded_image theorem
(hf : LipschitzWith K f) {s : Set α} (hs : IsBounded s) : IsBounded (f '' s)
Full source 
/-- The image of a bounded set under a Lipschitz map is bounded. -/
theorem isBounded_image (hf : LipschitzWith K f) {s : Set α} (hs : IsBounded s) :
    IsBounded (f '' s) :=
  hs.image (toLocallyBoundedMap f hf)
Boundedness of Images under Lipschitz Maps
Informal description
Let $f : \alpha \to \beta$ be a Lipschitz continuous map between pseudometric spaces with constant $K \geq 0$. For any bounded subset $s \subseteq \alpha$, the image $f(s) \subseteq \beta$ is bounded.
LipschitzWith.diam_image_le theorem
(hf : LipschitzWith K f) (s : Set α) (hs : IsBounded s) : Metric.diam (f '' s) ≤ K * Metric.diam s
Full source 
theorem diam_image_le (hf : LipschitzWith K f) (s : Set α) (hs : IsBounded s) :
    Metric.diam (f '' s) ≤ K * Metric.diam s :=
  Metric.diam_le_of_forall_dist_le (mul_nonneg K.coe_nonneg Metric.diam_nonneg) <|
    forall_mem_image.2 fun _x hx =>
      forall_mem_image.2 fun _y hy => hf.dist_le_mul_of_le <| Metric.dist_le_diam_of_mem hs hx hy
Diameter Bound for Images under Lipschitz Maps: $\text{diam}(f(s)) \leq K \cdot \text{diam}(s)$
Informal description
Let $f \colon \alpha \to \beta$ be a Lipschitz continuous map between pseudometric spaces with constant $K \geq 0$. For any bounded subset $s \subseteq \alpha$, the diameter of the image $f(s)$ satisfies $\text{diam}(f(s)) \leq K \cdot \text{diam}(s)$.
LipschitzWith.dist_left theorem
(y : α) : LipschitzWith 1 (dist · y)
Full source 
protected theorem dist_left (y : α) : LipschitzWith 1 (dist · y) :=
  LipschitzWith.mk_one fun _ _ => dist_dist_dist_le_left _ _ _
Lipschitz Continuity of Distance Function (Left Argument)
Informal description
For any fixed point $y$ in a pseudometric space $\alpha$, the function $x \mapsto \text{dist}(x, y)$ is Lipschitz continuous with constant $1$.
LipschitzWith.dist_right theorem
(x : α) : LipschitzWith 1 (dist x)
Full source 
protected theorem dist_right (x : α) : LipschitzWith 1 (dist x) :=
  LipschitzWith.of_le_add fun _ _ => dist_triangle_right _ _ _
Lipschitz Continuity of Distance Function (Right Argument)
Informal description
For any fixed point $x$ in a pseudometric space $\alpha$, the function $y \mapsto \text{dist}(x, y)$ is Lipschitz continuous with constant $1$.
LipschitzWith.dist theorem
: LipschitzWith 2 (Function.uncurry <| @dist α _)
Full source 
protected theorem dist : LipschitzWith 2 (Function.uncurry <| @dist α _) := by
  rw [← one_add_one_eq_two]
  exact LipschitzWith.uncurry LipschitzWith.dist_left LipschitzWith.dist_right
Lipschitz Continuity of Distance Function with Constant 2
Informal description
The distance function $\text{dist} : \alpha \times \alpha \to \mathbb{R}$ on a pseudometric space $\alpha$ is Lipschitz continuous with constant $2$ when viewed as a function of both arguments (i.e., when uncurried).
LipschitzWith.dist_iterate_succ_le_geometric theorem
{f : α → α} (hf : LipschitzWith K f) (x n) : dist (f^[n] x) (f^[n + 1] x) ≤ dist x (f x) * (K : ℝ) ^ n
Full source 
theorem dist_iterate_succ_le_geometric {f : α → α} (hf : LipschitzWith K f) (x n) :
    dist (f^[n] x) (f^[n + 1] x) ≤ dist x (f x) * (K : ℝ) ^ n := by
  rw [iterate_succ, mul_comm]
  simpa only [NNReal.coe_pow] using (hf.iterate n).dist_le_mul x (f x)
Geometric Bound for Iterated Lipschitz Function Distances
Informal description
Let $(α, d)$ be a pseudometric space and $f : α \to α$ be a $K$-Lipschitz function. Then for any point $x \in α$ and natural number $n$, the distance between the $n$-th iterate and $(n+1)$-th iterate of $f$ at $x$ satisfies: $$ d(f^{[n]}(x), f^{[n+1]}(x)) \leq d(x, f(x)) \cdot K^n $$ where $f^{[n]}$ denotes the $n$-fold composition of $f$ with itself.
lipschitzWith_max theorem
: LipschitzWith 1 fun p : ℝ × ℝ => max p.1 p.2
Full source 
theorem _root_.lipschitzWith_max : LipschitzWith 1 fun p : ℝℝ × ℝ => max p.1 p.2 :=
  LipschitzWith.of_le_add fun _ _ => sub_le_iff_le_add'.1 <|
    (le_abs_self _).trans (abs_max_sub_max_le_max _ _ _ _)
Lipschitz Continuity of the Maximum Function with Constant 1
Informal description
The function $f \colon \mathbb{R} \times \mathbb{R} \to \mathbb{R}$ defined by $f(x, y) = \max(x, y)$ is Lipschitz continuous with constant $1$ with respect to the supremum distance on $\mathbb{R} \times \mathbb{R}$.
lipschitzWith_min theorem
: LipschitzWith 1 fun p : ℝ × ℝ => min p.1 p.2
Full source 
theorem _root_.lipschitzWith_min : LipschitzWith 1 fun p : ℝℝ × ℝ => min p.1 p.2 :=
  LipschitzWith.of_le_add fun _ _ => sub_le_iff_le_add'.1 <|
    (le_abs_self _).trans (abs_min_sub_min_le_max _ _ _ _)
Lipschitz Continuity of the Minimum Function with Constant 1
Informal description
The function $\min \colon \mathbb{R} \times \mathbb{R} \to \mathbb{R}$, defined by $(x, y) \mapsto \min(x, y)$, is Lipschitz continuous with constant $1$.
Real.lipschitzWith_toNNReal theorem
: LipschitzWith 1 Real.toNNReal
Full source 
lemma _root_.Real.lipschitzWith_toNNReal : LipschitzWith 1 Real.toNNReal := by
  refine lipschitzWith_iff_dist_le_mul.mpr (fun x y ↦ ?_)
  simpa only [NNReal.coe_one, dist_prod_same_right, one_mul, Real.dist_eq] using
    lipschitzWith_iff_dist_le_mul.mp lipschitzWith_max (x, 0) (y, 0)
Lipschitz Continuity of Nonnegative Part Function: $\text{Lip}_1(\text{toNNReal})$
Informal description
The function $\text{toNNReal} \colon \mathbb{R} \to \mathbb{R}_{\geq 0}$, which maps a real number to its nonnegative part, is Lipschitz continuous with constant $1$.
LipschitzWith.cauchySeq_comp theorem
(hf : LipschitzWith K f) {u : ℕ → α} (hu : CauchySeq u) : CauchySeq (f ∘ u)
Full source 
lemma cauchySeq_comp (hf : LipschitzWith K f) {u : ℕ → α} (hu : CauchySeq u) :
    CauchySeq (f ∘ u) := by
  rcases cauchySeq_iff_le_tendsto_0.1 hu with ⟨b, b_nonneg, hb, blim⟩
  refine cauchySeq_iff_le_tendsto_0.2 ⟨fun n ↦ K * b n, ?_, ?_, ?_⟩
  · exact fun n ↦ mul_nonneg (by positivity) (b_nonneg n)
  · exact fun n m N hn hm ↦ hf.dist_le_mul_of_le (hb n m N hn hm)
  · rw [← mul_zero (K : ℝ)]
    exact blim.const_mul _
Lipschitz Continuous Maps Preserve Cauchy Sequences
Informal description
Let $f : \alpha \to \beta$ be a Lipschitz continuous map between pseudometric spaces with constant $K \geq 0$. If $u : \mathbb{N} \to \alpha$ is a Cauchy sequence in $\alpha$, then the composition $f \circ u : \mathbb{N} \to \beta$ is a Cauchy sequence in $\beta$.
LipschitzWith.max theorem
(hf : LipschitzWith Kf f) (hg : LipschitzWith Kg g) : LipschitzWith (max Kf Kg) fun x => max (f x) (g x)
Full source 
protected theorem max (hf : LipschitzWith Kf f) (hg : LipschitzWith Kg g) :
    LipschitzWith (max Kf Kg) fun x => max (f x) (g x) := by
  simpa only [(· ∘ ·), one_mul] using lipschitzWith_max.comp (hf.prodMk hg)
Lipschitz Continuity of Pointwise Maximum with Constant $\max(K_f, K_g)$
Informal description
Let $f : \alpha \to \mathbb{R}$ and $g : \alpha \to \mathbb{R}$ be Lipschitz continuous functions with constants $K_f$ and $K_g$ respectively. Then the function $x \mapsto \max(f(x), g(x))$ is Lipschitz continuous with constant $\max(K_f, K_g)$.
LipschitzWith.min theorem
(hf : LipschitzWith Kf f) (hg : LipschitzWith Kg g) : LipschitzWith (max Kf Kg) fun x => min (f x) (g x)
Full source 
protected theorem min (hf : LipschitzWith Kf f) (hg : LipschitzWith Kg g) :
    LipschitzWith (max Kf Kg) fun x => min (f x) (g x) := by
  simpa only [(· ∘ ·), one_mul] using lipschitzWith_min.comp (hf.prodMk hg)
Lipschitz continuity of the pointwise minimum of two Lipschitz functions
Informal description
Let $f, g : \alpha \to \mathbb{R}$ be Lipschitz continuous functions with constants $K_f$ and $K_g$ respectively. Then the function $x \mapsto \min(f(x), g(x))$ is Lipschitz continuous with constant $\max(K_f, K_g)$.
LipschitzWith.max_const theorem
(hf : LipschitzWith Kf f) (a : ℝ) : LipschitzWith Kf fun x => max (f x) a
Full source 
theorem max_const (hf : LipschitzWith Kf f) (a : ℝ) : LipschitzWith Kf fun x => max (f x) a := by
  simpa only [max_eq_left (zero_le Kf)] using hf.max (LipschitzWith.const a)
Lipschitz continuity of the pointwise maximum with a constant
Informal description
Let $f : \alpha \to \mathbb{R}$ be a Lipschitz continuous function with constant $K_f$, and let $a \in \mathbb{R}$. Then the function $x \mapsto \max(f(x), a)$ is Lipschitz continuous with the same constant $K_f$.
LipschitzWith.const_max theorem
(hf : LipschitzWith Kf f) (a : ℝ) : LipschitzWith Kf fun x => max a (f x)
Full source 
theorem const_max (hf : LipschitzWith Kf f) (a : ℝ) : LipschitzWith Kf fun x => max a (f x) := by
  simpa only [max_comm] using hf.max_const a
Lipschitz continuity of the pointwise maximum with a constant (symmetric version)
Informal description
Let $f : \alpha \to \mathbb{R}$ be a Lipschitz continuous function with constant $K_f$, and let $a \in \mathbb{R}$. Then the function $x \mapsto \max(a, f(x))$ is Lipschitz continuous with the same constant $K_f$.
LipschitzWith.min_const theorem
(hf : LipschitzWith Kf f) (a : ℝ) : LipschitzWith Kf fun x => min (f x) a
Full source 
theorem min_const (hf : LipschitzWith Kf f) (a : ℝ) : LipschitzWith Kf fun x => min (f x) a := by
  simpa only [max_eq_left (zero_le Kf)] using hf.min (LipschitzWith.const a)
Lipschitz continuity of the pointwise minimum with a constant
Informal description
Let $f : \alpha \to \mathbb{R}$ be a Lipschitz continuous function with constant $K_f$, and let $a \in \mathbb{R}$. Then the function $x \mapsto \min(f(x), a)$ is Lipschitz continuous with the same constant $K_f$.
LipschitzWith.const_min theorem
(hf : LipschitzWith Kf f) (a : ℝ) : LipschitzWith Kf fun x => min a (f x)
Full source 
theorem const_min (hf : LipschitzWith Kf f) (a : ℝ) : LipschitzWith Kf fun x => min a (f x) := by
  simpa only [min_comm] using hf.min_const a
Lipschitz continuity of the pointwise minimum with a constant (symmetric version)
Informal description
Let $f : \alpha \to \mathbb{R}$ be a Lipschitz continuous function with constant $K_f$, and let $a \in \mathbb{R}$. Then the function $x \mapsto \min(a, f(x))$ is Lipschitz continuous with the same constant $K_f$.
LipschitzWith.projIcc theorem
{a b : ℝ} (h : a ≤ b) : LipschitzWith 1 (projIcc a b h)
Full source 
protected theorem projIcc {a b : ℝ} (h : a ≤ b) : LipschitzWith 1 (projIcc a b h) :=
  ((LipschitzWith.id.const_min _).const_max _).subtype_mk _
Lipschitz Continuity of Interval Projection with Constant 1
Informal description
For any real numbers $a$ and $b$ with $a \leq b$, the projection function $\text{projIcc}(a, b, h) : \mathbb{R} \to [a, b]$ is Lipschitz continuous with constant $1$. Here, $\text{projIcc}(a, b, h)$ maps any real number $x$ to $\max(a, \min(b, x))$, ensuring the result lies within the closed interval $[a, b]$.
LipschitzWith.properSpace theorem
{X Y : Type*} [PseudoMetricSpace X] [PseudoMetricSpace Y] [ProperSpace Y] {f : X → Y} (hf : IsProperMap f) {K : ℝ≥0} (hf' : LipschitzWith K f) : ProperSpace X
Full source 
/-- The preimage of a proper space under a Lipschitz proper map is proper. -/
lemma LipschitzWith.properSpace {X Y : Type*} [PseudoMetricSpace X]
    [PseudoMetricSpace Y] [ProperSpace Y] {f : X → Y} (hf : IsProperMap f)
    {K : ℝ≥0} (hf' : LipschitzWith K f) : ProperSpace X :=
  ⟨fun x r ↦ (hf.isCompact_preimage (isCompact_closedBall (f x) (K * r))).of_isClosed_subset
    Metric.isClosed_closedBall (hf'.mapsTo_closedBall x r).subset_preimage⟩
Properness of Domain under Lipschitz Proper Maps
Informal description
Let $X$ and $Y$ be pseudometric spaces, with $Y$ being a proper space. Given a proper map $f \colon X \to Y$ that is Lipschitz continuous with constant $K \geq 0$, the space $X$ is also proper.
LipschitzOnWith.of_dist_le' theorem
{K : ℝ} (h : ∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ K * dist x y) : LipschitzOnWith (Real.toNNReal K) f s
Full source 
protected theorem of_dist_le' {K : ℝ} (h : ∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ K * dist x y) :
    LipschitzOnWith (Real.toNNReal K) f s :=
  of_dist_le_mul fun x hx y hy =>
    le_trans (h x hx y hy) <| by gcongr; apply Real.le_coe_toNNReal
Lipschitz Continuity on a Subset via Distance Inequality
Informal description
Let $s$ be a subset of a pseudometric space $\alpha$, and let $f : \alpha \to \beta$ be a map into another pseudometric space $\beta$. If there exists a real constant $K \geq 0$ such that for all $x, y \in s$, the distance inequality $\text{dist}(f(x), f(y)) \leq K \cdot \text{dist}(x, y)$ holds, then $f$ is Lipschitz continuous on $s$ with constant $K' = \text{Real.toNNReal}(K)$.
LipschitzOnWith.mk_one theorem
(h : ∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ dist x y) : LipschitzOnWith 1 f s
Full source 
protected theorem mk_one (h : ∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ dist x y) :
    LipschitzOnWith 1 f s :=
  of_dist_le_mul <| by simpa only [NNReal.coe_one, one_mul] using h
Lipschitz continuity with constant 1 via distance contraction
Informal description
Let $f : \alpha \to \beta$ be a function between pseudometric spaces, and let $s$ be a subset of $\alpha$. If for all $x, y \in s$ the distance between $f(x)$ and $f(y)$ is less than or equal to the distance between $x$ and $y$, then $f$ is Lipschitz continuous on $s$ with constant $1$.
LipschitzOnWith.of_le_add_mul' theorem
{f : α → ℝ} (K : ℝ) (h : ∀ x ∈ s, ∀ y ∈ s, f x ≤ f y + K * dist x y) : LipschitzOnWith (Real.toNNReal K) f s
Full source 
/-- For functions to `ℝ`, it suffices to prove `f x ≤ f y + K * dist x y`; this version
doesn't assume `0≤K`. -/
protected theorem of_le_add_mul' {f : α → ℝ} (K : ℝ)
    (h : ∀ x ∈ s, ∀ y ∈ s, f x ≤ f y + K * dist x y) : LipschitzOnWith (Real.toNNReal K) f s :=
  have I : ∀ x ∈ s, ∀ y ∈ s, f x - f y ≤ K * dist x y := fun x hx y hy =>
    sub_le_iff_le_add'.2 (h x hx y hy)
  LipschitzOnWith.of_dist_le' fun x hx y hy =>
    abs_sub_le_iff.2 ⟨I x hx y hy, dist_comm y x ▸ I y hy x hx⟩
Lipschitz continuity via one-sided distance inequality
Informal description
Let $f : \alpha \to \mathbb{R}$ be a function defined on a pseudometric space $\alpha$, and let $s$ be a subset of $\alpha$. If there exists a real constant $K$ such that for all $x, y \in s$, the inequality $f(x) \leq f(y) + K \cdot \text{dist}(x, y)$ holds, then $f$ is Lipschitz continuous on $s$ with constant $\text{Real.toNNReal}(K)$.
LipschitzOnWith.of_le_add_mul theorem
{f : α → ℝ} (K : ℝ≥0) (h : ∀ x ∈ s, ∀ y ∈ s, f x ≤ f y + K * dist x y) : LipschitzOnWith K f s
Full source 
/-- For functions to `ℝ`, it suffices to prove `f x ≤ f y + K * dist x y`; this version
assumes `0≤K`. -/
protected theorem of_le_add_mul {f : α → ℝ} (K : ℝ≥0)
    (h : ∀ x ∈ s, ∀ y ∈ s, f x ≤ f y + K * dist x y) : LipschitzOnWith K f s := by
  simpa only [Real.toNNReal_coe] using LipschitzOnWith.of_le_add_mul' K h
Lipschitz continuity via one-sided linear growth bound
Informal description
Let $f : \alpha \to \mathbb{R}$ be a function defined on a pseudometric space $\alpha$, and let $s \subseteq \alpha$. If there exists a non-negative real constant $K$ such that for all $x, y \in s$, the inequality $f(x) \leq f(y) + K \cdot \text{dist}(x, y)$ holds, then $f$ is Lipschitz continuous on $s$ with constant $K$.
LipschitzOnWith.of_le_add theorem
{f : α → ℝ} (h : ∀ x ∈ s, ∀ y ∈ s, f x ≤ f y + dist x y) : LipschitzOnWith 1 f s
Full source 
protected theorem of_le_add {f : α → ℝ} (h : ∀ x ∈ s, ∀ y ∈ s, f x ≤ f y + dist x y) :
    LipschitzOnWith 1 f s :=
  LipschitzOnWith.of_le_add_mul 1 <| by simpa only [NNReal.coe_one, one_mul]
Lipschitz continuity via additive distance bound with constant 1
Informal description
Let $f : \alpha \to \mathbb{R}$ be a function defined on a pseudometric space $\alpha$, and let $s \subseteq \alpha$. If for all $x, y \in s$, the inequality $f(x) \leq f(y) + \text{dist}(x, y)$ holds, then $f$ is Lipschitz continuous on $s$ with constant $1$.
LipschitzOnWith.le_add_mul theorem
{f : α → ℝ} {K : ℝ≥0} (h : LipschitzOnWith K f s) {x : α} (hx : x ∈ s) {y : α} (hy : y ∈ s) : f x ≤ f y + K * dist x y
Full source 
protected theorem le_add_mul {f : α → ℝ} {K : ℝ≥0} (h : LipschitzOnWith K f s) {x : α} (hx : x ∈ s)
    {y : α} (hy : y ∈ s) : f x ≤ f y + K * dist x y :=
  sub_le_iff_le_add'.1 <| le_trans (le_abs_self _) <| h.dist_le_mul x hx y hy
Lipschitz Condition Implies Linear Growth Bound on a Set
Informal description
Let $f : \alpha \to \mathbb{R}$ be a function defined on a pseudometric space $\alpha$, and let $s \subseteq \alpha$. If $f$ is Lipschitz continuous on $s$ with constant $K \geq 0$, then for any $x, y \in s$, we have $f(x) \leq f(y) + K \cdot d(x, y)$, where $d$ is the distance function on $\alpha$.
LipschitzOnWith.iff_le_add_mul theorem
{f : α → ℝ} {K : ℝ≥0} : LipschitzOnWith K f s ↔ ∀ x ∈ s, ∀ y ∈ s, f x ≤ f y + K * dist x y
Full source 
protected theorem iff_le_add_mul {f : α → ℝ} {K : ℝ≥0} :
    LipschitzOnWithLipschitzOnWith K f s ↔ ∀ x ∈ s, ∀ y ∈ s, f x ≤ f y + K * dist x y :=
  ⟨LipschitzOnWith.le_add_mul, LipschitzOnWith.of_le_add_mul K⟩
Lipschitz Continuity on a Set via One-Sided Linear Growth Bound
Informal description
Let $f : \alpha \to \mathbb{R}$ be a function defined on a pseudometric space $\alpha$, and let $s \subseteq \alpha$ be a subset. For any non-negative real constant $K$, the function $f$ is Lipschitz continuous on $s$ with constant $K$ if and only if for all $x, y \in s$, the inequality $f(x) \leq f(y) + K \cdot d(x, y)$ holds, where $d$ is the distance function on $\alpha$.
LipschitzOnWith.isBounded_image2 theorem
(f : α → β → γ) {K₁ K₂ : ℝ≥0} {s : Set α} {t : Set β} (hs : Bornology.IsBounded s) (ht : Bornology.IsBounded t) (hf₁ : ∀ b ∈ t, LipschitzOnWith K₁ (fun a => f a b) s) (hf₂ : ∀ a ∈ s, LipschitzOnWith K₂ (f a) t) : Bornology.IsBounded (Set.image2 f s t)
Full source 
theorem isBounded_image2 (f : α → β → γ) {K₁ K₂ : ℝ≥0} {s : Set α} {t : Set β}
    (hs : Bornology.IsBounded s) (ht : Bornology.IsBounded t)
    (hf₁ : ∀ b ∈ t, LipschitzOnWith K₁ (fun a => f a b) s)
    (hf₂ : ∀ a ∈ s, LipschitzOnWith K₂ (f a) t) : Bornology.IsBounded (Set.image2 f s t) :=
  Metric.isBounded_iff_ediam_ne_top.2 <|
    ne_top_of_le_ne_top
      (ENNReal.add_ne_top.mpr
        ⟨ENNReal.mul_ne_top ENNReal.coe_ne_top hs.ediam_ne_top,
          ENNReal.mul_ne_top ENNReal.coe_ne_top ht.ediam_ne_top⟩)
      (ediam_image2_le _ _ _ hf₁ hf₂)
Boundedness of Image under Lipschitz Continuous Binary Function on Bounded Domains
Informal description
Let $f : \alpha \times \beta \to \gamma$ be a function between pseudometric spaces, and let $s \subseteq \alpha$ and $t \subseteq \beta$ be bounded subsets. Suppose that for every $b \in t$, the function $f(\cdot, b)$ is Lipschitz continuous on $s$ with constant $K_1 \geq 0$, and for every $a \in s$, the function $f(a, \cdot)$ is Lipschitz continuous on $t$ with constant $K_2 \geq 0$. Then the image $\{f(a, b) \mid a \in s, b \in t\}$ is a bounded subset of $\gamma$.
LipschitzOnWith.cauchySeq_comp theorem
(hf : LipschitzOnWith K f s) {u : ℕ → α} (hu : CauchySeq u) (h'u : range u ⊆ s) : CauchySeq (f ∘ u)
Full source 
lemma cauchySeq_comp (hf : LipschitzOnWith K f s)
    {u : ℕ → α} (hu : CauchySeq u) (h'u : rangerange u ⊆ s) :
    CauchySeq (f ∘ u) := by
  rcases cauchySeq_iff_le_tendsto_0.1 hu with ⟨b, b_nonneg, hb, blim⟩
  refine cauchySeq_iff_le_tendsto_0.2 ⟨fun n ↦ K * b n, ?_, ?_, ?_⟩
  · exact fun n ↦ mul_nonneg (by positivity) (b_nonneg n)
  · intro n m N hn hm
    have A n : u n ∈ s := h'u (mem_range_self _)
    apply (hf.dist_le_mul _ (A n) _ (A m)).trans
    exact mul_le_mul_of_nonneg_left (hb n m N hn hm) K.2
  · rw [← mul_zero (K : ℝ)]
    exact blim.const_mul _
Preservation of Cauchy Sequences under Lipschitz Continuous Maps on Restricted Domains
Informal description
Let $f : \alpha \to \beta$ be a function that is Lipschitz continuous on a set $s \subseteq \alpha$ with constant $K \geq 0$. If $u : \mathbb{N} \to \alpha$ is a Cauchy sequence whose range is contained in $s$, then the composition $f \circ u : \mathbb{N} \to \beta$ is also a Cauchy sequence.
LocallyLipschitz.min theorem
(hf : LocallyLipschitz f) (hg : LocallyLipschitz g) : LocallyLipschitz (fun x => min (f x) (g x))
Full source 
/-- The minimum of locally Lipschitz functions is locally Lipschitz. -/
protected lemma min (hf : LocallyLipschitz f) (hg : LocallyLipschitz g) :
    LocallyLipschitz (fun x => min (f x) (g x)) :=
  lipschitzWith_min.locallyLipschitz.comp (hf.prodMk hg)
Local Lipschitz Continuity of the Minimum of Two Locally Lipschitz Functions
Informal description
If $f$ and $g$ are locally Lipschitz continuous functions from a metric space $\alpha$ to $\mathbb{R}$, then the function $x \mapsto \min(f(x), g(x))$ is also locally Lipschitz continuous.
LocallyLipschitz.max theorem
(hf : LocallyLipschitz f) (hg : LocallyLipschitz g) : LocallyLipschitz (fun x => max (f x) (g x))
Full source 
/-- The maximum of locally Lipschitz functions is locally Lipschitz. -/
protected lemma max (hf : LocallyLipschitz f) (hg : LocallyLipschitz g) :
    LocallyLipschitz (fun x => max (f x) (g x)) :=
  lipschitzWith_max.locallyLipschitz.comp (hf.prodMk hg)
Local Lipschitz continuity is preserved under pointwise maximum
Informal description
If $f$ and $g$ are locally Lipschitz continuous functions from a metric space $\alpha$ to $\mathbb{R}$, then the function $x \mapsto \max(f(x), g(x))$ is also locally Lipschitz continuous.
LocallyLipschitz.max_const theorem
(hf : LocallyLipschitz f) (a : ℝ) : LocallyLipschitz fun x => max (f x) a
Full source 
theorem max_const (hf : LocallyLipschitz f) (a : ℝ) : LocallyLipschitz fun x => max (f x) a :=
  hf.max (LocallyLipschitz.const a)
Local Lipschitz continuity of the pointwise maximum with a constant
Informal description
If $f$ is a locally Lipschitz continuous function from a metric space $\alpha$ to $\mathbb{R}$, then for any real number $a$, the function $x \mapsto \max(f(x), a)$ is also locally Lipschitz continuous.
LocallyLipschitz.const_max theorem
(hf : LocallyLipschitz f) (a : ℝ) : LocallyLipschitz fun x => max a (f x)
Full source 
theorem const_max (hf : LocallyLipschitz f) (a : ℝ) : LocallyLipschitz fun x => max a (f x) := by
  simpa [max_comm] using (hf.max_const a)
Local Lipschitz continuity of the pointwise maximum with a constant function
Informal description
If $f \colon \alpha \to \mathbb{R}$ is a locally Lipschitz continuous function from a metric space $\alpha$ to the real numbers, then for any real number $a$, the function $x \mapsto \max(a, f(x))$ is also locally Lipschitz continuous.
LocallyLipschitz.min_const theorem
(hf : LocallyLipschitz f) (a : ℝ) : LocallyLipschitz fun x => min (f x) a
Full source 
theorem min_const (hf : LocallyLipschitz f) (a : ℝ) : LocallyLipschitz fun x => min (f x) a :=
  hf.min (LocallyLipschitz.const a)
Local Lipschitz Continuity of Minimum with Constant Function
Informal description
If $f$ is a locally Lipschitz continuous function from a metric space $\alpha$ to $\mathbb{R}$, then for any real number $a$, the function $x \mapsto \min(f(x), a)$ is also locally Lipschitz continuous.
LocallyLipschitz.const_min theorem
(hf : LocallyLipschitz f) (a : ℝ) : LocallyLipschitz fun x => min a (f x)
Full source 
theorem const_min (hf : LocallyLipschitz f) (a : ℝ) : LocallyLipschitz fun x => min a (f x) := by
  simpa [min_comm] using (hf.min_const a)
Local Lipschitz Continuity of Minimum with Constant Function (Symmetric Version)
Informal description
If $f \colon \alpha \to \mathbb{R}$ is a locally Lipschitz continuous function from a metric space $\alpha$ to $\mathbb{R}$, then for any real number $a$, the function $x \mapsto \min(a, f(x))$ is also locally Lipschitz continuous.
continuousAt_of_locally_lipschitz theorem
{x : α} {r : ℝ} (hr : 0 < r) (K : ℝ) (h : ∀ y, dist y x < r → dist (f y) (f x) ≤ K * dist y x) : ContinuousAt f x
Full source 
/-- If a function is locally Lipschitz around a point, then it is continuous at this point. -/
theorem continuousAt_of_locally_lipschitz {x : α} {r : ℝ} (hr : 0 < r) (K : ℝ)
    (h : ∀ y, dist y x < r → dist (f y) (f x) ≤ K * dist y x) : ContinuousAt f x := by
  -- We use `h` to squeeze `dist (f y) (f x)` between `0` and `K * dist y x`
  refine tendsto_iff_dist_tendsto_zero.2 (squeeze_zero' (Eventually.of_forall fun _ => dist_nonneg)
    (mem_of_superset (ball_mem_nhds _ hr) h) ?_)
  -- Then show that `K * dist y x` tends to zero as `y → x`
  refine (continuous_const.mul (continuous_id.dist continuous_const)).tendsto' _ _ ?_
  simp
Local Lipschitz Condition Implies Continuity at a Point
Informal description
Let $f \colon \alpha \to \beta$ be a function between pseudometric spaces, and let $x \in \alpha$. If there exists $r > 0$ and $K \geq 0$ such that for all $y \in \alpha$ with $\text{dist}(y, x) < r$, the inequality $\text{dist}(f(y), f(x)) \leq K \cdot \text{dist}(y, x)$ holds, then $f$ is continuous at $x$.
LipschitzOnWith.extend_real theorem
{f : α → ℝ} {s : Set α} {K : ℝ≥0} (hf : LipschitzOnWith K f s) : ∃ g : α → ℝ, LipschitzWith K g ∧ EqOn f g s
Full source 
/-- A function `f : α → ℝ` which is `K`-Lipschitz on a subset `s` admits a `K`-Lipschitz extension
to the whole space. -/
theorem LipschitzOnWith.extend_real {f : α → ℝ} {s : Set α} {K : ℝ≥0} (hf : LipschitzOnWith K f s) :
    ∃ g : α → ℝ, LipschitzWith K g ∧ EqOn f g s := by
  /- An extension is given by `g y = Inf {f x + K * dist y x | x ∈ s}`. Taking `x = y`, one has
    `g y ≤ f y` for `y ∈ s`, and the other inequality holds because `f` is `K`-Lipschitz, so that it
    can not counterbalance the growth of `K * dist y x`. One readily checks from the formula that
    the extended function is also `K`-Lipschitz. -/
  rcases eq_empty_or_nonempty s with (rfl | hs)
  · exact ⟨fun _ => 0, (LipschitzWith.const _).weaken (zero_le _), eqOn_empty _ _⟩
  have : Nonempty s := by simp only [hs, nonempty_coe_sort]
  let g := fun y : α => iInf fun x : s => f x + K * dist y x
  have B : ∀ y : α, BddBelow (range fun x : s => f x + K * dist y x) := fun y => by
    rcases hs with ⟨z, hz⟩
    refine ⟨f z - K * dist y z, ?_⟩
    rintro w ⟨t, rfl⟩
    dsimp
    rw [sub_le_iff_le_add, add_assoc, ← mul_add, add_comm (dist y t)]
    calc
      f z ≤ f t + K * dist z t := hf.le_add_mul hz t.2
      _ ≤ f t + K * (dist y z + dist y t) := by gcongr; apply dist_triangle_left
  have E : EqOn f g s := fun x hx => by
    refine le_antisymm (le_ciInf fun y => hf.le_add_mul hx y.2) ?_
    simpa only [add_zero, Subtype.coe_mk, mul_zero, dist_self] using ciInf_le (B x) ⟨x, hx⟩
  refine ⟨g, LipschitzWith.of_le_add_mul K fun x y => ?_, E⟩
  rw [← sub_le_iff_le_add]
  refine le_ciInf fun z => ?_
  rw [sub_le_iff_le_add]
  calc
    g x ≤ f z + K * dist x z := ciInf_le (B x) _
    _ ≤ f z + K * dist y z + K * dist x y := by
      rw [add_assoc, ← mul_add, add_comm (dist y z)]
      gcongr
      apply dist_triangle
Lipschitz Extension Theorem for Real-Valued Functions on Metric Spaces
Informal description
Let $\alpha$ be a pseudometric space, $s \subseteq \alpha$ a subset, and $f : s \to \mathbb{R}$ a $K$-Lipschitz function on $s$ (i.e., $|f(x) - f(y)| \leq K \cdot d(x,y)$ for all $x, y \in s$). Then there exists a $K$-Lipschitz function $g : \alpha \to \mathbb{R}$ that extends $f$, meaning $g(x) = f(x)$ for all $x \in s$.
LipschitzOnWith.extend_pi theorem
[Fintype ι] {f : α → ι → ℝ} {s : Set α} {K : ℝ≥0} (hf : LipschitzOnWith K f s) : ∃ g : α → ι → ℝ, LipschitzWith K g ∧ EqOn f g s
Full source 
/-- A function `f : α → (ι → ℝ)` which is `K`-Lipschitz on a subset `s` admits a `K`-Lipschitz
extension to the whole space. The same result for the space `ℓ^∞ (ι, ℝ)` over a possibly infinite
type `ι` is implemented in `LipschitzOnWith.extend_lp_infty`. -/
theorem LipschitzOnWith.extend_pi [Fintype ι] {f : α → ι → ℝ} {s : Set α}
    {K : ℝ≥0} (hf : LipschitzOnWith K f s) : ∃ g : α → ι → ℝ, LipschitzWith K g ∧ EqOn f g s := by
  have : ∀ i, ∃ g : α → ℝ, LipschitzWith K g ∧ EqOn (fun x => f x i) g s := fun i => by
    have : LipschitzOnWith K (fun x : α => f x i) s :=
      LipschitzOnWith.of_dist_le_mul fun x hx y hy =>
        (dist_le_pi_dist _ _ i).trans (hf.dist_le_mul x hx y hy)
    exact this.extend_real
  choose g hg using this
  refine ⟨fun x i => g i x, LipschitzWith.of_dist_le_mul fun x y => ?_, fun x hx ↦ ?_⟩
  · exact (dist_pi_le_iff (mul_nonneg K.2 dist_nonneg)).2 fun i => (hg i).1.dist_le_mul x y
  · ext1 i
    exact (hg i).2 hx
Lipschitz Extension Theorem for Finite-Dimensional Real-Valued Functions on Metric Spaces
Informal description
Let $\alpha$ be a pseudometric space, $s \subseteq \alpha$ a subset, and $f : s \to \mathbb{R}^\iota$ a $K$-Lipschitz function on $s$ (i.e., $\text{dist}(f(x), f(y)) \leq K \cdot \text{dist}(x, y)$ for all $x, y \in s$), where $\iota$ is a finite index set. Then there exists a $K$-Lipschitz function $g : \alpha \to \mathbb{R}^\iota$ that extends $f$, meaning $g(x) = f(x)$ for all $x \in s$.