hausdorffDist_closure — Mathlib

English

For any sets S and T in a metric space, the Hausdorff distance between closures equals the distance between the original sets.

Русский

Для любых множеств S и T в метрическом пространстве расстояние Хаусдорфа между их замыканиями равно расстоянию между самими множествами.

LaTeX

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

Lean4

/-- The Hausdorff distances between two sets and their closures coincide. -/
theorem hausdorffDist_closure : hausdorffDist (closure s) (closure t) = hausdorffDist s t := by simp [hausdorffDist]

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