lipschitz_infDist_set — Mathlib

English

Fix a point x in α. The map sending a nonempty compact s to infDist(x, s) is 1-Lipschitz with respect to the Hausdorff metric on NonemptyCompacts α.

Русский

Пусть фиксировано x ∈ α. Отображение s ↦ infDist(x, s) на множество непустых компактных подмножеств α является 1- Lipschitz относительно расстояния Хаусдорфа между множествами.

LaTeX

$$$\operatorname{LipschitzWith}\,1\, (\lambda s:\mathrm{NonemptyCompacts}\,\alpha.\; \operatorname{infDist} x\, s)$$$

Lean4

theorem lipschitz_infDist_set (x : α) : LipschitzWith 1 fun s : NonemptyCompacts α => infDist x s :=
  LipschitzWith.of_le_add fun s t => by
    rw [dist_comm]
    exact infDist_le_infDist_add_hausdorffDist (edist_ne_top t s)

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