hausdorffDist_zero_iff_eq — Mathlib

English

Let S and T be closed subsets with finite Hausdorff distance. Then the distance is zero if and only if S = T.

Русский

Пусть S и T — замкнутые множества с конечной дистанцией Хаусдорфа. Тогда расстояние равно нулю тогда и только тогда, когда S = T.

LaTeX

$$$\\operatorname{hausdorffDist}(s, t) = 0 \\iff s = t \\quad\\text{(when } s,t\\text{ are closed and finite distance).}$$$

Lean4

/-- Two closed sets are at zero Hausdorff distance if and only if they coincide. -/
theorem _root_.IsClosed.hausdorffDist_zero_iff_eq (hs : IsClosed s) (ht : IsClosed t) (fin : hausdorffEdist s t ≠ ⊤) :
    hausdorffDist s t = 0 ↔ s = t := by
  simp [← hausdorffEdist_zero_iff_eq_of_closed hs ht, hausdorffDist, ENNReal.toReal_eq_zero_iff, fin]

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