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_finsetProd_atTop {ι : Type u_1} {ι' : Type u_2} : Tendsto (fun (p : Finset ι × Finset ι') => p.1 ×ˢ p.2) atTop atTop

@[deprecated Filter.tendsto_finsetProd_atTop (since := "2026-04-08")]

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

Alias of Filter.tendsto_finsetProd_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

theorem Filter.eventually_atBot_prod_self {α : Type u_3} [Nonempty α] [Preorder α] [IsCodirectedOrder α] {p : α × α → Prop} : (∀ᶠ (x : α × α) in atBot, p x) ↔ ∃ (a : α), ∀ (k l : α), k ≤ a → l ≤ a → p (k, l)

theorem Filter.eventually_atTop_prod_self {α : Type u_3} [Nonempty α] [Preorder α] [IsDirectedOrder α] {p : α × α → Prop} : (∀ᶠ (x : α × α) in atTop, p x) ↔ ∃ (a : α), ∀ (k l : α), a ≤ k → a ≤ l → p (k, l)

theorem Filter.eventually_atBot_prod_self' {α : Type u_3} [Nonempty α] [Preorder α] [IsCodirectedOrder α] {p : α × α → Prop} : (∀ᶠ (x : α × α) in atBot, p x) ↔ ∃ (a : α), ∀ k ≤ a, ∀ l ≤ a, p (k, l)

theorem Filter.eventually_atTop_prod_self' {α : Type u_3} [Nonempty α] [Preorder α] [IsDirectedOrder α] {p : α × α → Prop} : (∀ᶠ (x : α × α) in atTop, p x) ↔ ∃ (a : α), ∀ k ≥ a, ∀ l ≥ a, p (k, l)

theorem Filter.eventually_atTop_curry {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {p : α × β → Prop} (hp : ∀ᶠ (x : α × β) in atTop, p x) : ∀ᶠ (k : α) in atTop, ∀ᶠ (l : β) in atTop, p (k, l)

theorem Filter.eventually_atBot_curry {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {p : α × β → Prop} (hp : ∀ᶠ (x : α × β) in atBot, p x) : ∀ᶠ (k : α) in atBot, ∀ᶠ (l : β) in atBot, p (k, l)