no goals
α : Type u
β : Type v
X : Type ?u.302924
ι : Type ?u.302927
inst✝ : PseudoMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ
s✝ s : Set α
a : α
⊢ (∀ (i : ℝ), 0 < i → ∃ y, y ∈ s ∧ y ∈ ball a i) ↔ ∀ (ε : ℝ), ε > 0 → ∃ b, b ∈ s ∧ dist a b < ε
simp only [mem_ball, dist_comm]