dist_le_mul — Mathlib

English

For a contraction f with constant K, the distance between images does not exceed K times the distance between arguments: dist(f x, f y) ≤ K · dist(x, y).

Русский

Для отображения с сжатием коэффициентом K выполняется неравенство 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_le_mul (x y : α) : dist (f x) (f y) ≤ K * dist x y :=
  hf.toLipschitzWith.dist_le_mul x y

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