hausdorffDist_zero_iff_closure_eq_closure

English

If the Hausdorff distance between sets S and T is finite, then the distance is zero exactly when their closures coincide.

Русский

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

LaTeX

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

Lean4

/-- Two sets are at zero Hausdorff distance if and only if they have the same closures. -/
theorem hausdorffDist_zero_iff_closure_eq_closure (fin : hausdorffEdist s t ≠ ⊤) :
    hausdorffDist s t = 0 ↔ closure s = closure t := by
  simp [← hausdorffEdist_zero_iff_closure_eq_closure, hausdorffDist, ENNReal.toReal_eq_zero_iff, fin]

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