no goals
ι : Sort ?u.51836
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t u : Set α
Φ : α → β
⊢ hausdorffEdist s (closure s) = 0
rw [hausdorffEdist_zero_iff_closure_eq_closure, closure_closure]