antilipschitz

Mathlib.Analysis.Normed.Affine.Isometry

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

English

There exists an antilipschitz bound 1 for f, i.e., inverse of Lipschitz property.

Русский

Существует антип Lipschitz-ограничение 1 для f.

LaTeX

$$$\text{AntilipschitzWith } 1\ f$$$

Lean4

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

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

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

Разделы

Аффилиация

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