no goals
α : Type u
β : Type v
X : Type ?u.224214
inst✝² : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
u : β → α
a : α
⊢ (∀ (ib : ℝ≥0∞), 0 < ib → ∃ ia, True ∧ ∀ (x : β), x ∈ Ici ia → u x ∈ ball a ib) ↔
    ∀ (ε : ℝ≥0∞), ε > 0 → ∃ N, ∀ (n : β), n ≥ N → edist (u n) a < ε
simp only [exists_prop, true_and_iff, mem_Ici, mem_ball]