edist_lt_of_edist_lt_div — Mathlib

English

For a LipschitzWith K f, edist(f x, f y) ≤ K · edist(x,y) for all x,y.

Русский

Для LipschitzWith K f верно edist(f x, f y) ≤ K · edist(x,y) для всех x,y.

LaTeX

$$$\forall x,y,\ edist(f(x),f(y)) \le K \cdot edist(x,y)$$$

Lean4

theorem edist_lt_of_edist_lt_div (hf : LipschitzWith K f) {x y : α} {d : ℝ≥0∞} (h : edist x y < d / K) :
    edist (f x) (f y) < d :=
  calc
    edist (f x) (f y) ≤ K * edist x y := hf x y
    _ < d := ENNReal.mul_lt_of_lt_div' h

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