# `Filter.atTop` and `Filter.atBot` filters on products #

source
theorem Filter.prod_atTop_atTop_eq {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] :
atTop ×ˢ atTop = atTop
source
theorem Filter.tendsto_finset_prod_atTop {ι : Type u_1} {ι' : Type u_2} :
Tendsto (fun (p : Finset ι × Finset ι') => p.1 ×ˢ p.2) atTop atTop
source
theorem Filter.prod_atBot_atBot_eq {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] :
atBot ×ˢ atBot = atBot
source
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
source
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
source
theorem Filter.tendsto_atBot_diagonal {α : Type u_3} [Preorder α] :
Tendsto (fun (a : α) => (a, a)) atBot atBot
source
theorem Filter.tendsto_atTop_diagonal {α : Type u_3} [Preorder α] :
Tendsto (fun (a : α) => (a, a)) atTop atTop
source
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
source
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
source
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
source
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
source
theorem Filter.eventually_atBot_prod_self {α : Type u_3} [Nonempty α] [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≥ x2] {p : α × α → Prop} :
(∀ᶠ (x : α × α) in atBot, p x) ↔ ∃ (a : α), ∀ (k l : α), k ≤ a → l ≤ a → p (k, l)
source
theorem Filter.eventually_atTop_prod_self {α : Type u_3} [Nonempty α] [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≤ x2] {p : α × α → Prop} :
(∀ᶠ (x : α × α) in atTop, p x) ↔ ∃ (a : α), ∀ (k l : α), a ≤ k → a ≤ l → p (k, l)
source
theorem Filter.eventually_atBot_prod_self' {α : Type u_3} [Nonempty α] [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≥ x2] {p : α × α → Prop} :
(∀ᶠ (x : α × α) in atBot, p x) ↔ ∃ (a : α), ∀ k ≤ a, ∀ l ≤ a, p (k, l)
source
theorem Filter.eventually_atTop_prod_self' {α : Type u_3} [Nonempty α] [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≤ x2] {p : α × α → Prop} :
(∀ᶠ (x : α × α) in atTop, p x) ↔ ∃ (a : α), ∀ k ≥ a, ∀ l ≥ a, p (k, l)
source
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)
source
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)