hausdorffDist_empty' — Mathlib

English

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

Русский

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

LaTeX

$$$\operatorname{hausdorffDist}(\varnothing,s)=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 simp [hausdorffDist_comm]

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