antilipschitzWith_iff_le_mul_dist

English

An AntilipschitzWith map is equivalent to a pointwise dist inequality: dist(x,y) ≤ K dist(f x, f y).

Русский

Антилипшицево отображение эквивалентно неравенству по dist: dist(x,y) ≤ K dist(f x, f y).

LaTeX

$$$AntilipschitzWith(K,f) \\iff \\forall x,y,\\ dist(x,y) \\le K \\cdot dist(f x, f y)$$$

Lean4

theorem antilipschitzWith_iff_le_mul_dist : AntilipschitzWith K f ↔ ∀ x y, dist x y ≤ K * dist (f x) (f y) :=
  by
  simp only [antilipschitzWith_iff_le_mul_nndist, dist_nndist]
  norm_cast

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