no goals
α : Type u
β : Type v
X : Type ?u.305337
ι : Type ?u.305340
inst✝ : PseudoMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ
s✝ s : Set α
hs : IsClosed s
a : α
⊢ a ∈ s ↔ ∀ (ε : ℝ), ε > 0 → ∃ b, b ∈ s ∧ dist a b < ε
simpa only [hs.closure_eq] using @mem_closure_iff _ _ s a