edist_le_mul_of_le — Mathlib

English

If h is LipschitzOnWith K f s, then for x,y ∈ s and r with edist x y ≤ r, we have edist(f x) (f y) ≤ K · r.

Русский

Если h = LipschitzOnWith K f s, то для x,y ∈ s и r ≥ edist x y: edist(f x) (f y) ≤ K · r.

LaTeX

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

Lean4

theorem edist_le_mul_of_le (h : LipschitzOnWith K f s) {x y : α} (hx : x ∈ s) (hy : y ∈ s) {r : ℝ≥0∞}
    (hr : edist x y ≤ r) : edist (f x) (f y) ≤ K * r :=
  (h hx hy).trans <| mul_right_mono hr

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