no goals
ι : Sort ?u.66060
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
h : IsClosed s
hs : Set.Nonempty s
⊢ ¬x ∈ s ↔ 0 < infDist x s
simp [h.mem_iff_infDist_zero hs, infDist_nonneg.gt_iff_ne]