no goals
α : Type u_1
β✝ : Type ?u.395811
γ : Type ?u.395814
ι : Type ?u.395817
inst✝³ : Nonempty α
inst✝² : SemilatticeSup α
inst✝¹ : NoMaxOrder α
β : Type u_2
inst✝ : SeminormedAddCommGroup β
f : α → β
b : β
⊢ (∀ (ib : ℝ), 0 < ib → ∃ ia, True ∧ ∀ (x : α), x ∈ Set.Ioi ia → f x ∈ ball b ib) ↔
    ∀ (ε : ℝ), 0 < ε → ∃ N, ∀ (n : α), N < n → ‖f n - b‖ < ε
simp [dist_eq_norm]