hausdorffEdist_empty — Mathlib

English

The Hausdorff distance from a nonempty set to the empty set is infinite.

Русский

Расстояние Хаусдорфа от непустого множества до пустого равно бесконечности.

LaTeX

$$$ \operatorname{hausdorffEdist}(s, \varnothing) = \infty $$$

Lean4

/-- The Hausdorff edistance to the empty set is infinite. -/
theorem hausdorffEdist_empty (ne : s.Nonempty) : hausdorffEdist s ∅ = ∞ :=
  by
  rcases ne with ⟨x, xs⟩
  have : infEdist x ∅ ≤ hausdorffEdist s ∅ := infEdist_le_hausdorffEdist_of_mem xs
  simpa using this

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