dist_lt_mul_of_lt — Mathlib

English

For a Lipschitz f, the distance between f(x) and f(y) is bounded by K times the distance between x and y, for all x,y.

Русский

Для Lipschitz-функции неравенство расстояний: dist(f(x),f(y)) ≤ K dist(x,y).

LaTeX

$$$\operatorname{dist}(f(x),f(y)) \le K \cdot \operatorname{dist}(x,y)$$$

Lean4

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 <| by gcongr

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