no goals
α : Type u
β : Type v
γ : Type ?u.206424
δ : Type ?u.206427
ε : Type ?u.206430
ζ : Type ?u.206433
ι : Type u_1
π : ι → Type u_2
κ : Type ?u.206444
inst✝¹ : TopologicalSpace α
inst✝ : (i : ι) → TopologicalSpace (π i)
f✝ : α → (i : ι) → π i
f : β → (i : ι) → π i
g : (i : ι) → π i
u : Filter β
⊢ Tendsto f u (𝓝 g) ↔ ∀ (x : ι), Tendsto (fun i => f i x) u (𝓝 (g x))
rw [nhds_pi, Filter.tendsto_pi]