ι : Type ?u.286644
ι' : Type ?u.286647
α : Type u_1
β : Type ?u.286653
γ : Type u_2
inst✝¹ : SemilatticeInf α
inst✝ : SemilatticeInf γ
f g : α → γ
hf : Tendsto f atBot atBot
hg : Tendsto g atBot atBot
⊢ Tendsto (Prod.map f g) (atBot ×ˢ atBot) atBot
ι : Type ?u.286644
ι' : Type ?u.286647
α : Type u_1
β : Type ?u.286653
γ : Type u_2
inst✝¹ : SemilatticeInf α
inst✝ : SemilatticeInf γ
f g : α → γ
hf : Tendsto f atBot atBot
hg : Tendsto g atBot atBot
⊢ Tendsto (Prod.map f g) atBot atBot
rw [← prod_atBot_atBot_eq]
no goals
ι : Type ?u.286644
ι' : Type ?u.286647
α : Type u_1
β : Type ?u.286653
γ : Type u_2
inst✝¹ : SemilatticeInf α
inst✝ : SemilatticeInf γ
f g : α → γ
hf : Tendsto f atBot atBot
hg : Tendsto g atBot atBot
⊢ Tendsto (Prod.map f g) (atBot ×ˢ atBot) atBot
exact hf.prod_map_prod_atBot hg