no goals
ι : Sort ?u.54522
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t u : Set α
Φ : α → β
hs : IsClosed s
ht : IsClosed t
⊢ hausdorffEdist s t = 0 ↔ s = t
rw [hausdorffEdist_zero_iff_closure_eq_closure, hs.closure_eq, ht.closure_eq]