ι : Type ?u.283686
ι' : Type ?u.283689
α : Type u_2
β : Type u_3
γ : Type u_1
inst✝ : SemilatticeInf γ
F : Filter α
G : Filter β
f : α → γ
g : β → γ
hf : Tendsto f F atBot
hg : Tendsto g G atBot
⊢ Tendsto (Prod.map f g) (F ×ˢ G) (atBot ×ˢ atBot)
ι : Type ?u.283686
ι' : Type ?u.283689
α : Type u_2
β : Type u_3
γ : Type u_1
inst✝ : SemilatticeInf γ
F : Filter α
G : Filter β
f : α → γ
g : β → γ
hf : Tendsto f F atBot
hg : Tendsto g G atBot
⊢ Tendsto (Prod.map f g) (F ×ˢ G) atBot
rw [← prod_atBot_atBot_eq]
no goals
ι : Type ?u.283686
ι' : Type ?u.283689
α : Type u_2
β : Type u_3
γ : Type u_1
inst✝ : SemilatticeInf γ
F : Filter α
G : Filter β
f : α → γ
g : β → γ
hf : Tendsto f F atBot
hg : Tendsto g G atBot
⊢ Tendsto (Prod.map f g) (F ×ˢ G) (atBot ×ˢ atBot)
exact hf.prod_map hg