lipschitz_infDist — Mathlib

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

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