no goals
α : Type u
β : Type v
X : Type ?u.306971
ι : Type ?u.306974
inst✝ : PseudoMetricSpace α
x✝ y z : α
ε ε₁ ε₂ : ℝ
s : Set α
f : β → α
x : α
⊢ x ∈ closure (range f) ↔ ∀ (r : ℝ), r > 0 → ∃ y, dist x (f y) < r
simp only [mem_closure_iff, exists_range_iff]