α : Type u
β : Type v
γ✝ : Type ?u.40052
δ : Type ?u.40055
ε : Type ?u.40058
ζ : Type ?u.40061
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ✝
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
γ : Type u_1
a : α
b : β
f : Filter γ
ma : γ → α
mb : γ → β
ha : Tendsto ma f (𝓝 a)
hb : Tendsto mb f (𝓝 b)
⊢ Tendsto (fun c => (ma c, mb c)) f (𝓝 a ×ˢ 𝓝 b)
α : Type u
β : Type v
γ✝ : Type ?u.40052
δ : Type ?u.40055
ε : Type ?u.40058
ζ : Type ?u.40061
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ✝
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
γ : Type u_1
a : α
b : β
f : Filter γ
ma : γ → α
mb : γ → β
ha : Tendsto ma f (𝓝 a)
hb : Tendsto mb f (𝓝 b)
⊢ Tendsto (fun c => (ma c, mb c)) f (𝓝 (a, b))
rw [nhds_prod_eq]
no goals
α : Type u
β : Type v
γ✝ : Type ?u.40052
δ : Type ?u.40055
ε : Type ?u.40058
ζ : Type ?u.40061
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ✝
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
γ : Type u_1
a : α
b : β
f : Filter γ
ma : γ → α
mb : γ → β
ha : Tendsto ma f (𝓝 a)
hb : Tendsto mb f (𝓝 b)
⊢ Tendsto (fun c => (ma c, mb c)) f (𝓝 a ×ˢ 𝓝 b)
exact Filter.Tendsto.prod_mk ha hb