lipschitz

Mathlib.Analysis.Normed.Affine.Isometry

URI: https://scilib.ai/kg/mathlib#AffineIsometryEquiv.lipschitz

English

AffineIsometryEquiv is 1-Lipschitz with respect to the underlying metric.

Русский

Аффинная изометрия образует 1-Липшицеву функцию по базовой метрике.

LaTeX

$$$\mathrm{LipschitzWith}_{1}(e)$$$

Lean4

protected theorem lipschitz : LipschitzWith 1 e :=
  e.isometry.lipschitz

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

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

Разделы

Аффилиация

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