hausdorffEdist_zero_iff_closure_eq_closure

English

The Hausdorff edistance between s and t is zero if and only if the closures of s and t are equal.

Русский

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

LaTeX

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

Lean4

/-- Two sets are at zero Hausdorff edistance if and only if they have the same closure. -/
theorem hausdorffEdist_zero_iff_closure_eq_closure : hausdorffEdist s t = 0 ↔ closure s = closure t := by
  simp only [hausdorffEdist_def, ENNReal.sup_eq_zero, ENNReal.iSup_eq_zero, ← subset_def,
    ← mem_closure_iff_infEdist_zero, subset_antisymm_iff, isClosed_closure.closure_subset_iff]

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