dist_right

Mathlib.Topology.MetricSpace.Lipschitz

URI: https://scilib.ai/kg/mathlib#LipschitzWith.dist_right

English

For any x, the map t ↦ dist(t, x) is 1-Lipschitz.

Русский

Для фиксированной x функция t ↦ dist(t, x) является 1-L Lipschitz.

LaTeX

$$$\\text{LipschitzWith}(1,\\, \\lambda t. \\operatorname{dist}(t, x))$$$

Lean4

protected theorem dist_right (x : α) : LipschitzWith 1 (dist x) :=
  LipschitzWith.of_le_add fun _ _ => dist_triangle_right _ _ _

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

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

Разделы

Аффилиация

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