hausdorffDist_self_closure — Mathlib

English

The Hausdorff distance between a set and its closure is zero: hausdorffDist(s, closure(s)) = 0.

Русский

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

LaTeX

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

Lean4

/-- The Hausdorff distance between a set and its closure vanishes. -/
@[simp]
theorem hausdorffDist_self_closure : hausdorffDist s (closure s) = 0 := by simp [hausdorffDist]

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