no goals
ι : Sort ?u.65322
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
h : Set.Nonempty s
⊢ x ∈ closure s ↔ infDist x s = 0
simp [mem_closure_iff_infEdist_zero, infDist, ENNReal.toReal_eq_zero_iff, infEdist_ne_top h]