dist_left

Mathlib.Topology.MetricSpace.Lipschitz

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

English

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

Русский

Функция x ↦ dist(x, y) для фиксированного y является 1- Lipschitz.

LaTeX

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

Lean4

protected theorem dist_left (y : α) : LipschitzWith 1 (dist · y) :=
  LipschitzWith.mk_one fun _ _ => dist_dist_dist_le_left _ _ _

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

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

Разделы

Аффилиация

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