antilipschitz

Mathlib.Topology.MetricSpace.Isometry

URI: https://scilib.ai/kg/mathlib#Isometry.antilipschitz

English

An isometric action of M on X induces isometric translations on Additive M.

Русский

Изометрическое действие M на X индуцирует изометрические преобразования на Additive M.

LaTeX

$$$IsometricVAdd (Additive M) X$$$

Lean4

theorem antilipschitz (h : Isometry f) : AntilipschitzWith 1 f := fun x y => by
  simp only [h x y, ENNReal.coe_one, one_mul, le_refl]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru