id

Mathlib.Topology.MetricSpace.Antilipschitz

URI: https://scilib.ai/kg/mathlib#AntilipschitzWith.id

English

The diameter of preimage of a set is bounded by K times the diameter of the set.

Русский

Диаметр прообраза множества ограничен диагиентом на K раз диаметр самого множества.

LaTeX

$$$\\operatorname{diam}(f^{-1}(s)) \\le K \\cdot \\operatorname{diam}(s)$$$

Lean4

protected theorem id : AntilipschitzWith 1 (id : α → α) := fun x y => by
  simp only [ENNReal.coe_one, one_mul, id, le_refl]

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

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

Разделы

Аффилиация

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