no goals
ι : Sort ?u.17614
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x✝ y : α
s t : Set α
Φ : α → β
x : α
E : Set α
⊢ 0 < infEdist x E ↔ ¬x ∈ closure E
rw [mem_closure_iff_infEdist_zero, pos_iff_ne_zero]