Mathlib.Order.Filter.AtTopBot.Prod

Filter.prod_atTop_atTop_eq theorem

[Preorder α] [Preorder β] : (atTop : Filter α) ×ˢ (atTop : Filter β) = (atTop : Filter (α × β))

Full source

theorem prod_atTop_atTop_eq [Preorder α] [Preorder β] :
    (atTop : Filter α) ×ˢ (atTop : Filter β) = (atTop : Filter (α × β)) := by
  cases isEmpty_or_nonempty α
  · subsingleton
  cases isEmpty_or_nonempty β
  · subsingleton
  simpa [atTop, prod_iInf_left, prod_iInf_right, iInf_prod] using iInf_comm

Product of `atTop` Filters Equals `atTop` on Product Type

Informal description

For preordered types $\alpha$ and $\beta$, the product filter of the `atTop` filters on $\alpha$ and $\beta$ is equal to the `atTop` filter on the product type $\alpha \times \beta$. In other words, \[ \text{atTop}_{\alpha} \times \text{atTop}_{\beta} = \text{atTop}_{\alpha \times \beta}. \]

Filter.tendsto_finset_prod_atTop theorem

: Tendsto (fun (p : Finset ι × Finset ι') ↦ p.1 ×ˢ p.2) atTop atTop

Full source

lemma tendsto_finset_prod_atTop :
    Tendsto (fun (p : FinsetFinset ι × Finset ι') ↦ p.1 ×ˢ p.2) atTop atTop := by
  classical
  apply Monotone.tendsto_atTop_atTop
  · intro p q hpq
    simpa using Finset.product_subset_product hpq.1 hpq.2
  · intro b
    use (Finset.image Prod.fst b, Finset.image Prod.snd b)
    exact Finset.subset_product

Cartesian Product of Finite Sets Tends to Infinity in Both Coordinates

Informal description

Let $\iota$ and $\iota'$ be index types. The function that maps a pair of finite subsets $(s, t) \in \text{Finset } \iota \times \text{Finset } \iota'$ to their Cartesian product $s \times t \in \text{Finset } (\iota \times \iota')$ tends to infinity in both coordinates. More precisely, the induced map between the product of `atTop` filters on $\text{Finset } \iota$ and $\text{Finset } \iota'$ is equal to the `atTop` filter on $\text{Finset } (\iota \times \iota')$.

Filter.prod_atBot_atBot_eq theorem

[Preorder α] [Preorder β] : (atBot : Filter α) ×ˢ (atBot : Filter β) = (atBot : Filter (α × β))

Full source

theorem prod_atBot_atBot_eq [Preorder α] [Preorder β] :
    (atBot : Filter α) ×ˢ (atBot : Filter β) = (atBot : Filter (α × β)) :=
  @prod_atTop_atTop_eq αᵒᵈ βᵒᵈ _ _

Product of `atBot` Filters Equals `atBot` on Product Type

Informal description

For preordered types $\alpha$ and $\beta$, the product filter of the `atBot` filters on $\alpha$ and $\beta$ is equal to the `atBot` filter on the product type $\alpha \times \beta$. In other words, \[ \text{atBot}_{\alpha} \times \text{atBot}_{\beta} = \text{atBot}_{\alpha \times \beta}. \]

Filter.prod_map_atTop_eq theorem

 {α₁ α₂ β₁ β₂ : Type*} [Preorder β₁] [Preorder β₂] (u₁ : β₁ → α₁) (u₂ : β₂ → α₂) :
  map u₁ atTop ×ˢ map u₂ atTop = map (Prod.map u₁ u₂) atTop

Full source

theorem prod_map_atTop_eq {α₁ α₂ β₁ β₂ : Type*} [Preorder β₁] [Preorder β₂]
    (u₁ : β₁ → α₁) (u₂ : β₂ → α₂) : map u₁ atTop ×ˢ map u₂ atTop = map (Prod.map u₁ u₂) atTop := by
  rw [prod_map_map_eq, prod_atTop_atTop_eq, Prod.map_def]

Product of Pushforward Filters at Infinity Equals Pushforward of Product Map

Informal description

Let $\beta_1$ and $\beta_2$ be preordered types, and let $u_1 : \beta_1 \to \alpha_1$ and $u_2 : \beta_2 \to \alpha_2$ be functions. The product of the pushforward filters $\text{map}\,u_1\,\text{atTop}$ and $\text{map}\,u_2\,\text{atTop}$ is equal to the pushforward of the product map $\text{Prod.map}\,u_1\,u_2$ applied to the $\text{atTop}$ filter on $\beta_1 \times \beta_2$. In other words, \[ \text{map}\,u_1\,\text{atTop} \times \text{map}\,u_2\,\text{atTop} = \text{map}\,(\text{Prod.map}\,u_1\,u_2)\,\text{atTop}. \]

Filter.prod_map_atBot_eq theorem

 {α₁ α₂ β₁ β₂ : Type*} [Preorder β₁] [Preorder β₂] (u₁ : β₁ → α₁) (u₂ : β₂ → α₂) :
  map u₁ atBot ×ˢ map u₂ atBot = map (Prod.map u₁ u₂) atBot

Full source

theorem prod_map_atBot_eq {α₁ α₂ β₁ β₂ : Type*} [Preorder β₁] [Preorder β₂]
    (u₁ : β₁ → α₁) (u₂ : β₂ → α₂) : map u₁ atBot ×ˢ map u₂ atBot = map (Prod.map u₁ u₂) atBot :=
  @prod_map_atTop_eq _ _ β₁ᵒᵈ β₂ᵒᵈ _ _ _ _

Product of Pushforward Filters at Negative Infinity Equals Pushforward of Product Map

Informal description

Let $\beta_1$ and $\beta_2$ be preordered types, and let $u_1 : \beta_1 \to \alpha_1$ and $u_2 : \beta_2 \to \alpha_2$ be functions. The product of the pushforward filters $\text{map}\,u_1\,\text{atBot}$ and $\text{map}\,u_2\,\text{atBot}$ is equal to the pushforward of the product map $(u_1 \times u_2)$ applied to the $\text{atBot}$ filter on $\beta_1 \times \beta_2$. In other words, \[ \text{map}\,u_1\,\text{atBot} \times \text{map}\,u_2\,\text{atBot} = \text{map}\,(u_1 \times u_2)\,\text{atBot}. \]

Filter.tendsto_atBot_diagonal theorem

[Preorder α] : Tendsto (fun a : α => (a, a)) atBot atBot

Full source

theorem tendsto_atBot_diagonal [Preorder α] : Tendsto (fun a : α => (a, a)) atBot atBot := by
  rw [← prod_atBot_atBot_eq]
  exact tendsto_id.prodMk tendsto_id

Diagonal Map Preserves Limit at Negative Infinity

Informal description

For any preordered type $\alpha$, the diagonal map $a \mapsto (a, a)$ preserves limits at negative infinity, i.e., the function tends to $-\infty$ in $\alpha \times \alpha$ as $a$ tends to $-\infty$ in $\alpha$.

Filter.tendsto_atTop_diagonal theorem

[Preorder α] : Tendsto (fun a : α => (a, a)) atTop atTop

Full source

theorem tendsto_atTop_diagonal [Preorder α] : Tendsto (fun a : α => (a, a)) atTop atTop := by
  rw [← prod_atTop_atTop_eq]
  exact tendsto_id.prodMk tendsto_id

Diagonal Map Preserves Limit at Infinity in Product Space

Informal description

For any preordered type $\alpha$, the diagonal map $a \mapsto (a, a)$ tends to infinity in $\alpha \times \alpha$ as $a$ tends to infinity in $\alpha$. In other words, the function $\lambda a. (a, a)$ is a mapping from $\alpha$ to $\alpha \times \alpha$ that preserves the limit at infinity.

Filter.Tendsto.prod_map_prod_atBot theorem

 [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

Full source

theorem Tendsto.prod_map_prod_atBot [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 := by
  rw [← prod_atBot_atBot_eq]
  exact hf.prodMap hg

Product Map Tends to Negative Infinity under Product Filter

Informal description

Let $\alpha$, $\beta$, and $\gamma$ be preordered types, and let $F$ and $G$ be filters on $\alpha$ and $\beta$ respectively. Given functions $f : \alpha \to \gamma$ and $g : \beta \to \gamma$ such that $f$ tends to $-\infty$ along $F$ and $g$ tends to $-\infty$ along $G$, then the product map $(f, g) : \alpha \times \beta \to \gamma \times \gamma$ tends to $-\infty$ along the product filter $F \times G$.

Filter.Tendsto.prod_map_prod_atTop theorem

 [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

Full source

theorem Tendsto.prod_map_prod_atTop [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 := by
  rw [← prod_atTop_atTop_eq]
  exact hf.prodMap hg

Product Map Tends to $\text{atTop}$ under Product Filter

Informal description

Let $\alpha$, $\beta$, and $\gamma$ be preordered types, and let $F$ and $G$ be filters on $\alpha$ and $\beta$ respectively. Given functions $f : \alpha \to \gamma$ and $g : \beta \to \gamma$ such that $f$ tends to $\text{atTop}$ along $F$ and $g$ tends to $\text{atTop}$ along $G$, then the product map $(f, g) : \alpha \times \beta \to \gamma \times \gamma$ tends to $\text{atTop}$ along the product filter $F \times G$.

Filter.Tendsto.prod_atBot theorem

 [Preorder α] [Preorder γ] {f g : α → γ} (hf : Tendsto f atBot atBot) (hg : Tendsto g atBot atBot) :
  Tendsto (Prod.map f g) atBot atBot

Full source

theorem Tendsto.prod_atBot [Preorder α] [Preorder γ] {f g : α → γ}
    (hf : Tendsto f atBot atBot) (hg : Tendsto g atBot atBot) :
    Tendsto (Prod.map f g) atBot atBot := by
  rw [← prod_atBot_atBot_eq]
  exact hf.prod_map_prod_atBot hg

Product Map Tends to Negative Infinity under `atBot` Filter

Informal description

Let $\alpha$ and $\gamma$ be preordered types, and let $f, g : \alpha \to \gamma$ be functions such that $f$ tends to $-\infty$ along the `atBot` filter and $g$ tends to $-\infty$ along the `atBot` filter. Then the product map $(f, g) : \alpha \to \gamma \times \gamma$ tends to $-\infty$ along the `atBot` filter.

Filter.Tendsto.prod_atTop theorem

 [Preorder α] [Preorder γ] {f g : α → γ} (hf : Tendsto f atTop atTop) (hg : Tendsto g atTop atTop) :
  Tendsto (Prod.map f g) atTop atTop

Full source

theorem Tendsto.prod_atTop [Preorder α] [Preorder γ] {f g : α → γ}
    (hf : Tendsto f atTop atTop) (hg : Tendsto g atTop atTop) :
    Tendsto (Prod.map f g) atTop atTop := by
  rw [← prod_atTop_atTop_eq]
  exact hf.prod_map_prod_atTop hg

Product Map Tends to $\text{atTop}$ under $\text{atTop}$ Filter

Informal description

Let $\alpha$ and $\gamma$ be preordered types, and let $f, g : \alpha \to \gamma$ be functions such that $f$ tends to $\text{atTop}$ along $\text{atTop}$ and $g$ tends to $\text{atTop}$ along $\text{atTop}$. Then the product map $(f, g) : \alpha \to \gamma \times \gamma$ tends to $\text{atTop}$ along $\text{atTop}$.

Filter.eventually_atBot_prod_self theorem

 [Nonempty α] [Preorder α] [IsDirected α (· ≥ ·)] {p : α × α → Prop} :
  (∀ᶠ x in atBot, p x) ↔ ∃ a, ∀ k l, k ≤ a → l ≤ a → p (k, l)

Full source

theorem eventually_atBot_prod_self [Nonempty α] [Preorder α] [IsDirected α (· ≥ ·)]
    {p : α × α → Prop} : (∀ᶠ x in atBot, p x) ↔ ∃ a, ∀ k l, k ≤ a → l ≤ a → p (k, l) := by
  simp [← prod_atBot_atBot_eq, (@atBot_basis α _ _).prod_self.eventually_iff]

Characterization of Eventually True Predicates in the Product `atBot` Filter

Informal description

Let $\alpha$ be a nonempty preordered type that is directed with respect to the reverse order $\geq$. For any predicate $p$ on $\alpha \times \alpha$, the following are equivalent: 1. The predicate $p(x)$ holds for all $x$ eventually in the `atBot` filter on $\alpha \times \alpha$. 2. There exists an element $a \in \alpha$ such that for all $k, l \in \alpha$ with $k \leq a$ and $l \leq a$, the predicate $p(k, l)$ holds.

Filter.eventually_atTop_prod_self theorem

 [Nonempty α] [Preorder α] [IsDirected α (· ≤ ·)] {p : α × α → Prop} :
  (∀ᶠ x in atTop, p x) ↔ ∃ a, ∀ k l, a ≤ k → a ≤ l → p (k, l)

Full source

theorem eventually_atTop_prod_self [Nonempty α] [Preorder α] [IsDirected α (· ≤ ·)]
    {p : α × α → Prop} : (∀ᶠ x in atTop, p x) ↔ ∃ a, ∀ k l, a ≤ k → a ≤ l → p (k, l) :=
  eventually_atBot_prod_self (α := αᵒᵈ)

Characterization of Eventually True Predicates in the Product `atTop` Filter

Informal description

Let $\alpha$ be a nonempty preordered type that is directed with respect to the order $\leq$. For any predicate $p$ on $\alpha \times \alpha$, the following are equivalent: 1. The predicate $p(x)$ holds for all $x$ eventually in the `atTop` filter on $\alpha \times \alpha$. 2. There exists an element $a \in \alpha$ such that for all $k, l \in \alpha$ with $a \leq k$ and $a \leq l$, the predicate $p(k, l)$ holds.

Filter.eventually_atBot_prod_self' theorem

 [Nonempty α] [Preorder α] [IsDirected α (· ≥ ·)] {p : α × α → Prop} :
  (∀ᶠ x in atBot, p x) ↔ ∃ a, ∀ k ≤ a, ∀ l ≤ a, p (k, l)

Full source

theorem eventually_atBot_prod_self' [Nonempty α] [Preorder α] [IsDirected α (· ≥ ·)]
    {p : α × α → Prop} : (∀ᶠ x in atBot, p x) ↔ ∃ a, ∀ k ≤ a, ∀ l ≤ a, p (k, l) := by
  simp only [eventually_atBot_prod_self, forall_cond_comm]

Characterization of Eventually True Predicates in Product `atBot` Filter

Informal description

Let $\alpha$ be a nonempty type with a preorder $\leq$ such that $\alpha$ is directed with respect to the reverse order $\geq$. For any predicate $p$ on $\alpha \times \alpha$, the following are equivalent: 1. The predicate $p(x)$ holds for all $x$ in the filter `atBot` on $\alpha \times \alpha$. 2. There exists an element $a \in \alpha$ such that for all $k, l \in \alpha$ with $k \leq a$ and $l \leq a$, the predicate $p(k, l)$ holds.

Filter.eventually_atTop_prod_self' theorem

 [Nonempty α] [Preorder α] [IsDirected α (· ≤ ·)] {p : α × α → Prop} :
  (∀ᶠ x in atTop, p x) ↔ ∃ a, ∀ k ≥ a, ∀ l ≥ a, p (k, l)

Full source

theorem eventually_atTop_prod_self' [Nonempty α] [Preorder α] [IsDirected α (· ≤ ·)]
    {p : α × α → Prop} : (∀ᶠ x in atTop, p x) ↔ ∃ a, ∀ k ≥ a, ∀ l ≥ a, p (k, l) := by
  simp only [eventually_atTop_prod_self, forall_cond_comm]

Characterization of Eventually True Predicates in Product `atTop` Filter

Informal description

Let $\alpha$ be a nonempty type with a preorder $\leq$ such that $\alpha$ is directed with respect to $\leq$. For any predicate $p$ on $\alpha \times \alpha$, the following are equivalent: 1. The predicate $p(x)$ holds for all $x$ in the filter `atTop` on $\alpha \times \alpha$. 2. There exists an element $a \in \alpha$ such that for all $k, l \in \alpha$ with $a \leq k$ and $a \leq l$, the predicate $p(k, l)$ holds. In other words, $p$ holds eventually in the product filter `atTop × atTop` if and only if there is a common lower bound $a$ beyond which $p$ holds for all pairs $(k, l)$.

Filter.eventually_atTop_curry theorem

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

Full source

theorem eventually_atTop_curry [Preorder α] [Preorder β] {p : α × β → Prop}
    (hp : ∀ᶠ x : α × β in Filter.atTop, p x) : ∀ᶠ k in atTop, ∀ᶠ l in atTop, p (k, l) := by
  rw [← prod_atTop_atTop_eq] at hp
  exact hp.curry

Currying of Eventually True Predicates in Product `atTop` Filter

Informal description

Let $\alpha$ and $\beta$ be preordered types, and let $p : \alpha \times \beta \to \text{Prop}$ be a predicate. If $p(x)$ holds for all $x$ in the `atTop` filter on $\alpha \times \beta$, then for all $k$ in the `atTop` filter on $\alpha$ and all $l$ in the `atTop` filter on $\beta$, the predicate $p(k, l)$ holds. In other words, if $p$ holds eventually in the product filter `atTop` on $\alpha \times \beta$, then $p$ holds eventually in each component filter `atTop` on $\alpha$ and $\beta$ separately.

Filter.eventually_atBot_curry theorem

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

Full source

theorem eventually_atBot_curry [Preorder α] [Preorder β] {p : α × β → Prop}
    (hp : ∀ᶠ x : α × β in Filter.atBot, p x) : ∀ᶠ k in atBot, ∀ᶠ l in atBot, p (k, l) :=
  @eventually_atTop_curry αᵒᵈ βᵒᵈ _ _ _ hp

Currying of Eventually True Predicates in Product `atBot` Filter

Informal description

Let $\alpha$ and $\beta$ be preordered types, and let $p : \alpha \times \beta \to \text{Prop}$ be a predicate. If $p(x)$ holds for all $x$ in the `atBot` filter on $\alpha \times \beta$, then for all $k$ in the `atBot` filter on $\alpha$ and all $l$ in the `atBot` filter on $\beta$, the predicate $p(k, l)$ holds. In other words, if $p$ holds eventually in the product filter `atBot` on $\alpha \times \beta$, then $p$ holds eventually in each component filter `atBot` on $\alpha$ and $\beta$ separately.