ι : Type ?u.284969
ι' : Type ?u.284972
α : Type u_2
β : Type u_3
γ : Type u_1
inst✝ : SemilatticeSup γ
F : Filter α
G : Filter β
f : α → γ
g : β → γ
hf : Tendsto f F atTop
hg : Tendsto g G atTop
⊢ Tendsto (Prod.map f g) (F ×ˢ G) (atTop ×ˢ atTop)
ι : Type ?u.284969
ι' : Type ?u.284972
α : Type u_2
β : Type u_3
γ : Type u_1
inst✝ : SemilatticeSup γ
F : Filter α
G : Filter β
f : α → γ
g : β → γ
hf : Tendsto f F atTop
hg : Tendsto g G atTop
⊢ Tendsto (Prod.map f g) (F ×ˢ G) atTop
rw [← prod_atTop_atTop_eq]
no goals
ι : Type ?u.284969
ι' : Type ?u.284972
α : Type u_2
β : Type u_3
γ : Type u_1
inst✝ : SemilatticeSup γ
F : Filter α
G : Filter β
f : α → γ
g : β → γ
hf : Tendsto f F atTop
hg : Tendsto g G atTop
⊢ Tendsto (Prod.map f g) (F ×ˢ G) (atTop ×ˢ atTop)
exact hf.prod_map hg