no goals
α : Type u
β : Type v
X : Type ?u.306162
ι : Type ?u.306165
inst✝ : PseudoMetricSpace α
x✝ y z : α
ε ε₁ ε₂ : ℝ
s✝ s : Set α
x : α
⊢ x ∈ closure s ↔ ∀ (r : ℝ), r > 0 → Set.Nonempty (ball x r ∩ s)
simp only [mem_closure_iff, Set.Nonempty, exists_prop, mem_inter_iff, mem_ball', and_comm]