no goals
ι : Sort ?u.50354
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t u : Set α
Φ : α → β
⊢ hausdorffEdist s t = 0 ↔ closure s = closure t
simp only [hausdorffEdist_def, ENNReal.sup_eq_zero, ENNReal.iSup_eq_zero, ← subset_def,
  ← mem_closure_iff_infEdist_zero, subset_antisymm_iff, isClosed_closure.closure_subset_iff]