no goals
ι : Sort ?u.17353
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t : Set α
Φ : α → β
h : IsClosed s
⊢ x ∈ s ↔ infEdist x s = 0
rw [← mem_closure_iff_infEdist_zero, h.closure_eq]