antilipschitzWith_iff_le_mul_nndist

English

An AntilipschitzWith map is equivalent to a pointwise nndist comparison with the image, i.e., nndist ≤ K times nndist of image.

Русский

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

LaTeX

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

Lean4

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

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