hausdorffEdist_zero_iff_eq_of_closed

English

If s and t are closed and their Hausdorff distance is zero, then s = t.

Русский

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

LaTeX

$$$ \operatorname{hausdorffEdist}(s,t) = 0 \Rightarrow s = t \text{, при } IsClosed(s) \text{ и } IsClosed(t) $$$

Lean4

/-- Two closed sets are at zero Hausdorff edistance if and only if they coincide. -/
theorem hausdorffEdist_zero_iff_eq_of_closed (hs : IsClosed s) (ht : IsClosed t) : hausdorffEdist s t = 0 ↔ s = t := by
  rw [hausdorffEdist_zero_iff_closure_eq_closure, hs.closure_eq, ht.closure_eq]

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