English
The map p ↦ infDist p.fst p.snd on α × NonemptyCompacts α is 2-Lipschitz.
Русский
Отображение p ↦ infDist(первый компонент p, второй компонент p) на произведении α × NonemptyCompacts α является 2-Lipschitz.
LaTeX
$$$\operatorname{LipschitzWith}\,2\, (\lambda p: \alpha \times \mathrm{NonemptyCompacts}\, \alpha. \operatorname{infDist} p.1 p.2)$$$
Lean4
theorem lipschitz_infDist : LipschitzWith 2 fun p : α × NonemptyCompacts α => infDist p.1 p.2 :=
by
rw [← one_add_one_eq_two]
exact LipschitzWith.uncurry (fun s : NonemptyCompacts α => lipschitz_infDist_pt (s : Set α)) lipschitz_infDist_set