hausdorffDist_empty — Mathlib

English

The Hausdorff distance to the empty set vanishes: hausdorffDist(s, ∅) = 0.

Русский

Расстояние Хаусдорфа до пустого множества равно нулю: hausdorffDist(s, ∅) = 0.

LaTeX

$$$\operatorname{hausdorffDist}(s,\varnothing)=0.$$$

Lean4

/-- The Hausdorff distance to the empty set vanishes (if you want to have the more reasonable
value `∞` instead, use `EMetric.hausdorffEdist`, which takes values in `ℝ≥0∞`). -/
@[simp]
theorem hausdorffDist_empty : hausdorffDist s ∅ = 0 :=
  by
  rcases s.eq_empty_or_nonempty with h | h
  · simp [h]
  · simp [hausdorffDist, hausdorffEdist_empty h]

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