Filter.atTop and Filter.atBot filters on products

theorem Filter.prod_atTop_atTop_eq {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] : atTop ×ˢ atTop = atTop

theorem Filter.tendsto_finset_prod_atTop {ι : Type u_1} {ι' : Type u_2} : Tendsto (fun (p : Finset ι × Finset ι') => p.1 ×ˢ p.2) atTop atTop

theorem Filter.prod_atBot_atBot_eq {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] : atBot ×ˢ atBot = atBot

theorem Filter.prod_map_atTop_eq {α₁ : Type u_6} {α₂ : Type u_7} {β₁ : Type u_8} {β₂ : Type u_9} [Preorder β₁] [Preorder β₂] (u₁ : β₁ → α₁) (u₂ : β₂ → α₂) : map u₁ atTop ×ˢ map u₂ atTop = map (Prod.map u₁ u₂) atTop

theorem Filter.prod_map_atBot_eq {α₁ : Type u_6} {α₂ : Type u_7} {β₁ : Type u_8} {β₂ : Type u_9} [Preorder β₁] [Preorder β₂] (u₁ : β₁ → α₁) (u₂ : β₂ → α₂) : map u₁ atBot ×ˢ map u₂ atBot = map (Prod.map u₁ u₂) atBot

theorem Filter.tendsto_atBot_diagonal {α : Type u_3} [Preorder α] : Tendsto (fun (a : α) => (a, a)) atBot atBot

theorem Filter.tendsto_atTop_diagonal {α : Type u_3} [Preorder α] : Tendsto (fun (a : α) => (a, a)) atTop atTop

theorem Filter.Tendsto.prod_map_prod_atBot {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Preorder γ] {F : Filter α} {G : Filter β} {f : α → γ} {g : β → γ} (hf : Tendsto f F atBot) (hg : Tendsto g G atBot) : Tendsto (Prod.map f g) (F ×ˢ G) atBot

theorem Filter.Tendsto.prod_map_prod_atTop {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Preorder γ] {F : Filter α} {G : Filter β} {f : α → γ} {g : β → γ} (hf : Tendsto f F atTop) (hg : Tendsto g G atTop) : Tendsto (Prod.map f g) (F ×ˢ G) atTop

theorem Filter.Tendsto.prod_atBot {α : Type u_3} {γ : Type u_5} [Preorder α] [Preorder γ] {f g : α → γ} (hf : Tendsto f atBot atBot) (hg : Tendsto g atBot atBot) : Tendsto (Prod.map f g) atBot atBot

theorem Filter.Tendsto.prod_atTop {α : Type u_3} {γ : Type u_5} [Preorder α] [Preorder γ] {f g : α → γ} (hf : Tendsto f atTop atTop) (hg : Tendsto g atTop atTop) : Tendsto (Prod.map f g) atTop atTop