hausdorffEdist_closure — Mathlib

English

The distance between two sets equals the distance between their closures.

Русский

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

LaTeX

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

Lean4

/-- The Hausdorff edistance between sets or their closures is the same. -/
theorem hausdorffEdist_closure : hausdorffEdist (closure s) (closure t) = hausdorffEdist s t := by simp

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