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)