no goals
α : Type u
β : Type v
X : Type ?u.304312
ι : Type ?u.304315
inst✝ : PseudoMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ
s : Set α
e : β → α
a : α
⊢ (∀ (i : ℕ), True → ∃ y, y ∈ range e ∧ y ∈ ball a (1 / (↑i + 1))) ↔ ∀ (n : ℕ), ∃ k, dist a (e k) < 1 / (↑n + 1)
simp only [mem_ball, dist_comm, exists_range_iff, forall_const]