antilipschitz — Mathlib

English

If f is an isometry between extended metric spaces, then f is 1-antilipschitz; equivalently, for all x, y, distance does not shrink: dist(f(x), f(y)) ≥ dist(x, y).

Русский

Пусть f — изометрия между расширенными метрическими пространствами; тогда f является 1-антиллипшицевым отображением, то есть для любых x,y выполняется d(f(x), f(y)) ≥ d(x, y).

LaTeX

$$$\\forall x,y, \\\\operatorname{dist}(f x, f y) \\\\ge \\\\operatorname{dist}(x,y)$$$

Lean4

protected theorem antilipschitz : AntilipschitzWith 1 f :=
  (IsometryClass.isometry f).antilipschitz

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