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