uniformContinuous_infDist_Hausdorff_dist

English

The map p ↦ infDist p.1 p.2 from α × NonemptyCompacts α to ℝ is uniformly continuous.

Русский

Отображение p ↦ infDist p.1 p.2 из α × NonemptyCompacts α в ℝ является uniformly continuous.

LaTeX

$$$\text{UniformContinuous}\, (\lambda p:\alpha \times \mathrm{NonemptyCompacts}\, \alpha.\; \operatorname{infDist} p.1 p.2)$$$

Lean4

theorem uniformContinuous_infDist_Hausdorff_dist :
    UniformContinuous fun p : α × NonemptyCompacts α => infDist p.1 p.2 :=
  lipschitz_infDist.uniformContinuous

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