antilipschitz — Mathlib

English

Let e be a linear isometry between normed spaces. Then e is 1-antilipschitz, hence it is distance-decreasing from below: there exists c=1 such that for all x,y, ||e x − e y|| ≥ ||x − y|| (in fact equality holds).

Русский

Пусть e — линейное изометрическое отображение между нормированными пространствами. Тогда оно антилипшицево с коэффициентом 1: для всех x,y выполняется ||e x − e y|| ≥ ||x − y|| (на самом деле равенство).

LaTeX

$$$\forall x,y\in E:\; \|e x - e y\| \geq \|x - y\|$$$

Lean4

protected theorem antilipschitz : AntilipschitzWith 1 e :=
  e.isometry.antilipschitz

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