ι : Type ?u.281006
ι' : Type ?u.281009
α : Type u_1
β : Type ?u.281015
γ : Type ?u.281018
inst✝ : SemilatticeInf α
⊢ Tendsto (fun a => (a, a)) atBot (atBot ×ˢ atBot)
ι : Type ?u.281006
ι' : Type ?u.281009
α : Type u_1
β : Type ?u.281015
γ : Type ?u.281018
inst✝ : SemilatticeInf α
⊢ Tendsto (fun a => (a, a)) atBot atBot
rw [← prod_atBot_atBot_eq]
no goals
ι : Type ?u.281006
ι' : Type ?u.281009
α : Type u_1
β : Type ?u.281015
γ : Type ?u.281018
inst✝ : SemilatticeInf α
⊢ Tendsto (fun a => (a, a)) atBot (atBot ×ˢ atBot)
exact tendsto_id.prod_mk tendsto_id