edist_lt_of_edist_lt_div — Mathlib

English

If f is K-Lipschitz on s, and x,y ∈ s with edist x y < d / K, then edist (f x) (f y) < d.

Русский

Если f липшицево на s с константой K и x,y ∈ s такие, что edist x y < d / K, то edist(f x) (f y) < d.

LaTeX

$$$\\text{LipschitzOnWith } K f s \\Rightarrow \\forall x,y\\in s,\\ \\operatorname{edist}(x,y) < d/K \\Rightarrow \\operatorname{edist}(f x, f y) < d$$$

Lean4

theorem edist_lt_of_edist_lt_div (hf : LipschitzOnWith K f s) {x y : α} (hx : x ∈ s) (hy : y ∈ s) {d : ℝ≥0∞}
    (hd : edist x y < d / K) : edist (f x) (f y) < d :=
  hf.to_restrict.edist_lt_of_edist_lt_div <| show edist (⟨x, hx⟩ : s) ⟨y, hy⟩ < d / K from hd

Похожие утверждения