no goals
α : Type u_1
β : Type u_2
γ : Type ?u.171379
δ : Type ?u.171382
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
⊢ Continuous f ↔ ∀ (x : α) (g : Ultrafilter α), ↑g ≤ 𝓝 x → Tendsto f (↑g) (𝓝 (f x))
simp only [continuous_iff_continuousAt, continuousAt_iff_ultrafilter]