ι : Type ?u.288498
ι' : Type ?u.288501
α : Type u_1
β : Type ?u.288507
γ : Type u_2
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup γ
f g : α → γ
hf : Tendsto f atTop atTop
hg : Tendsto g atTop atTop
⊢ Tendsto (Prod.map f g) (atTop ×ˢ atTop) atTop
ι : Type ?u.288498
ι' : Type ?u.288501
α : Type u_1
β : Type ?u.288507
γ : Type u_2
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup γ
f g : α → γ
hf : Tendsto f atTop atTop
hg : Tendsto g atTop atTop
⊢ Tendsto (Prod.map f g) atTop atTop
rw [← prod_atTop_atTop_eq]
no goals
ι : Type ?u.288498
ι' : Type ?u.288501
α : Type u_1
β : Type ?u.288507
γ : Type u_2
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup γ
f g : α → γ
hf : Tendsto f atTop atTop
hg : Tendsto g atTop atTop
⊢ Tendsto (Prod.map f g) (atTop ×ˢ atTop) atTop
exact hf.prod_map_prod_atTop hg