Mathlib.Order.Filter.Prod

Filter.prod_mem_prod theorem

(hs : s ∈ f) (ht : t ∈ g) : s ×ˢ t ∈ f ×ˢ g

Full source

theorem prod_mem_prod (hs : s ∈ f) (ht : t ∈ g) : s ×ˢ t ∈ f ×ˢ g :=
  inter_mem_inf (preimage_mem_comap hs) (preimage_mem_comap ht)

Cartesian Product of Filter Sets Belongs to Product Filter

Informal description

For any sets $s \in f$ and $t \in g$, where $f$ is a filter on type $\alpha$ and $g$ is a filter on type $\beta$, the Cartesian product $s \times t$ belongs to the product filter $f \timesˢ g$ on $\alpha \times \beta$.

Filter.mem_prod_iff theorem

 {s : Set (α × β)} {f : Filter α} {g : Filter β} : s ∈ f ×ˢ g ↔ ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ ×ˢ t₂ ⊆ s

Full source

theorem mem_prod_iff {s : Set (α × β)} {f : Filter α} {g : Filter β} :
    s ∈ f ×ˢ gs ∈ f ×ˢ g ↔ ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ ×ˢ t₂ ⊆ s := by
  constructor
  · rintro ⟨t₁, ⟨s₁, hs₁, hts₁⟩, t₂, ⟨s₂, hs₂, hts₂⟩, rfl⟩
    exact ⟨s₁, hs₁, s₂, hs₂, fun p ⟨h, h'⟩ => ⟨hts₁ h, hts₂ h'⟩⟩
  · rintro ⟨t₁, ht₁, t₂, ht₂, h⟩
    exact mem_inf_of_inter (preimage_mem_comap ht₁) (preimage_mem_comap ht₂) h

Characterization of Membership in Product Filter: $s \in f \timesˢ g \leftrightarrow \exists t_1 \in f, \exists t_2 \in g, t_1 \times t_2 \subseteq s$

Informal description

For any set $s \subseteq \alpha \times \beta$ and filters $f$ on $\alpha$ and $g$ on $\beta$, the set $s$ belongs to the product filter $f \timesˢ g$ if and only if there exist sets $t_1 \in f$ and $t_2 \in g$ such that the Cartesian product $t_1 \times t_2$ is contained in $s$.

Filter.compl_diagonal_mem_prod theorem

{l₁ l₂ : Filter α} : (diagonal α)ᶜ ∈ l₁ ×ˢ l₂ ↔ Disjoint l₁ l₂

Full source

@[simp]
theorem compl_diagonal_mem_prod {l₁ l₂ : Filter α} : (diagonal α)ᶜ(diagonal α)ᶜ ∈ l₁ ×ˢ l₂(diagonal α)ᶜ ∈ l₁ ×ˢ l₂ ↔ Disjoint l₁ l₂ := by
  simp only [mem_prod_iff, Filter.disjoint_iff, prod_subset_compl_diagonal_iff_disjoint]

Complement of Diagonal in Product Filter Characterizes Disjointness of Filters

Informal description

For any two filters $l_1$ and $l_2$ on a type $\alpha$, the complement of the diagonal set $\{(a,a) \mid a \in \alpha\}$ belongs to the product filter $l_1 \timesˢ l_2$ if and only if $l_1$ and $l_2$ are disjoint filters.

Filter.prod_mem_prod_iff theorem

[f.NeBot] [g.NeBot] : s ×ˢ t ∈ f ×ˢ g ↔ s ∈ f ∧ t ∈ g

Full source

@[simp]
theorem prod_mem_prod_iff [f.NeBot] [g.NeBot] : s ×ˢ t ∈ f ×ˢ gs ×ˢ t ∈ f ×ˢ g ↔ s ∈ f ∧ t ∈ g :=
  ⟨fun h =>
    let ⟨_s', hs', _t', ht', H⟩ := mem_prod_iff.1 h
    (prod_subset_prod_iff.1 H).elim
      (fun ⟨hs's, ht't⟩ => ⟨mem_of_superset hs' hs's, mem_of_superset ht' ht't⟩) fun h =>
      h.elim (fun hs'e => absurd hs'e (nonempty_of_mem hs').ne_empty) fun ht'e =>
        absurd ht'e (nonempty_of_mem ht').ne_empty,
    fun h => prod_mem_prod h.1 h.2⟩

Characterization of Cartesian Products in Product Filter for Non-trivial Filters

Informal description

For non-trivial filters $f$ on $\alpha$ and $g$ on $\beta$, and sets $s \subseteq \alpha$, $t \subseteq \beta$, the Cartesian product $s \times t$ belongs to the product filter $f \timesˢ g$ if and only if $s \in f$ and $t \in g$.

Filter.mem_prod_principal theorem

{s : Set (α × β)} : s ∈ f ×ˢ 𝓟 t ↔ {a | ∀ b ∈ t, (a, b) ∈ s} ∈ f

Full source

theorem mem_prod_principal {s : Set (α × β)} :
    s ∈ f ×ˢ 𝓟 ts ∈ f ×ˢ 𝓟 t ↔ { a | ∀ b ∈ t, (a, b) ∈ s } ∈ f := by
  rw [← @exists_mem_subset_iff _ f, mem_prod_iff]
  refine exists_congr fun u => Iff.rfl.and ⟨?_, fun h => ⟨t, mem_principal_self t, ?_⟩⟩
  · rintro ⟨v, v_in, hv⟩ a a_in b b_in
    exact hv (mk_mem_prod a_in <| v_in b_in)
  · rintro ⟨x, y⟩ ⟨hx, hy⟩
    exact h hx y hy

Characterization of Membership in Product Filter with Principal Filter: $s \in f \timesˢ \mathfrak{P}(t) \leftrightarrow \{a \mid \forall b \in t, (a, b) \in s\} \in f$

Informal description

For any set $s \subseteq \alpha \times \beta$ and any filter $f$ on $\alpha$, the set $s$ belongs to the product filter $f \timesˢ \mathfrak{P}(t)$ (where $\mathfrak{P}(t)$ is the principal filter generated by $t \subseteq \beta$) if and only if the set $\{a \in \alpha \mid \forall b \in t, (a, b) \in s\}$ belongs to $f$.

Filter.mem_prod_top theorem

{s : Set (α × β)} : s ∈ f ×ˢ (⊤ : Filter β) ↔ {a | ∀ b, (a, b) ∈ s} ∈ f

Full source

theorem mem_prod_top {s : Set (α × β)} :
    s ∈ f ×ˢ (⊤ : Filter β)s ∈ f ×ˢ (⊤ : Filter β) ↔ { a | ∀ b, (a, b) ∈ s } ∈ f := by
  rw [← principal_univ, mem_prod_principal]
  simp only [mem_univ, forall_true_left]

Characterization of Membership in Product Filter with Top Filter: $s \in f \timesˢ \top \leftrightarrow \{a \mid \forall b, (a, b) \in s\} \in f$

Informal description

For any set $s \subseteq \alpha \times \beta$ and any filter $f$ on $\alpha$, the set $s$ belongs to the product filter $f \timesˢ \top$ (where $\top$ is the top filter on $\beta$) if and only if the set $\{a \in \alpha \mid \forall b \in \beta, (a, b) \in s\}$ belongs to $f$.

Filter.eventually_prod_principal_iff theorem

 {p : α × β → Prop} {s : Set β} : (∀ᶠ x : α × β in f ×ˢ 𝓟 s, p x) ↔ ∀ᶠ x : α in f, ∀ y : β, y ∈ s → p (x, y)

Full source

theorem eventually_prod_principal_iff {p : α × β → Prop} {s : Set β} :
    (∀ᶠ x : α × β in f ×ˢ 𝓟 s, p x) ↔ ∀ᶠ x : α in f, ∀ y : β, y ∈ s → p (x, y) := by
  rw [eventually_iff, eventually_iff, mem_prod_principal]
  simp only [mem_setOf_eq]

Characterization of "Eventually" in Product Filter with Principal Filter

Informal description

For any predicate $p : \alpha \times \beta \to \text{Prop}$ and any subset $s \subseteq \beta$, the statement $\forallᶠ (x, y) \text{ in } f \timesˢ \mathfrak{P}(s), p(x, y)$ holds if and only if $\forallᶠ x \text{ in } f, \forall y \in s, p(x, y)$, where $\mathfrak{P}(s)$ denotes the principal filter generated by $s$.

Filter.comap_prod theorem

 (f : α → β × γ) (b : Filter β) (c : Filter γ) : comap f (b ×ˢ c) = comap (Prod.fst ∘ f) b ⊓ comap (Prod.snd ∘ f) c

Full source

theorem comap_prod (f : α → β × γ) (b : Filter β) (c : Filter γ) :
    comap f (b ×ˢ c) = comapcomap (Prod.fst ∘ f) b ⊓ comap (Prod.snd ∘ f) c := by
  rw [prod_eq_inf, comap_inf, Filter.comap_comap, Filter.comap_comap]

Preimage of Product Filter Decomposes as Infimum of Preimage Filters

Informal description

For any function $f \colon \alpha \to \beta \times \gamma$ and filters $b$ on $\beta$ and $c$ on $\gamma$, the preimage filter of the product filter $b \timesˢ c$ under $f$ is equal to the infimum of the preimage filters of $b$ under $\pi_1 \circ f$ and of $c$ under $\pi_2 \circ f$, where $\pi_1$ and $\pi_2$ are the first and second projection maps. In symbols: \[ \text{comap}_f (b \timesˢ c) = \text{comap}_{\pi_1 \circ f} b \sqcap \text{comap}_{\pi_2 \circ f} c. \]

Filter.comap_prodMap_prod theorem

 (f : α → β) (g : γ → δ) (lb : Filter β) (ld : Filter δ) : comap (Prod.map f g) (lb ×ˢ ld) = comap f lb ×ˢ comap g ld

Full source

theorem comap_prodMap_prod (f : α → β) (g : γ → δ) (lb : Filter β) (ld : Filter δ) :
    comap (Prod.map f g) (lb ×ˢ ld) = comap f lb ×ˢ comap g ld := by
  simp [prod_eq_inf, comap_comap, Function.comp_def]

Preimage of Product Filter under Product Map Equals Product of Preimage Filters

Informal description

For any functions $f \colon \alpha \to \beta$ and $g \colon \gamma \to \delta$, and any filters $lb$ on $\beta$ and $ld$ on $\delta$, the preimage filter of the product filter $lb \timesˢ ld$ under the product map $\text{Prod.map } f g$ is equal to the product of the preimage filters $\text{comap } f lb$ and $\text{comap } g ld$. In symbols: \[ \text{comap } (\text{Prod.map } f g) (lb \timesˢ ld) = (\text{comap } f lb) \timesˢ (\text{comap } g ld). \]

Filter.prod_top theorem

: f ×ˢ (⊤ : Filter β) = f.comap Prod.fst

Full source

theorem prod_top : f ×ˢ (⊤ : Filter β) = f.comap Prod.fst := by
  rw [prod_eq_inf, comap_top, inf_top_eq]

Product Filter with Top Filter Equals Preimage under First Projection

Informal description

For any filter $f$ on a type $\alpha$, the product filter $f \times^s \top$ on $\alpha \times \beta$ (where $\top$ is the top filter on $\beta$) is equal to the preimage filter of $f$ under the first projection map $\pi_1 : \alpha \times \beta \to \alpha$. That is, $f \times^s \top = \text{comap } \pi_1 f$.

Filter.top_prod theorem

: (⊤ : Filter α) ×ˢ g = g.comap Prod.snd

Full source

theorem top_prod : (⊤ : Filter α) ×ˢ g = g.comap Prod.snd := by
  rw [prod_eq_inf, comap_top, top_inf_eq]

Product of Top Filter with Any Filter Equals Preimage under Second Projection

Informal description

For any filter $g$ on a type $\beta$, the product filter $\top \timesˢ g$ on $\alpha \times \beta$ is equal to the preimage filter of $g$ under the second projection $\pi_2 : \alpha \times \beta \to \beta$, i.e., $\top \timesˢ g = \text{comap } \pi_2 g$.

Filter.sup_prod theorem

(f₁ f₂ : Filter α) (g : Filter β) : (f₁ ⊔ f₂) ×ˢ g = (f₁ ×ˢ g) ⊔ (f₂ ×ˢ g)

Full source

theorem sup_prod (f₁ f₂ : Filter α) (g : Filter β) : (f₁ ⊔ f₂) ×ˢ g = (f₁ ×ˢ g) ⊔ (f₂ ×ˢ g) := by
  simp only [prod_eq_inf, comap_sup, inf_sup_right]

Distributivity of Product Filter over Supremum: $(f_1 \sqcup f_2) \timesˢ g = (f_1 \timesˢ g) \sqcup (f_2 \timesˢ g)$

Informal description

For any two filters $f_1$ and $f_2$ on a type $\alpha$ and any filter $g$ on a type $\beta$, the product filter of the supremum $f_1 \sqcup f_2$ with $g$ is equal to the supremum of the product filters $f_1 \timesˢ g$ and $f_2 \timesˢ g$: $$ (f_1 \sqcup f_2) \timesˢ g = (f_1 \timesˢ g) \sqcup (f_2 \timesˢ g). $$

Filter.prod_sup theorem

(f : Filter α) (g₁ g₂ : Filter β) : f ×ˢ (g₁ ⊔ g₂) = (f ×ˢ g₁) ⊔ (f ×ˢ g₂)

Full source

theorem prod_sup (f : Filter α) (g₁ g₂ : Filter β) : f ×ˢ (g₁ ⊔ g₂) = (f ×ˢ g₁) ⊔ (f ×ˢ g₂) := by
  simp only [prod_eq_inf, comap_sup, inf_sup_left]

Distributivity of Product Filter over Supremum: $f \timesˢ (g_1 \sqcup g_2) = (f \timesˢ g_1) \sqcup (f \timesˢ g_2)$

Informal description

For any filter $f$ on a type $\alpha$ and any two filters $g_1$ and $g_2$ on a type $\beta$, the product filter $f \timesˢ (g_1 \sqcup g_2)$ is equal to the supremum of the product filters $(f \timesˢ g_1) \sqcup (f \timesˢ g_2)$. In other words, the product filter operation distributes over the supremum of filters on the second component: $$ f \timesˢ (g_1 \sqcup g_2) = (f \timesˢ g_1) \sqcup (f \timesˢ g_2). $$

Filter.eventually_prod_iff theorem

 {p : α × β → Prop} :
  (∀ᶠ x in f ×ˢ g, p x) ↔
    ∃ pa : α → Prop, (∀ᶠ x in f, pa x) ∧ ∃ pb : β → Prop, (∀ᶠ y in g, pb y) ∧ ∀ {x}, pa x → ∀ {y}, pb y → p (x, y)

Full source

theorem eventually_prod_iff {p : α × β → Prop} :
    (∀ᶠ x in f ×ˢ g, p x) ↔
      ∃ pa : α → Prop, (∀ᶠ x in f, pa x) ∧ ∃ pb : β → Prop, (∀ᶠ y in g, pb y) ∧
        ∀ {x}, pa x → ∀ {y}, pb y → p (x, y) := by
  simpa only [Set.prod_subset_iff] using @mem_prod_iff α β p f g

Characterization of Eventually Property in Product Filter

Informal description

For any predicate $p : \alpha \times \beta \to \text{Prop}$ and filters $f$ on $\alpha$ and $g$ on $\beta$, the following are equivalent: 1. The predicate $p(x,y)$ holds for all $(x,y)$ in some set belonging to the product filter $f \timesˢ g$. 2. There exist predicates $p_a : \alpha \to \text{Prop}$ and $p_b : \beta \to \text{Prop}$ such that: - $p_a(x)$ holds for all $x$ in some set belonging to $f$, - $p_b(y)$ holds for all $y$ in some set belonging to $g$, - For any $x$ satisfying $p_a(x)$ and any $y$ satisfying $p_b(y)$, the predicate $p(x,y)$ holds.

Filter.tendsto_fst theorem

: Tendsto Prod.fst (f ×ˢ g) f

Full source

theorem tendsto_fst : Tendsto Prod.fst (f ×ˢ g) f :=
  tendsto_inf_left tendsto_comap

Projection to First Component Preserves Limits Under Product Filter

Informal description

For any filters $f$ on a type $\alpha$ and $g$ on a type $\beta$, the projection map $\pi_1: \alpha \times \beta \to \alpha$ tends to $f$ with respect to the product filter $f \timesˢ g$ on $\alpha \times \beta$.

Filter.tendsto_snd theorem

: Tendsto Prod.snd (f ×ˢ g) g

Full source

theorem tendsto_snd : Tendsto Prod.snd (f ×ˢ g) g :=
  tendsto_inf_right tendsto_comap

Second projection preserves limits under product filter

Informal description

For any filters $f$ on a type $\alpha$ and $g$ on a type $\beta$, the projection map $\operatorname{snd} : \alpha \times \beta \to \beta$ tends to $g$ with respect to the product filter $f \timesˢ g$. In other words, the second projection is a limit-preserving map from the product filter to its second component.

Filter.Tendsto.fst theorem

{h : Filter γ} {m : α → β × γ} (H : Tendsto m f (g ×ˢ h)) : Tendsto (fun a ↦ (m a).1) f g

Full source

/-- If a function tends to a product `g ×ˢ h` of filters, then its first component tends to
`g`. See also `Filter.Tendsto.fst_nhds` for the special case of converging to a point in a
product of two topological spaces. -/
theorem Tendsto.fst {h : Filter γ} {m : α → β × γ} (H : Tendsto m f (g ×ˢ h)) :
    Tendsto (fun a ↦ (m a).1) f g :=
  tendsto_fst.comp H

First Component Preserves Limits Under Product Filter

Informal description

Let $f$ be a filter on a type $\alpha$, $g$ be a filter on a type $\beta$, and $h$ be a filter on a type $\gamma$. Given a function $m : \alpha \to \beta \times \gamma$ such that $m$ tends to the product filter $g \timesˢ h$ with respect to $f$, then the first component function $a \mapsto (m a).1$ tends to $g$ with respect to $f$.

Filter.Tendsto.snd theorem

{h : Filter γ} {m : α → β × γ} (H : Tendsto m f (g ×ˢ h)) : Tendsto (fun a ↦ (m a).2) f h

Full source

/-- If a function tends to a product `g ×ˢ h` of filters, then its second component tends to
`h`. See also `Filter.Tendsto.snd_nhds` for the special case of converging to a point in a
product of two topological spaces. -/
theorem Tendsto.snd {h : Filter γ} {m : α → β × γ} (H : Tendsto m f (g ×ˢ h)) :
    Tendsto (fun a ↦ (m a).2) f h :=
  tendsto_snd.comp H

Second component tends to second filter under product filter convergence

Informal description

Let $f$ be a filter on a type $\alpha$, $g$ a filter on $\beta$, and $h$ a filter on $\gamma$. If a function $m : \alpha \to \beta \times \gamma$ tends to the product filter $g \timesˢ h$ with respect to $f$, then the second component function $a \mapsto (m a).2$ tends to $h$ with respect to $f$.

Filter.Tendsto.prodMk theorem

 {h : Filter γ} {m₁ : α → β} {m₂ : α → γ} (h₁ : Tendsto m₁ f g) (h₂ : Tendsto m₂ f h) :
  Tendsto (fun x => (m₁ x, m₂ x)) f (g ×ˢ h)

Full source

theorem Tendsto.prodMk {h : Filter γ} {m₁ : α → β} {m₂ : α → γ}
    (h₁ : Tendsto m₁ f g) (h₂ : Tendsto m₂ f h) : Tendsto (fun x => (m₁ x, m₂ x)) f (g ×ˢ h) :=
  tendsto_inf.2 ⟨tendsto_comap_iff.2 h₁, tendsto_comap_iff.2 h₂⟩

Tendsto of Product Map to Product Filter

Informal description

Given two functions $m_1 : \alpha \to \beta$ and $m_2 : \alpha \to \gamma$, and filters $f$ on $\alpha$, $g$ on $\beta$, and $h$ on $\gamma$, if $m_1$ tends to $g$ with respect to $f$ and $m_2$ tends to $h$ with respect to $f$, then the combined function $x \mapsto (m_1(x), m_2(x))$ tends to the product filter $g \timesˢ h$ with respect to $f$.

Filter.tendsto_prod_swap theorem

: Tendsto (Prod.swap : α × β → β × α) (f ×ˢ g) (g ×ˢ f)

Full source

theorem tendsto_prod_swap : Tendsto (Prod.swap : α × β → β × α) (f ×ˢ g) (g ×ˢ f) :=
  tendsto_snd.prodMk tendsto_fst

Limit Preservation of Swap Operation on Product Filters

Informal description

The swap function $(x, y) \mapsto (y, x)$ from $\alpha \times \beta$ to $\beta \times \alpha$ tends to the product filter $g \timesˢ f$ with respect to the product filter $f \timesˢ g$. In other words, the swap operation preserves limits when applied to product filters.

Filter.Eventually.prod_inl theorem

 {la : Filter α} {p : α → Prop} (h : ∀ᶠ x in la, p x) (lb : Filter β) : ∀ᶠ x in la ×ˢ lb, p (x : α × β).1

Full source

theorem Eventually.prod_inl {la : Filter α} {p : α → Prop} (h : ∀ᶠ x in la, p x) (lb : Filter β) :
    ∀ᶠ x in la ×ˢ lb, p (x : α × β).1 :=
  tendsto_fst.eventually h

Eventual Property Preservation under First Projection in Product Filter

Informal description

Let $p : \alpha \to \text{Prop}$ be a predicate and $l_a$ a filter on $\alpha$ such that $p$ holds eventually with respect to $l_a$ (i.e., $\{x \mid p x\} \in l_a$). Then for any filter $l_b$ on $\beta$, the predicate $p$ holds eventually for the first component of elements in the product filter $l_a \timesˢ l_b$ on $\alpha \times \beta$. That is, $\forallᶠ x \text{ in } l_a \timesˢ l_b, p (x.1)$.

Filter.Eventually.prod_inr theorem

 {lb : Filter β} {p : β → Prop} (h : ∀ᶠ x in lb, p x) (la : Filter α) : ∀ᶠ x in la ×ˢ lb, p (x : α × β).2

Full source

theorem Eventually.prod_inr {lb : Filter β} {p : β → Prop} (h : ∀ᶠ x in lb, p x) (la : Filter α) :
    ∀ᶠ x in la ×ˢ lb, p (x : α × β).2 :=
  tendsto_snd.eventually h

Eventual Property Preservation under Second Projection in Product Filter

Informal description

Let $p : \beta \to \text{Prop}$ be a predicate and $l_b$ a filter on $\beta$ such that $p$ holds eventually with respect to $l_b$ (i.e., $\{x \mid p x\} \in l_b$). Then for any filter $l_a$ on $\alpha$, the predicate $p$ holds eventually for the second component of elements in the product filter $l_a \timesˢ l_b$ on $\alpha \times \beta$. That is, $\forallᶠ x \text{ in } l_a \timesˢ l_b, p (x.2)$.

Filter.Eventually.prod_mk theorem

 {la : Filter α} {pa : α → Prop} (ha : ∀ᶠ x in la, pa x) {lb : Filter β} {pb : β → Prop} (hb : ∀ᶠ y in lb, pb y) :
  ∀ᶠ p in la ×ˢ lb, pa (p : α × β).1 ∧ pb p.2

Full source

theorem Eventually.prod_mk {la : Filter α} {pa : α → Prop} (ha : ∀ᶠ x in la, pa x) {lb : Filter β}
    {pb : β → Prop} (hb : ∀ᶠ y in lb, pb y) : ∀ᶠ p in la ×ˢ lb, pa (p : α × β).1 ∧ pb p.2 :=
  (ha.prod_inl lb).and (hb.prod_inr la)

Eventual Conjunction in Product Filter

Informal description

Let $l_a$ be a filter on a type $\alpha$ and $l_b$ a filter on a type $\beta$. If a predicate $p_a : \alpha \to \text{Prop}$ holds eventually with respect to $l_a$ and a predicate $p_b : \beta \to \text{Prop}$ holds eventually with respect to $l_b$, then the conjunction $p_a(x) \land p_b(y)$ holds eventually for all pairs $(x, y)$ in the product filter $l_a \timesˢ l_b$ on $\alpha \times \beta$.

Filter.EventuallyEq.prodMap theorem

 {δ} {la : Filter α} {fa ga : α → γ} (ha : fa =ᶠ[la] ga) {lb : Filter β} {fb gb : β → δ} (hb : fb =ᶠ[lb] gb) :
  Prod.map fa fb =ᶠ[la ×ˢ lb] Prod.map ga gb

Full source

theorem EventuallyEq.prodMap {δ} {la : Filter α} {fa ga : α → γ} (ha : fa =ᶠ[la] ga)
    {lb : Filter β} {fb gb : β → δ} (hb : fb =ᶠ[lb] gb) :
    Prod.mapProd.map fa fb =ᶠ[la ×ˢ lb] Prod.map ga gb :=
  (Eventually.prod_mk ha hb).mono fun _ h => Prod.ext h.1 h.2

Eventual Equality of Product Maps under Product Filter

Informal description

Let $\alpha$, $\beta$, $\gamma$, and $\delta$ be types, and let $l_a$ and $l_b$ be filters on $\alpha$ and $\beta$ respectively. Suppose $f_a, g_a : \alpha \to \gamma$ are functions that are eventually equal with respect to $l_a$, and $f_b, g_b : \beta \to \delta$ are functions that are eventually equal with respect to $l_b$. Then the product maps $\text{Prod.map}\, f_a\, f_b$ and $\text{Prod.map}\, g_a\, g_b$ are eventually equal with respect to the product filter $l_a \timesˢ l_b$ on $\alpha \times \beta$.

Filter.EventuallyLE.prodMap theorem

 {δ} [LE γ] [LE δ] {la : Filter α} {fa ga : α → γ} (ha : fa ≤ᶠ[la] ga) {lb : Filter β} {fb gb : β → δ}
  (hb : fb ≤ᶠ[lb] gb) : Prod.map fa fb ≤ᶠ[la ×ˢ lb] Prod.map ga gb

Full source

theorem EventuallyLE.prodMap {δ} [LE γ] [LE δ] {la : Filter α} {fa ga : α → γ} (ha : fa ≤ᶠ[la] ga)
    {lb : Filter β} {fb gb : β → δ} (hb : fb ≤ᶠ[lb] gb) :
    Prod.mapProd.map fa fb ≤ᶠ[la ×ˢ lb] Prod.map ga gb :=
  Eventually.prod_mk ha hb

Product Filter Preserves Pointwise Inequality under Mapping

Informal description

Let $\gamma$ and $\delta$ be types equipped with a less-than-or-equal relation $\leq$, and let $l_a$ be a filter on a type $\alpha$ and $l_b$ a filter on a type $\beta$. If $f_a \leqᶠ[l_a] g_a$ and $f_b \leqᶠ[l_b] g_b$, then the product map $(f_a, f_b) \leqᶠ[l_a \timesˢ l_b] (g_a, g_b)$ in the product filter $l_a \timesˢ l_b$ on $\alpha \times \beta$.

Filter.Eventually.curry theorem

 {la : Filter α} {lb : Filter β} {p : α × β → Prop} (h : ∀ᶠ x in la ×ˢ lb, p x) : ∀ᶠ x in la, ∀ᶠ y in lb, p (x, y)

Full source

theorem Eventually.curry {la : Filter α} {lb : Filter β} {p : α × β → Prop}
    (h : ∀ᶠ x in la ×ˢ lb, p x) : ∀ᶠ x in la, ∀ᶠ y in lb, p (x, y) := by
  rcases eventually_prod_iff.1 h with ⟨pa, ha, pb, hb, h⟩
  exact ha.mono fun a ha => hb.mono fun b hb => h ha hb

Currying Property of Eventually in Product Filter

Informal description

Let $f$ be a filter on a type $\alpha$ and $g$ a filter on a type $\beta$. For any predicate $p : \alpha \times \beta \to \text{Prop}$, if $p(x,y)$ holds for all $(x,y)$ in some set belonging to the product filter $f \timesˢ g$, then for all $x$ in some set belonging to $f$, the predicate $p(x,y)$ holds for all $y$ in some set belonging to $g$.

Filter.Frequently.uncurry theorem

 {la : Filter α} {lb : Filter β} {p : α → β → Prop} (h : ∃ᶠ x in la, ∃ᶠ y in lb, p x y) : ∃ᶠ xy in la ×ˢ lb, p xy.1 xy.2

Full source

protected lemma Frequently.uncurry {la : Filter α} {lb : Filter β} {p : α → β → Prop}
    (h : ∃ᶠ x in la, ∃ᶠ y in lb, p x y) : ∃ᶠ xy in la ×ˢ lb, p xy.1 xy.2 :=
  mt (fun h ↦ by simpa only [not_frequently] using h.curry) h

Frequent Uncurrying in Product Filter

Informal description

Let $f$ be a filter on a type $\alpha$ and $g$ a filter on a type $\beta$. For any predicate $p : \alpha \times \beta \to \text{Prop}$, if there exist frequently an $x \in f$ and frequently a $y \in g$ such that $p(x,y)$ holds, then there exists frequently a pair $(x,y) \in f \timesˢ g$ such that $p(x,y)$ holds.

Filter.Frequently.of_curry theorem

 {la : Filter α} {lb : Filter β} {p : α × β → Prop} (h : ∃ᶠ x in la, ∃ᶠ y in lb, p (x, y)) : ∃ᶠ xy in la ×ˢ lb, p xy

Full source

lemma Frequently.of_curry {la : Filter α} {lb : Filter β} {p : α × β → Prop}
    (h : ∃ᶠ x in la, ∃ᶠ y in lb, p (x, y)) : ∃ᶠ xy in la ×ˢ lb, p xy :=
  h.uncurry

Frequent Occurrence in Product Filter via Currying

Informal description

Let $f$ be a filter on a type $\alpha$ and $g$ a filter on a type $\beta$. For any predicate $p : \alpha \times \beta \to \text{Prop}$, if there exist frequently an $x \in f$ and frequently a $y \in g$ such that $p(x,y)$ holds, then there exists frequently a pair $(x,y) \in f \timesˢ g$ such that $p(x,y)$ holds.

Filter.Eventually.diag_of_prod theorem

{p : α × α → Prop} (h : ∀ᶠ i in f ×ˢ f, p i) : ∀ᶠ i in f, p (i, i)

Full source

/-- A fact that is eventually true about all pairs `l ×ˢ l` is eventually true about
all diagonal pairs `(i, i)` -/
theorem Eventually.diag_of_prod {p : α × α → Prop} (h : ∀ᶠ i in f ×ˢ f, p i) :
    ∀ᶠ i in f, p (i, i) := by
  obtain ⟨t, ht, s, hs, hst⟩ := eventually_prod_iff.1 h
  apply (ht.and hs).mono fun x hx => hst hx.1 hx.2

Diagonal Property in Product Filter: $p(x,y)$ holds for all $(x,y) \in f \timesˢ f$ implies $p(i,i)$ holds for all $i \in f$

Informal description

Let $f$ be a filter on a type $\alpha$ and let $p : \alpha \times \alpha \to \text{Prop}$ be a predicate. If $p(x, y)$ holds for all $(x, y)$ in some set belonging to the product filter $f \timesˢ f$, then $p(i, i)$ holds for all $i$ in some set belonging to $f$.

Filter.Eventually.diag_of_prod_left theorem

 {f : Filter α} {g : Filter γ} {p : (α × α) × γ → Prop} :
  (∀ᶠ x in (f ×ˢ f) ×ˢ g, p x) → ∀ᶠ x : α × γ in f ×ˢ g, p ((x.1, x.1), x.2)

Full source

theorem Eventually.diag_of_prod_left {f : Filter α} {g : Filter γ} {p : (α × α) × γ → Prop} :
    (∀ᶠ x in (f ×ˢ f) ×ˢ g, p x) → ∀ᶠ x : α × γ in f ×ˢ g, p ((x.1, x.1), x.2) := by
  intro h
  obtain ⟨t, ht, s, hs, hst⟩ := eventually_prod_iff.1 h
  exact (ht.diag_of_prod.prod_mk hs).mono fun x hx => by simp only [hst hx.1 hx.2]

Diagonal Property in Left Product Filter: $p(x,y)$ holds for all $(x,y) \in (f \timesˢ f) \timesˢ g$ implies $p((a,a),c)$ holds for all $(a,c) \in f \timesˢ g$

Informal description

Let $f$ be a filter on a type $\alpha$, $g$ a filter on a type $\gamma$, and $p : (\alpha \times \alpha) \times \gamma \to \text{Prop}$ a predicate. If $p(x, y)$ holds for all $(x, y)$ in some set belonging to the product filter $(f \timesˢ f) \timesˢ g$, then for all pairs $(a, c) \in \alpha \times \gamma$ in the product filter $f \timesˢ g$, the predicate $p((a, a), c)$ holds.

Filter.Eventually.diag_of_prod_right theorem

 {f : Filter α} {g : Filter γ} {p : α × γ × γ → Prop} :
  (∀ᶠ x in f ×ˢ (g ×ˢ g), p x) → ∀ᶠ x : α × γ in f ×ˢ g, p (x.1, x.2, x.2)

Full source

theorem Eventually.diag_of_prod_right {f : Filter α} {g : Filter γ} {p : α × γ × γ → Prop} :
    (∀ᶠ x in f ×ˢ (g ×ˢ g), p x) → ∀ᶠ x : α × γ in f ×ˢ g, p (x.1, x.2, x.2) := by
  intro h
  obtain ⟨t, ht, s, hs, hst⟩ := eventually_prod_iff.1 h
  exact (ht.prod_mk hs.diag_of_prod).mono fun x hx => by simp only [hst hx.1 hx.2]

Diagonal Property in Right Product Filter: $p(x,y,z)$ holds in $f \timesˢ (g \timesˢ g)$ implies $p(x,y,y)$ holds in $f \timesˢ g$

Informal description

Let $f$ be a filter on a type $\alpha$, $g$ a filter on a type $\gamma$, and $p : \alpha \times \gamma \times \gamma \to \text{Prop}$ a predicate. If $p(x, y, z)$ holds for all $(x, y, z)$ in some set belonging to the product filter $f \timesˢ (g \timesˢ g)$, then $p(x, y, y)$ holds for all $(x, y)$ in some set belonging to the product filter $f \timesˢ g$.

Filter.tendsto_diag theorem

: Tendsto (fun i => (i, i)) f (f ×ˢ f)

Full source

theorem tendsto_diag : Tendsto (fun i => (i, i)) f (f ×ˢ f) :=
  tendsto_iff_eventually.mpr fun _ hpr => hpr.diag_of_prod

Diagonal Map Tends to Product Filter: $i \mapsto (i,i)$ tends to $f \timesˢ f$

Informal description

The diagonal map $i \mapsto (i, i)$ tends to the product filter $f \timesˢ f$ as $i$ tends to $f$. In other words, for any filter $f$ on a type $\alpha$, the function $\lambda i, (i, i)$ is a limit point of the product filter $f \timesˢ f$ with respect to $f$.

Filter.prod_iInf_left theorem

[Nonempty ι] {f : ι → Filter α} {g : Filter β} : (⨅ i, f i) ×ˢ g = ⨅ i, f i ×ˢ g

Full source

theorem prod_iInf_left [Nonempty ι] {f : ι → Filter α} {g : Filter β} :
    (⨅ i, f i) ×ˢ g = ⨅ i, f i ×ˢ g := by
  simp only [prod_eq_inf, comap_iInf, iInf_inf]

Infimum Distributes Over Product Filter on the Left: $(\bigsqcap_i f_i) \timesˢ g = \bigsqcap_i (f_i \timesˢ g)$

Informal description

For a nonempty index set $\iota$, a family of filters $\{f_i\}_{i \in \iota}$ on a type $\alpha$, and a filter $g$ on a type $\beta$, the product filter of the infimum of the $f_i$ with $g$ is equal to the infimum of the product filters $f_i \timesˢ g$: \[ \left(\bigsqcap_{i \in \iota} f_i\right) \timesˢ g = \bigsqcap_{i \in \iota} (f_i \timesˢ g). \]

Filter.prod_iInf_right theorem

[Nonempty ι] {f : Filter α} {g : ι → Filter β} : (f ×ˢ ⨅ i, g i) = ⨅ i, f ×ˢ g i

Full source

theorem prod_iInf_right [Nonempty ι] {f : Filter α} {g : ι → Filter β} :
    (f ×ˢ ⨅ i, g i) = ⨅ i, f ×ˢ g i := by
  simp only [prod_eq_inf, comap_iInf, inf_iInf]

Product Filter Distributes Over Infima in Second Argument: $f \timesˢ \bigsqcap_i g_i = \bigsqcap_i (f \timesˢ g_i)$

Informal description

For a nonempty index type $\iota$, a filter $f$ on a type $\alpha$, and a family of filters $(g_i)_{i \in \iota}$ on a type $\beta$, the product filter $f \timesˢ \bigsqcap_i g_i$ is equal to the infimum of the product filters $\bigsqcap_i (f \timesˢ g_i)$. In other words, the product filter operation distributes over infima in its second argument: \[ f \timesˢ \left(\bigsqcap_{i \in \iota} g_i\right) = \bigsqcap_{i \in \iota} (f \timesˢ g_i). \]

Filter.prod_mono theorem

 {f₁ f₂ : Filter α} {g₁ g₂ : Filter β} (hf : f₁ ≤ f₂) (hg : g₁ ≤ g₂) : f₁ ×ˢ g₁ ≤ f₂ ×ˢ g₂

Full source

@[mono, gcongr]
theorem prod_mono {f₁ f₂ : Filter α} {g₁ g₂ : Filter β} (hf : f₁ ≤ f₂) (hg : g₁ ≤ g₂) :
    f₁ ×ˢ g₁ ≤ f₂ ×ˢ g₂ :=
  inf_le_inf (comap_mono hf) (comap_mono hg)

Monotonicity of Product Filter: $f_1 \leq f_2 \land g_1 \leq g_2 \Rightarrow f_1 \timesˢ g_1 \leq f_2 \timesˢ g_2$

Informal description

For any filters $f_1, f_2$ on a type $\alpha$ and $g_1, g_2$ on a type $\beta$, if $f_1 \leq f_2$ and $g_1 \leq g_2$, then the product filter $f_1 \timesˢ g_1$ is less than or equal to $f_2 \timesˢ g_2$.

Filter.prod_mono_left theorem

(g : Filter β) {f₁ f₂ : Filter α} (hf : f₁ ≤ f₂) : f₁ ×ˢ g ≤ f₂ ×ˢ g

Full source

@[gcongr]
theorem prod_mono_left (g : Filter β) {f₁ f₂ : Filter α} (hf : f₁ ≤ f₂) : f₁ ×ˢ g ≤ f₂ ×ˢ g :=
  Filter.prod_mono hf rfl.le

Monotonicity of Left Product Filter: $f_1 \leq f_2 \Rightarrow f_1 \timesˢ g \leq f_2 \timesˢ g$

Informal description

For any filter $g$ on a type $\beta$ and filters $f_1, f_2$ on a type $\alpha$, if $f_1 \leq f_2$, then the product filter $f_1 \timesˢ g$ is less than or equal to $f_2 \timesˢ g$.

Filter.prod_mono_right theorem

(f : Filter α) {g₁ g₂ : Filter β} (hf : g₁ ≤ g₂) : f ×ˢ g₁ ≤ f ×ˢ g₂

Full source

@[gcongr]
theorem prod_mono_right (f : Filter α) {g₁ g₂ : Filter β} (hf : g₁ ≤ g₂) : f ×ˢ g₁ ≤ f ×ˢ g₂ :=
  Filter.prod_mono rfl.le hf

Right Monotonicity of Product Filter: $g_1 \leq g_2 \Rightarrow f \timesˢ g_1 \leq f \timesˢ g_2$

Informal description

For any filter $f$ on a type $\alpha$ and any two filters $g_1, g_2$ on a type $\beta$, if $g_1 \leq g_2$, then the product filter $f \timesˢ g_1$ is less than or equal to $f \timesˢ g_2$.

Filter.prod_comap_comap_eq theorem

 {α₁ : Type u} {α₂ : Type v} {β₁ : Type w} {β₂ : Type x} {f₁ : Filter α₁} {f₂ : Filter α₂} {m₁ : β₁ → α₁}
  {m₂ : β₂ → α₂} : comap m₁ f₁ ×ˢ comap m₂ f₂ = comap (fun p : β₁ × β₂ => (m₁ p.1, m₂ p.2)) (f₁ ×ˢ f₂)

Full source

theorem prod_comap_comap_eq.{u, v, w, x} {α₁ : Type u} {α₂ : Type v} {β₁ : Type w} {β₂ : Type x}
    {f₁ : Filter α₁} {f₂ : Filter α₂} {m₁ : β₁ → α₁} {m₂ : β₂ → α₂} :
    comap m₁ f₁ ×ˢ comap m₂ f₂ = comap (fun p : β₁ × β₂ => (m₁ p.1, m₂ p.2)) (f₁ ×ˢ f₂) := by
  simp only [prod_eq_inf, comap_comap, comap_inf, Function.comp_def]

Product of Preimage Filters Equals Preimage of Product Filter

Informal description

For any types $\alpha_1, \alpha_2, \beta_1, \beta_2$, filters $f_1$ on $\alpha_1$ and $f_2$ on $\alpha_2$, and functions $m_1 : \beta_1 \to \alpha_1$ and $m_2 : \beta_2 \to \alpha_2$, the product filter of the preimage filters $\text{comap } m_1 f_1$ and $\text{comap } m_2 f_2$ is equal to the preimage filter of the product filter $f_1 \timesˢ f_2$ under the map $(p_1, p_2) \mapsto (m_1 p_1, m_2 p_2)$. In symbols: $$ \text{comap } m_1 f_1 \timesˢ \text{comap } m_2 f_2 = \text{comap } (p \mapsto (m_1 p.1, m_2 p.2)) (f_1 \timesˢ f_2). $$

Filter.prod_comm' theorem

: f ×ˢ g = comap Prod.swap (g ×ˢ f)

Full source

theorem prod_comm' : f ×ˢ g = comap Prod.swap (g ×ˢ f) := by
  simp only [prod_eq_inf, comap_comap, Function.comp_def, inf_comm, Prod.swap, comap_inf]

Commutativity of Product Filter via Preimage: $f \timesˢ g = \text{comap}_{\text{swap}}(g \timesˢ f)$

Informal description

For any filters $f$ on type $\alpha$ and $g$ on type $\beta$, the product filter $f \timesˢ g$ is equal to the preimage filter of the swapped product filter $g \timesˢ f$ under the swap function $\text{swap} \colon \beta \times \alpha \to \alpha \times \beta$. In symbols: $$ f \timesˢ g = \text{comap}_{\text{swap}} (g \timesˢ f). $$

Filter.prod_comm theorem

: f ×ˢ g = map (fun p : β × α => (p.2, p.1)) (g ×ˢ f)

Full source

theorem prod_comm : f ×ˢ g = map (fun p : β × α => (p.2, p.1)) (g ×ˢ f) := by
  rw [prod_comm', ← map_swap_eq_comap_swap]
  rfl

Commutativity of Product Filter via Image: $f \timesˢ g = \text{map}_{\text{swap}}(g \timesˢ f)$

Informal description

For any filters $f$ on type $\alpha$ and $g$ on type $\beta$, the product filter $f \timesˢ g$ is equal to the image filter of the swapped product filter $g \timesˢ f$ under the swap function $(p_1, p_2) \mapsto (p_2, p_1)$. In symbols: $$ f \timesˢ g = \text{map } (p \mapsto (p.2, p.1)) (g \timesˢ f). $$

Filter.mem_prod_iff_left theorem

{s : Set (α × β)} : s ∈ f ×ˢ g ↔ ∃ t ∈ f, ∀ᶠ y in g, ∀ x ∈ t, (x, y) ∈ s

Full source

theorem mem_prod_iff_left {s : Set (α × β)} :
    s ∈ f ×ˢ gs ∈ f ×ˢ g ↔ ∃ t ∈ f, ∀ᶠ y in g, ∀ x ∈ t, (x, y) ∈ s := by
  simp only [mem_prod_iff, prod_subset_iff]
  refine exists_congr fun _ => Iff.rfl.and <| Iff.trans ?_ exists_mem_subset_iff
  exact exists_congr fun _ => Iff.rfl.and forall₂_swap

Characterization of Membership in Product Filter via Left Component

Informal description

For any set $s \subseteq \alpha \times \beta$, $s$ belongs to the product filter $f \timesˢ g$ if and only if there exists a set $t \in f$ such that for all $y$ eventually in $g$ and for all $x \in t$, the pair $(x, y)$ belongs to $s$.

Filter.mem_prod_iff_right theorem

{s : Set (α × β)} : s ∈ f ×ˢ g ↔ ∃ t ∈ g, ∀ᶠ x in f, ∀ y ∈ t, (x, y) ∈ s

Full source

theorem mem_prod_iff_right {s : Set (α × β)} :
    s ∈ f ×ˢ gs ∈ f ×ˢ g ↔ ∃ t ∈ g, ∀ᶠ x in f, ∀ y ∈ t, (x, y) ∈ s := by
  rw [prod_comm, mem_map, mem_prod_iff_left]; rfl

Characterization of Membership in Product Filter via Right Component

Informal description

For any set $s \subseteq \alpha \times \beta$, $s$ belongs to the product filter $f \timesˢ g$ if and only if there exists a set $t \in g$ such that for all $x$ eventually in $f$ and for all $y \in t$, the pair $(x, y)$ belongs to $s$.

Filter.map_fst_prod theorem

(f : Filter α) (g : Filter β) [NeBot g] : map Prod.fst (f ×ˢ g) = f

Full source

@[simp]
theorem map_fst_prod (f : Filter α) (g : Filter β) [NeBot g] : map Prod.fst (f ×ˢ g) = f := by
  ext s
  simp only [mem_map, mem_prod_iff_left, mem_preimage, eventually_const, ← subset_def,
    exists_mem_subset_iff]

Projection of Product Filter onto First Component

Informal description

For any filter $f$ on a type $\alpha$ and any non-trivial filter $g$ on a type $\beta$, the image filter of the product filter $f \timesˢ g$ under the first projection map $\mathrm{fst} : \alpha \times \beta \to \alpha$ is equal to $f$.

Filter.map_snd_prod theorem

(f : Filter α) (g : Filter β) [NeBot f] : map Prod.snd (f ×ˢ g) = g

Full source

@[simp]
theorem map_snd_prod (f : Filter α) (g : Filter β) [NeBot f] : map Prod.snd (f ×ˢ g) = g := by
  rw [prod_comm, map_map]; apply map_fst_prod

Projection of Product Filter onto Second Component

Informal description

For any filter $f$ on a type $\alpha$ and any non-trivial filter $g$ on a type $\beta$, the image filter of the product filter $f \timesˢ g$ under the second projection map $\mathrm{snd} : \alpha \times \beta \to \beta$ is equal to $g$.

Filter.prod_le_prod theorem

 {f₁ f₂ : Filter α} {g₁ g₂ : Filter β} [NeBot f₁] [NeBot g₁] : f₁ ×ˢ g₁ ≤ f₂ ×ˢ g₂ ↔ f₁ ≤ f₂ ∧ g₁ ≤ g₂

Full source

@[simp]
theorem prod_le_prod {f₁ f₂ : Filter α} {g₁ g₂ : Filter β} [NeBot f₁] [NeBot g₁] :
    f₁ ×ˢ g₁ ≤ f₂ ×ˢ g₂ ↔ f₁ ≤ f₂ ∧ g₁ ≤ g₂ :=
  ⟨fun h =>
    ⟨map_fst_prod f₁ g₁ ▸ tendsto_fst.mono_left h, map_snd_prod f₁ g₁ ▸ tendsto_snd.mono_left h⟩,
    fun h => prod_mono h.1 h.2⟩

Product Filter Order Comparison: $f_1 \timesˢ g_1 \leq f_2 \timesˢ g_2 \leftrightarrow f_1 \leq f_2 \land g_1 \leq g_2$

Informal description

For any non-trivial filters $f_1, f_2$ on a type $\alpha$ and $g_1, g_2$ on a type $\beta$, the product filter $f_1 \timesˢ g_1$ is less than or equal to $f_2 \timesˢ g_2$ if and only if $f_1 \leq f_2$ and $g_1 \leq g_2$.

Filter.prod_inj theorem

 {f₁ f₂ : Filter α} {g₁ g₂ : Filter β} [NeBot f₁] [NeBot g₁] : f₁ ×ˢ g₁ = f₂ ×ˢ g₂ ↔ f₁ = f₂ ∧ g₁ = g₂

Full source

@[simp]
theorem prod_inj {f₁ f₂ : Filter α} {g₁ g₂ : Filter β} [NeBot f₁] [NeBot g₁] :
    f₁ ×ˢ g₁ = f₂ ×ˢ g₂ ↔ f₁ = f₂ ∧ g₁ = g₂ := by
  refine ⟨fun h => ?_, fun h => h.1 ▸ h.2 ▸ rfl⟩
  have hle : f₁ ≤ f₂ ∧ g₁ ≤ g₂ := prod_le_prod.1 h.le
  haveI := neBot_of_le hle.1; haveI := neBot_of_le hle.2
  exact ⟨hle.1.antisymm <| (prod_le_prod.1 h.ge).1, hle.2.antisymm <| (prod_le_prod.1 h.ge).2⟩

Injectivity of Product Filter Construction: $f_1 \timesˢ g_1 = f_2 \timesˢ g_2 \leftrightarrow f_1 = f_2 \land g_1 = g_2$

Informal description

For any non-trivial filters $f_1, f_2$ on a type $\alpha$ and $g_1, g_2$ on a type $\beta$, the product filters $f_1 \timesˢ g_1$ and $f_2 \timesˢ g_2$ are equal if and only if $f_1 = f_2$ and $g_1 = g_2$.

Filter.eventually_swap_iff theorem

{p : α × β → Prop} : (∀ᶠ x : α × β in f ×ˢ g, p x) ↔ ∀ᶠ y : β × α in g ×ˢ f, p y.swap

Full source

theorem eventually_swap_iff {p : α × β → Prop} :
    (∀ᶠ x : α × β in f ×ˢ g, p x) ↔ ∀ᶠ y : β × α in g ×ˢ f, p y.swap := by
  rw [prod_comm]; rfl

Equivalence of Eventual Properties under Filter Product Swap

Informal description

For any predicate $p : \alpha \times \beta \to \text{Prop}$ and filters $f$ on $\alpha$ and $g$ on $\beta$, the property $p$ holds eventually in the product filter $f \timesˢ g$ if and only if the swapped property $p \circ \text{swap}$ holds eventually in the product filter $g \timesˢ f$. In symbols: $$ (\forallᶠ x \text{ in } f \timesˢ g, p x) \leftrightarrow (\forallᶠ y \text{ in } g \timesˢ f, p(y.\text{swap})). $$

Filter.prod_assoc theorem

 (f : Filter α) (g : Filter β) (h : Filter γ) : map (Equiv.prodAssoc α β γ) ((f ×ˢ g) ×ˢ h) = f ×ˢ (g ×ˢ h)

Full source

theorem prod_assoc (f : Filter α) (g : Filter β) (h : Filter γ) :
    map (Equiv.prodAssoc α β γ) ((f ×ˢ g) ×ˢ h) = f ×ˢ (g ×ˢ h) := by
  simp_rw [← comap_equiv_symm, prod_eq_inf, comap_inf, comap_comap, inf_assoc,
    Function.comp_def, Equiv.prodAssoc_symm_apply]

Associativity of Filter Product under Associativity Equivalence

Informal description

For any filters $f$ on a type $\alpha$, $g$ on a type $\beta$, and $h$ on a type $\gamma$, the image filter of the product filter $(f \timesˢ g) \timesˢ h$ under the associativity equivalence $\text{Equiv.prodAssoc} \colon (\alpha \times \beta) \times \gamma \simeq \alpha \times (\beta \times \gamma)$ is equal to the product filter $f \timesˢ (g \timesˢ h)$. In other words, the following diagram commutes: \[ \text{map } \text{Equiv.prodAssoc} \big( (f \timesˢ g) \timesˢ h \big) = f \timesˢ (g \timesˢ h). \]

Filter.prod_assoc_symm theorem

 (f : Filter α) (g : Filter β) (h : Filter γ) : map (Equiv.prodAssoc α β γ).symm (f ×ˢ (g ×ˢ h)) = (f ×ˢ g) ×ˢ h

Full source

theorem prod_assoc_symm (f : Filter α) (g : Filter β) (h : Filter γ) :
    map (Equiv.prodAssoc α β γ).symm (f ×ˢ (g ×ˢ h)) = (f ×ˢ g) ×ˢ h := by
  simp_rw [map_equiv_symm, prod_eq_inf, comap_inf, comap_comap, inf_assoc,
    Function.comp_def, Equiv.prodAssoc_apply]

Inverse Associativity of Filter Products: $\text{map } \text{prodAssoc}^{-1} (f \timesˢ (g \timesˢ h)) = (f \timesˢ g) \timesˢ h$

Informal description

For any filters $f$ on a type $\alpha$, $g$ on a type $\beta$, and $h$ on a type $\gamma$, the image filter of the product filter $f \timesˢ (g \timesˢ h)$ under the inverse associativity equivalence $(\alpha \times \beta \times \gamma) \simeq ((\alpha \times \beta) \times \gamma)$ is equal to the product filter $(f \timesˢ g) \timesˢ h$. In other words, the following diagram commutes: \[ \text{map } (\text{Equiv.prodAssoc } \alpha \beta \gamma)^{-1} \big( f \timesˢ (g \timesˢ h) \big) = (f \timesˢ g) \timesˢ h. \]

Filter.tendsto_prodAssoc theorem

{h : Filter γ} : Tendsto (Equiv.prodAssoc α β γ) ((f ×ˢ g) ×ˢ h) (f ×ˢ (g ×ˢ h))

Full source

theorem tendsto_prodAssoc {h : Filter γ} :
    Tendsto (Equiv.prodAssoc α β γ) ((f ×ˢ g) ×ˢ h) (f ×ˢ (g ×ˢ h)) :=
  (prod_assoc f g h).le

Limit Preservation under Associativity Equivalence for Filter Products

Informal description

For any filters $f$ on a type $\alpha$, $g$ on a type $\beta$, and $h$ on a type $\gamma$, the associativity equivalence $\text{Equiv.prodAssoc} \colon (\alpha \times \beta) \times \gamma \simeq \alpha \times (\beta \times \gamma)$ induces a limit-preserving map from the product filter $(f \timesˢ g) \timesˢ h$ to the product filter $f \timesˢ (g \timesˢ h)$. In other words, the function $\text{Equiv.prodAssoc}$ satisfies: \[ \text{Tendsto } \text{Equiv.prodAssoc} \big( (f \timesˢ g) \timesˢ h \big) \big( f \timesˢ (g \timesˢ h) \big). \]

Filter.tendsto_prodAssoc_symm theorem

{h : Filter γ} : Tendsto (Equiv.prodAssoc α β γ).symm (f ×ˢ (g ×ˢ h)) ((f ×ˢ g) ×ˢ h)

Full source

theorem tendsto_prodAssoc_symm {h : Filter γ} :
    Tendsto (Equiv.prodAssoc α β γ).symm (f ×ˢ (g ×ˢ h)) ((f ×ˢ g) ×ˢ h) :=
  (prod_assoc_symm f g h).le

Limit Preservation under Inverse Associativity Equivalence for Filter Products

Informal description

For any filters $f$ on a type $\alpha$, $g$ on a type $\beta$, and $h$ on a type $\gamma$, the inverse associativity equivalence $(\alpha \times \beta \times \gamma) \simeq ((\alpha \times \beta) \times \gamma)$ preserves limits in the sense that it maps the product filter $f \timesˢ (g \timesˢ h)$ to the product filter $(f \timesˢ g) \timesˢ h$. In other words, the following limit relation holds: \[ \text{Tendsto } (\text{Equiv.prodAssoc } \alpha \beta \gamma)^{-1} \big( f \timesˢ (g \timesˢ h) \big) \big( (f \timesˢ g) \timesˢ h \big). \]

Filter.map_swap4_prod theorem

 {h : Filter γ} {k : Filter δ} :
  map (fun p : (α × β) × γ × δ => ((p.1.1, p.2.1), (p.1.2, p.2.2))) ((f ×ˢ g) ×ˢ (h ×ˢ k)) = (f ×ˢ h) ×ˢ (g ×ˢ k)

Full source

/-- A useful lemma when dealing with uniformities. -/
theorem map_swap4_prod {h : Filter γ} {k : Filter δ} :
    map (fun p : (α × β) × γ × δ => ((p.1.1, p.2.1), (p.1.2, p.2.2))) ((f ×ˢ g) ×ˢ (h ×ˢ k)) =
      (f ×ˢ h) ×ˢ (g ×ˢ k) := by
  simp_rw [map_swap4_eq_comap, prod_eq_inf, comap_inf, comap_comap]; ac_rfl

Image of Product Filter under Component Swapping Equals Swapped Product Filter

Informal description

For any filters $f$ on type $\alpha$, $g$ on type $\beta$, $h$ on type $\gamma$, and $k$ on type $\delta$, the image filter under the component-swapping function \[ p \mapsto ((p_{1,1}, p_{2,1}), (p_{1,2}, p_{2,2})) \] applied to the product filter $(f \timesˢ g) \timesˢ (h \timesˢ k)$ is equal to the product filter $(f \timesˢ h) \timesˢ (g \timesˢ k)$.

Filter.tendsto_swap4_prod theorem

 {h : Filter γ} {k : Filter δ} :
  Tendsto (fun p : (α × β) × γ × δ => ((p.1.1, p.2.1), (p.1.2, p.2.2))) ((f ×ˢ g) ×ˢ (h ×ˢ k)) ((f ×ˢ h) ×ˢ (g ×ˢ k))

Full source

theorem tendsto_swap4_prod {h : Filter γ} {k : Filter δ} :
    Tendsto (fun p : (α × β) × γ × δ => ((p.1.1, p.2.1), (p.1.2, p.2.2))) ((f ×ˢ g) ×ˢ (h ×ˢ k))
      ((f ×ˢ h) ×ˢ (g ×ˢ k)) :=
  map_swap4_prod.le

Component-Swapping Function Preserves Filter Products

Informal description

For any filters $f$ on type $\alpha$, $g$ on type $\beta$, $h$ on type $\gamma$, and $k$ on type $\delta$, the function that swaps components as \[ ((x, y), (z, w)) \mapsto ((x, z), (y, w)) \] maps the product filter $(f \timesˢ g) \timesˢ (h \timesˢ k)$ to the product filter $(f \timesˢ h) \timesˢ (g \timesˢ k)$.

Filter.prod_map_map_eq theorem

 {α₁ : Type u} {α₂ : Type v} {β₁ : Type w} {β₂ : Type x} {f₁ : Filter α₁} {f₂ : Filter α₂} {m₁ : α₁ → β₁}
  {m₂ : α₂ → β₂} : map m₁ f₁ ×ˢ map m₂ f₂ = map (fun p : α₁ × α₂ => (m₁ p.1, m₂ p.2)) (f₁ ×ˢ f₂)

Full source

theorem prod_map_map_eq.{u, v, w, x} {α₁ : Type u} {α₂ : Type v} {β₁ : Type w} {β₂ : Type x}
    {f₁ : Filter α₁} {f₂ : Filter α₂} {m₁ : α₁ → β₁} {m₂ : α₂ → β₂} :
    map m₁ f₁ ×ˢ map m₂ f₂ = map (fun p : α₁ × α₂ => (m₁ p.1, m₂ p.2)) (f₁ ×ˢ f₂) :=
  le_antisymm
    (fun s hs =>
      let ⟨s₁, hs₁, s₂, hs₂, h⟩ := mem_prod_iff.mp hs
      mem_of_superset (prod_mem_prod (image_mem_map hs₁) (image_mem_map hs₂)) <|
        by rwa [prod_image_image_eq, image_subset_iff])
    ((tendsto_map.comp tendsto_fst).prodMk (tendsto_map.comp tendsto_snd))

Equality of Product of Image Filters and Image of Product Filter under Component-wise Mapping

Informal description

For any types $\alpha_1, \alpha_2, \beta_1, \beta_2$, filters $f_1$ on $\alpha_1$ and $f_2$ on $\alpha_2$, and functions $m_1: \alpha_1 \to \beta_1$ and $m_2: \alpha_2 \to \beta_2$, the product filter of the image filters $\text{map } m_1 f_1$ and $\text{map } m_2 f_2$ is equal to the image filter of the product filter $f_1 \timesˢ f_2$ under the component-wise mapping $(x,y) \mapsto (m_1(x), m_2(y))$. In symbols: \[ \text{map } m_1 f_1 \timesˢ \text{map } m_2 f_2 = \text{map } \big((x,y) \mapsto (m_1(x), m_2(y))\big) (f_1 \timesˢ f_2) \]

Filter.prod_map_map_eq' theorem

 {α₁ : Type*} {α₂ : Type*} {β₁ : Type*} {β₂ : Type*} (f : α₁ → α₂) (g : β₁ → β₂) (F : Filter α₁) (G : Filter β₁) :
  map f F ×ˢ map g G = map (Prod.map f g) (F ×ˢ G)

Full source

theorem prod_map_map_eq' {α₁ : Type*} {α₂ : Type*} {β₁ : Type*} {β₂ : Type*} (f : α₁ → α₂)
    (g : β₁ → β₂) (F : Filter α₁) (G : Filter β₁) :
    map f F ×ˢ map g G = map (Prod.map f g) (F ×ˢ G) :=
  prod_map_map_eq

Equality of Product of Image Filters and Image of Product Filter under Component-wise Mapping (Primed Version)

Informal description

For any types $\alpha_1, \alpha_2, \beta_1, \beta_2$, functions $f : \alpha_1 \to \alpha_2$ and $g : \beta_1 \to \beta_2$, and filters $F$ on $\alpha_1$ and $G$ on $\beta_1$, the product filter of the image filters $\text{map } f F$ and $\text{map } g G$ is equal to the image filter of the product filter $F \timesˢ G$ under the component-wise mapping $(x,y) \mapsto (f(x), g(y))$. In symbols: \[ \text{map } f F \timesˢ \text{map } g G = \text{map } (f \times g) (F \timesˢ G) \]

Filter.prod_map_left theorem

(f : α → β) (F : Filter α) (G : Filter γ) : map f F ×ˢ G = map (Prod.map f id) (F ×ˢ G)

Full source

theorem prod_map_left (f : α → β) (F : Filter α) (G : Filter γ) :
    map f F ×ˢ G = map (Prod.map f id) (F ×ˢ G) := by
  rw [← prod_map_map_eq', map_id]

Equality of Product Filter with Left Image Filter and Image of Product Filter under Left Component-wise Mapping

Informal description

For any function $f : \alpha \to \beta$ and filters $F$ on $\alpha$ and $G$ on $\gamma$, the product filter of the image filter $\text{map } f F$ and $G$ is equal to the image filter of the product filter $F \timesˢ G$ under the mapping $(x, y) \mapsto (f(x), y)$. In symbols: \[ \text{map } f F \timesˢ G = \text{map } (f \times \text{id}) (F \timesˢ G) \]

Filter.prod_map_right theorem

(f : β → γ) (F : Filter α) (G : Filter β) : F ×ˢ map f G = map (Prod.map id f) (F ×ˢ G)

Full source

theorem prod_map_right (f : β → γ) (F : Filter α) (G : Filter β) :
    F ×ˢ map f G = map (Prod.map id f) (F ×ˢ G) := by
  rw [← prod_map_map_eq', map_id]

Right Component Mapping Preserves Product Filter

Informal description

For any function $f : \beta \to \gamma$ and filters $F$ on $\alpha$ and $G$ on $\beta$, the product filter $F \timesˢ \text{map } f G$ is equal to the image filter of the product filter $F \timesˢ G$ under the mapping $(x, y) \mapsto (x, f(y))$. In symbols: \[ F \timesˢ \text{map } f G = \text{map } (\text{id} \times f) (F \timesˢ G) \]

Filter.le_prod_map_fst_snd theorem

{f : Filter (α × β)} : f ≤ map Prod.fst f ×ˢ map Prod.snd f

Full source

theorem le_prod_map_fst_snd {f : Filter (α × β)} : f ≤ map Prod.fst f ×ˢ map Prod.snd f :=
  le_inf le_comap_map le_comap_map

Filter Containment in Product of Projection Filters

Informal description

For any filter $f$ on the product type $\alpha \times \beta$, the filter $f$ is contained in the product filter formed by the image of $f$ under the first projection $\text{map } \text{Prod.fst } f$ and the image of $f$ under the second projection $\text{map } \text{Prod.snd } f$. In symbols: \[ f \leq (\text{map } \pi_1 f) \timesˢ (\text{map } \pi_2 f) \] where $\pi_1$ and $\pi_2$ denote the first and second projections respectively.

Filter.Tendsto.prodMap theorem

 {δ : Type*} {f : α → γ} {g : β → δ} {a : Filter α} {b : Filter β} {c : Filter γ} {d : Filter δ} (hf : Tendsto f a c)
  (hg : Tendsto g b d) : Tendsto (Prod.map f g) (a ×ˢ b) (c ×ˢ d)

Full source

theorem Tendsto.prodMap {δ : Type*} {f : α → γ} {g : β → δ} {a : Filter α} {b : Filter β}
    {c : Filter γ} {d : Filter δ} (hf : Tendsto f a c) (hg : Tendsto g b d) :
    Tendsto (Prod.map f g) (a ×ˢ b) (c ×ˢ d) := by
  rw [Tendsto, Prod.map_def, ← prod_map_map_eq]
  exact Filter.prod_mono hf hg

Tendsto of Product Map under Product Filters

Informal description

Let $f : \alpha \to \gamma$ and $g : \beta \to \delta$ be functions, and let $a$ be a filter on $\alpha$, $b$ a filter on $\beta$, $c$ a filter on $\gamma$, and $d$ a filter on $\delta$. If $f$ tends to $c$ along $a$ and $g$ tends to $d$ along $b$, then the product map $(x,y) \mapsto (f(x), g(y))$ tends to the product filter $c \timesˢ d$ along the product filter $a \timesˢ b$.

Filter.map_prod theorem

(m : α × β → γ) (f : Filter α) (g : Filter β) : map m (f ×ˢ g) = (f.map fun a b => m (a, b)).seq g

Full source

protected theorem map_prod (m : α × β → γ) (f : Filter α) (g : Filter β) :
    map m (f ×ˢ g) = (f.map fun a b => m (a, b)).seq g := by
  simp only [Filter.ext_iff, mem_map, mem_prod_iff, mem_map_seq_iff, exists_and_left]
  intro s
  constructor
  · exact fun ⟨t, ht, s, hs, h⟩ => ⟨s, hs, t, ht, fun x hx y hy => @h ⟨x, y⟩ ⟨hx, hy⟩⟩
  · exact fun ⟨s, hs, t, ht, h⟩ => ⟨t, ht, s, hs, fun ⟨x, y⟩ ⟨hx, hy⟩ => h x hx y hy⟩

Image of Product Filter under a Function Equals Sequential Composition of Mapped Filters

Informal description

For any function $m : \alpha \times \beta \to \gamma$ and filters $f$ on $\alpha$ and $g$ on $\beta$, the image filter of the product filter $f \timesˢ g$ under $m$ is equal to the sequential composition of the filter obtained by mapping the curried function $\lambda a \, b, m(a, b)$ through $f$ with the filter $g$. In symbols: \[ \text{map } m (f \timesˢ g) = (\text{map } (\lambda a \, b, m(a, b)) f) \text{ seq } g \]

Filter.prod_eq theorem

: f ×ˢ g = (f.map Prod.mk).seq g

Full source

theorem prod_eq : f ×ˢ g = (f.map Prod.mk).seq g := f.map_prod id g

Product Filter as Sequential Composition of Mapped Pairing Function

Informal description

For any filters $f$ on type $\alpha$ and $g$ on type $\beta$, the product filter $f \timesˢ g$ on $\alpha \times \beta$ is equal to the sequential composition of the filter obtained by mapping the pairing function $\lambda a, (a, \cdot)$ through $f$ with the filter $g$. In symbols: \[ f \timesˢ g = (\text{map } (\lambda a b, (a, b)) f) \text{ seq } g \]

Filter.prod_inf_prod theorem

 {f₁ f₂ : Filter α} {g₁ g₂ : Filter β} : (f₁ ×ˢ g₁) ⊓ (f₂ ×ˢ g₂) = (f₁ ⊓ f₂) ×ˢ (g₁ ⊓ g₂)

Full source

theorem prod_inf_prod {f₁ f₂ : Filter α} {g₁ g₂ : Filter β} :
    (f₁ ×ˢ g₁) ⊓ (f₂ ×ˢ g₂) = (f₁ ⊓ f₂) ×ˢ (g₁ ⊓ g₂) := by
  simp only [prod_eq_inf, comap_inf, inf_comm, inf_assoc, inf_left_comm]

Infimum of Product Filters Equals Product of Infima

Informal description

For any filters $f_1, f_2$ on a type $\alpha$ and $g_1, g_2$ on a type $\beta$, the infimum of the product filters $f_1 \timesˢ g_1$ and $f_2 \timesˢ g_2$ equals the product filter of the infima $(f_1 \sqcap f_2) \timesˢ (g_1 \sqcap g_2)$. In symbols: $$ (f_1 \timesˢ g_1) \sqcap (f_2 \timesˢ g_2) = (f_1 \sqcap f_2) \timesˢ (g_1 \sqcap g_2) $$

Filter.inf_prod theorem

{f₁ f₂ : Filter α} : (f₁ ⊓ f₂) ×ˢ g = (f₁ ×ˢ g) ⊓ (f₂ ×ˢ g)

Full source

theorem inf_prod {f₁ f₂ : Filter α} : (f₁ ⊓ f₂) ×ˢ g = (f₁ ×ˢ g) ⊓ (f₂ ×ˢ g) := by
  rw [prod_inf_prod, inf_idem]

Distributivity of Product Filter over Infimum: $(f_1 \sqcap f_2) \timesˢ g = (f_1 \timesˢ g) \sqcap (f_2 \timesˢ g)$

Informal description

For any filters $f_1, f_2$ on a type $\alpha$ and any filter $g$ on a type $\beta$, the product filter of the infimum $f_1 \sqcap f_2$ with $g$ is equal to the infimum of the product filters $f_1 \timesˢ g$ and $f_2 \timesˢ g$. In symbols: $$ (f_1 \sqcap f_2) \timesˢ g = (f_1 \timesˢ g) \sqcap (f_2 \timesˢ g) $$

Filter.prod_inf theorem

{g₁ g₂ : Filter β} : f ×ˢ (g₁ ⊓ g₂) = (f ×ˢ g₁) ⊓ (f ×ˢ g₂)

Full source

theorem prod_inf {g₁ g₂ : Filter β} : f ×ˢ (g₁ ⊓ g₂) = (f ×ˢ g₁) ⊓ (f ×ˢ g₂) := by
  rw [prod_inf_prod, inf_idem]

Distributivity of Product Filter over Infimum: $f \timesˢ (g_1 \sqcap g_2) = (f \timesˢ g_1) \sqcap (f \timesˢ g_2)$

Informal description

For any filter $f$ on a type $\alpha$ and any filters $g_1, g_2$ on a type $\beta$, the product filter $f \timesˢ (g_1 \sqcap g_2)$ is equal to the infimum of the product filters $(f \timesˢ g_1) \sqcap (f \timesˢ g_2)$. In symbols: $$ f \timesˢ (g_1 \sqcap g_2) = (f \timesˢ g_1) \sqcap (f \timesˢ g_2) $$

Filter.prod_principal_principal theorem

{s : Set α} {t : Set β} : 𝓟 s ×ˢ 𝓟 t = 𝓟 (s ×ˢ t)

Full source

@[simp]
theorem prod_principal_principal {s : Set α} {t : Set β} : 𝓟 s ×ˢ 𝓟 t = 𝓟 (s ×ˢ t) := by
  simp only [prod_eq_inf, comap_principal, principal_eq_iff_eq, comap_principal, inf_principal]; rfl

Product of Principal Filters is Principal Filter of Product Sets

Informal description

For any sets $s \subseteq \alpha$ and $t \subseteq \beta$, the product filter of the principal filters generated by $s$ and $t$ is equal to the principal filter generated by the Cartesian product $s \times t$. In symbols: \[ \mathcal{P}(s) \timesˢ \mathcal{P}(t) = \mathcal{P}(s \times t) \]

Filter.pure_prod theorem

{a : α} {f : Filter β} : pure a ×ˢ f = map (Prod.mk a) f

Full source

@[simp]
theorem pure_prod {a : α} {f : Filter β} : pure a ×ˢ f = map (Prod.mk a) f := by
  rw [prod_eq, map_pure, pure_seq_eq_map]

Product of Pure Filter with Another Filter Equals Image of Pairing Function

Informal description

For any element $a \in \alpha$ and any filter $f$ on $\beta$, the product filter $\text{pure } a \timesˢ f$ is equal to the image filter of $f$ under the function $\lambda b, (a, b)$. In symbols: $$\text{pure } a \timesˢ f = \text{map } (\lambda b, (a, b)) f$$

Filter.map_pure_prod theorem

(f : α → β → γ) (a : α) (B : Filter β) : map (Function.uncurry f) (pure a ×ˢ B) = map (f a) B

Full source

theorem map_pure_prod (f : α → β → γ) (a : α) (B : Filter β) :
    map (Function.uncurry f) (pure a ×ˢ B) = map (f a) B := by
  rw [Filter.pure_prod]; rfl

Image of Product Filter under Uncurried Function Equals Image under Partial Application

Informal description

For any function $f : \alpha \to \beta \to \gamma$, any element $a \in \alpha$, and any filter $B$ on $\beta$, the image filter of the product filter $\text{pure } a \timesˢ B$ under the uncurried function $\text{Function.uncurry } f$ is equal to the image filter of $B$ under $f(a)$. In symbols: $$\text{map } (\text{Function.uncurry } f) (\text{pure } a \timesˢ B) = \text{map } (f a) B$$

Filter.prod_pure theorem

{b : β} : f ×ˢ pure b = map (fun a => (a, b)) f

Full source

@[simp]
theorem prod_pure {b : β} : f ×ˢ pure b = map (fun a => (a, b)) f := by
  rw [prod_eq, seq_pure, map_map]; rfl

Product Filter with Principal Filter Equals Pairing Map

Informal description

For any filter $f$ on a type $\alpha$ and any element $b$ in a type $\beta$, the product filter $f \timesˢ \text{pure } b$ is equal to the image filter of $f$ under the function $\lambda a, (a, b)$. In other words, the product of a filter $f$ with the principal filter generated by a singleton $\{b\}$ is the same as mapping each element $a$ in $f$ to the pair $(a, b)$.

Filter.prod_pure_pure theorem

{a : α} {b : β} : (pure a : Filter α) ×ˢ (pure b : Filter β) = pure (a, b)

Full source

theorem prod_pure_pure {a : α} {b : β} :
    (pure a : Filter α) ×ˢ (pure b : Filter β) = pure (a, b) := by simp

Product of Principal Filters is Principal Filter of Pair

Informal description

For any elements $a$ in a type $\alpha$ and $b$ in a type $\beta$, the product filter of the principal filters generated by $\{a\}$ and $\{b\}$ is equal to the principal filter generated by the pair $(a, b)$. In other words, $\mathcal{P}\{a\} \timesˢ \mathcal{P}\{b\} = \mathcal{P}\{(a, b)\}$.

Filter.prod_eq_bot theorem

: f ×ˢ g = ⊥ ↔ f = ⊥ ∨ g = ⊥

Full source

@[simp]
theorem prod_eq_bot : f ×ˢ g = ⊥ ↔ f = ⊥ ∨ g = ⊥ := by
  simp_rw [← empty_mem_iff_bot, mem_prod_iff, subset_empty_iff, prod_eq_empty_iff, ← exists_prop,
    Subtype.exists', exists_or, exists_const, Subtype.exists, exists_prop, exists_eq_right]

Product Filter is Bottom if and only if One Component is Bottom

Informal description

The product filter $f \timesˢ g$ is equal to the bottom filter $\bot$ if and only if either $f$ is the bottom filter or $g$ is the bottom filter.

Filter.prod_bot theorem

: f ×ˢ (⊥ : Filter β) = ⊥

Full source

@[simp] theorem prod_bot : f ×ˢ (⊥ : Filter β) = ⊥ := prod_eq_bot.2 <| Or.inr rfl

Product with Bottom Filter Yields Bottom Filter

Informal description

For any filter $f$ on a type $\alpha$, the product filter $f \timesˢ \bot$ is equal to the bottom filter $\bot$, where $\bot$ is the bottom filter on a type $\beta$.

Filter.bot_prod theorem

: (⊥ : Filter α) ×ˢ g = ⊥

Full source

@[simp] theorem bot_prod : (⊥ : Filter α) ×ˢ g = ⊥ := prod_eq_bot.2 <| Or.inl rfl

Bottom Filter is Left Annihilator for Product Filter

Informal description

The product of the bottom filter on a type $\alpha$ with any filter $g$ on a type $\beta$ is equal to the bottom filter on $\alpha \times \beta$, i.e., $\bot \timesˢ g = \bot$.

Filter.prod_neBot theorem

: NeBot (f ×ˢ g) ↔ NeBot f ∧ NeBot g

Full source

theorem prod_neBot : NeBotNeBot (f ×ˢ g) ↔ NeBot f ∧ NeBot g := by
  simp only [neBot_iff, Ne, prod_eq_bot, not_or]

Non-triviality of Product Filter: $f \timesˢ g \neq \bot \leftrightarrow f \neq \bot \land g \neq \bot$

Informal description

The product filter $f \timesˢ g$ is non-trivial if and only if both filters $f$ and $g$ are non-trivial.

Filter.NeBot.prod theorem

(hf : NeBot f) (hg : NeBot g) : NeBot (f ×ˢ g)

Full source

protected theorem NeBot.prod (hf : NeBot f) (hg : NeBot g) : NeBot (f ×ˢ g) := prod_neBot.2 ⟨hf, hg⟩

Product of Non-trivial Filters is Non-trivial

Informal description

If $f$ and $g$ are non-trivial filters on types $\alpha$ and $\beta$ respectively, then their product filter $f \timesˢ g$ on $\alpha \times \beta$ is also non-trivial.

Filter.prod.instNeBot instance

[hf : NeBot f] [hg : NeBot g] : NeBot (f ×ˢ g)

Full source

instance prod.instNeBot [hf : NeBot f] [hg : NeBot g] : NeBot (f ×ˢ g) := hf.prod hg

Product of Non-trivial Filters is Non-trivial

Informal description

For any two non-trivial filters $f$ on type $\alpha$ and $g$ on type $\beta$, their product filter $f \timesˢ g$ on $\alpha \times \beta$ is also non-trivial.

Filter.disjoint_prod theorem

{f' : Filter α} {g' : Filter β} : Disjoint (f ×ˢ g) (f' ×ˢ g') ↔ Disjoint f f' ∨ Disjoint g g'

Full source

@[simp]
lemma disjoint_prod {f' : Filter α} {g' : Filter β} :
    DisjointDisjoint (f ×ˢ g) (f' ×ˢ g') ↔ Disjoint f f' ∨ Disjoint g g' := by
  simp only [disjoint_iff, prod_inf_prod, prod_eq_bot]

Disjointness of Product Filters is Equivalent to Disjointness of Components

Informal description

For any filters $f, f'$ on a type $\alpha$ and $g, g'$ on a type $\beta$, the product filters $f \timesˢ g$ and $f' \timesˢ g'$ are disjoint if and only if either $f$ and $f'$ are disjoint or $g$ and $g'$ are disjoint. In symbols: $$ \text{Disjoint}(f \timesˢ g, f' \timesˢ g') \leftrightarrow \text{Disjoint}(f, f') \lor \text{Disjoint}(g, g') $$

Filter.frequently_prod_and theorem

 {p : α → Prop} {q : β → Prop} : (∃ᶠ x in f ×ˢ g, p x.1 ∧ q x.2) ↔ (∃ᶠ a in f, p a) ∧ ∃ᶠ b in g, q b

Full source

/-- `p ∧ q` occurs frequently along the product of two filters
iff both `p` and `q` occur frequently along the corresponding filters. -/
theorem frequently_prod_and {p : α → Prop} {q : β → Prop} :
    (∃ᶠ x in f ×ˢ g, p x.1 ∧ q x.2) ↔ (∃ᶠ a in f, p a) ∧ ∃ᶠ b in g, q b := by
  simp only [frequently_iff_neBot, ← prod_neBot, ← prod_inf_prod, prod_principal_principal]
  rfl

Frequent Occurrence of Conjunction in Product Filter iff Frequent in Components

Informal description

For any predicates $p : \alpha \to \text{Prop}$ and $q : \beta \to \text{Prop}$, and filters $f$ on $\alpha$ and $g$ on $\beta$, the following are equivalent: 1. The property $p(x) \land q(y)$ holds frequently in the product filter $f \timesˢ g$. 2. The property $p$ holds frequently in $f$ and $q$ holds frequently in $g$. In symbols: \[ \existsᶠ (x,y) \text{ in } f \timesˢ g, \, p(x) \land q(y) \quad \leftrightarrow \quad (\existsᶠ x \text{ in } f, \, p(x)) \land (\existsᶠ y \text{ in } g, \, q(y)) \]

Filter.tendsto_prod_iff theorem

 {f : α × β → γ} {x : Filter α} {y : Filter β} {z : Filter γ} :
  Tendsto f (x ×ˢ y) z ↔ ∀ W ∈ z, ∃ U ∈ x, ∃ V ∈ y, ∀ x y, x ∈ U → y ∈ V → f (x, y) ∈ W

Full source

theorem tendsto_prod_iff {f : α × β → γ} {x : Filter α} {y : Filter β} {z : Filter γ} :
    TendstoTendsto f (x ×ˢ y) z ↔ ∀ W ∈ z, ∃ U ∈ x, ∃ V ∈ y, ∀ x y, x ∈ U → y ∈ V → f (x, y) ∈ W := by
  simp only [tendsto_def, mem_prod_iff, prod_sub_preimage_iff, exists_prop]

Characterization of Tendsto for Product Filters: $f$ tends to $z$ in $x \timesˢ y$ iff for all $W \in z$, there exist $U \in x$ and $V \in y$ mapping into $W$

Informal description

For a function $f : \alpha \times \beta \to \gamma$ and filters $x$ on $\alpha$, $y$ on $\beta$, and $z$ on $\gamma$, the following are equivalent: 1. The function $f$ tends to $z$ with respect to the product filter $x \timesˢ y$. 2. For every set $W \in z$, there exist sets $U \in x$ and $V \in y$ such that for all $x \in U$ and $y \in V$, the image $f(x, y)$ belongs to $W$.

Filter.tendsto_prod_iff' theorem

 {g' : Filter γ} {s : α → β × γ} :
  Tendsto s f (g ×ˢ g') ↔ Tendsto (fun n => (s n).1) f g ∧ Tendsto (fun n => (s n).2) f g'

Full source

theorem tendsto_prod_iff' {g' : Filter γ} {s : α → β × γ} :
    TendstoTendsto s f (g ×ˢ g') ↔ Tendsto (fun n => (s n).1) f g ∧ Tendsto (fun n => (s n).2) f g' := by
  simp only [prod_eq_inf, tendsto_inf, tendsto_comap_iff, Function.comp_def]

Characterization of Convergence to Product Filter via Componentwise Convergence

Informal description

For any function $s : \alpha \to \beta \times \gamma$ and filters $f$ on $\alpha$, $g$ on $\beta$, and $g'$ on $\gamma$, the following are equivalent: 1. The function $s$ tends to the product filter $g \timesˢ g'$ with respect to $f$. 2. The first component function $n \mapsto (s(n)).1$ tends to $g$ with respect to $f$, and the second component function $n \mapsto (s(n)).2$ tends to $g'$ with respect to $f$. In other words, $\lim_{f} s = (g \timesˢ g')$ if and only if $\lim_{f} (\text{pr}_1 \circ s) = g$ and $\lim_{f} (\text{pr}_2 \circ s) = g'$, where $\text{pr}_1$ and $\text{pr}_2$ are the projection maps.

Filter.le_prod theorem

 {f : Filter (α × β)} {g : Filter α} {g' : Filter β} : (f ≤ g ×ˢ g') ↔ Tendsto Prod.fst f g ∧ Tendsto Prod.snd f g'

Full source

theorem le_prod {f : Filter (α × β)} {g : Filter α} {g' : Filter β} :
    (f ≤ g ×ˢ g') ↔ Tendsto Prod.fst f g ∧ Tendsto Prod.snd f g' :=
  tendsto_prod_iff'

Characterization of Filter Refinement via Projection Maps: $f \leq g \timesˢ g'$ iff $\text{pr}_1$ tends to $g$ and $\text{pr}_2$ tends to $g'$ under $f$

Informal description

For any filter $f$ on the product type $\alpha \times \beta$ and filters $g$ on $\alpha$ and $g'$ on $\beta$, the following are equivalent: 1. The filter $f$ is finer than the product filter $g \timesˢ g'$. 2. The projection map $\text{pr}_1 : \alpha \times \beta \to \alpha$ tends to $g$ with respect to $f$, and the projection map $\text{pr}_2 : \alpha \times \beta \to \beta$ tends to $g'$ with respect to $f$. In other words, $f \leq g \timesˢ g'$ if and only if $\lim_{f} \text{pr}_1 = g$ and $\lim_{f} \text{pr}_2 = g'$.

Filter.coprod_eq_prod_top_sup_top_prod theorem

(f : Filter α) (g : Filter β) : Filter.coprod f g = f ×ˢ ⊤ ⊔ ⊤ ×ˢ g

Full source

theorem coprod_eq_prod_top_sup_top_prod (f : Filter α) (g : Filter β) :
    Filter.coprod f g = f ×ˢ ⊤ ⊔ ⊤ ×ˢ g := by
  rw [prod_top, top_prod]
  rfl

Coproduct Filter Decomposition: $\text{coprod } f g = (f \timesˢ \top) \sqcup (\top \timesˢ g)$

Informal description

For any filters $f$ on a type $\alpha$ and $g$ on a type $\beta$, the coproduct filter $\text{coprod } f g$ on $\alpha \times \beta$ is equal to the supremum of the product filter $f \timesˢ \top$ and the product filter $\top \timesˢ g$, where $\top$ denotes the top filter on the respective type.

Filter.mem_coprod_iff theorem

 {s : Set (α × β)} {f : Filter α} {g : Filter β} :
  s ∈ f.coprod g ↔ (∃ t₁ ∈ f, Prod.fst ⁻¹' t₁ ⊆ s) ∧ ∃ t₂ ∈ g, Prod.snd ⁻¹' t₂ ⊆ s

Full source

theorem mem_coprod_iff {s : Set (α × β)} {f : Filter α} {g : Filter β} :
    s ∈ f.coprod gs ∈ f.coprod g ↔ (∃ t₁ ∈ f, Prod.fst ⁻¹' t₁ ⊆ s) ∧ ∃ t₂ ∈ g, Prod.snd ⁻¹' t₂ ⊆ s := by
  simp [Filter.coprod]

Characterization of Membership in Coproduct Filter: $s \in f \mathbin{\text{coprod}} g$ iff $\text{pr}_1^{-1}(t_1) \subseteq s$ and $\text{pr}_2^{-1}(t_2) \subseteq s$ for some $t_1 \in f$, $t_2 \in g$

Informal description

For any set $s \subseteq \alpha \times \beta$ and filters $f$ on $\alpha$ and $g$ on $\beta$, the set $s$ belongs to the coproduct filter $f \mathbin{\text{coprod}} g$ if and only if there exist sets $t_1 \in f$ and $t_2 \in g$ such that the preimage of $t_1$ under the first projection $\text{pr}_1$ is contained in $s$ and the preimage of $t_2$ under the second projection $\text{pr}_2$ is contained in $s$.

Filter.bot_coprod theorem

(l : Filter β) : (⊥ : Filter α).coprod l = comap Prod.snd l

Full source

@[simp]
theorem bot_coprod (l : Filter β) : (⊥ : Filter α).coprod l = comap Prod.snd l := by
  simp [Filter.coprod]

Coproduct with Bottom Filter Yields Preimage under Second Projection

Informal description

For any filter $l$ on a type $\beta$, the coproduct filter of the bottom filter $\bot$ on $\alpha$ with $l$ is equal to the preimage filter of $l$ under the second projection $\text{Prod.snd} : \alpha \times \beta \to \beta$.

Filter.coprod_bot theorem

(l : Filter α) : l.coprod (⊥ : Filter β) = comap Prod.fst l

Full source

@[simp]
theorem coprod_bot (l : Filter α) : l.coprod (⊥ : Filter β) = comap Prod.fst l := by
  simp [Filter.coprod]

Coproduct with Bottom Filter Yields Preimage under First Projection

Informal description

For any filter $l$ on a type $\alpha$, the coproduct filter of $l$ with the bottom filter $\bot$ on $\beta$ is equal to the preimage filter of $l$ under the first projection $\text{pr}_1 : \alpha \times \beta \to \alpha$.

Filter.bot_coprod_bot theorem

: (⊥ : Filter α).coprod (⊥ : Filter β) = ⊥

Full source

theorem bot_coprod_bot : (⊥ : Filter α).coprod (⊥ : Filter β) = ⊥ := by simp

Coproduct of Bottom Filters is Bottom Filter

Informal description

The coproduct filter of the bottom filter on $\alpha$ with the bottom filter on $\beta$ is equal to the bottom filter on $\alpha \times \beta$.

Filter.compl_mem_coprod theorem

 {s : Set (α × β)} {la : Filter α} {lb : Filter β} : sᶜ ∈ la.coprod lb ↔ (Prod.fst '' s)ᶜ ∈ la ∧ (Prod.snd '' s)ᶜ ∈ lb

Full source

theorem compl_mem_coprod {s : Set (α × β)} {la : Filter α} {lb : Filter β} :
    sᶜsᶜ ∈ la.coprod lbsᶜ ∈ la.coprod lb ↔ (Prod.fst '' s)ᶜ ∈ la ∧ (Prod.snd '' s)ᶜ ∈ lb := by
  simp only [Filter.coprod, mem_sup, compl_mem_comap]

Complement Membership in Coproduct Filter via Projections

Informal description

For any set $s \subseteq \alpha \times \beta$ and filters $l_a$ on $\alpha$ and $l_b$ on $\beta$, the complement $s^c$ belongs to the coproduct filter $l_a \times^s l_b$ if and only if the complement of the image of $s$ under the first projection is in $l_a$ and the complement of the image of $s$ under the second projection is in $l_b$. In other words, $s^c \in l_a \times^s l_b \leftrightarrow (\text{fst}(s))^c \in l_a \land (\text{snd}(s))^c \in l_b$.

Filter.coprod_mono theorem

 {f₁ f₂ : Filter α} {g₁ g₂ : Filter β} (hf : f₁ ≤ f₂) (hg : g₁ ≤ g₂) : f₁.coprod g₁ ≤ f₂.coprod g₂

Full source

@[mono]
theorem coprod_mono {f₁ f₂ : Filter α} {g₁ g₂ : Filter β} (hf : f₁ ≤ f₂) (hg : g₁ ≤ g₂) :
    f₁.coprod g₁ ≤ f₂.coprod g₂ :=
  sup_le_sup (comap_mono hf) (comap_mono hg)

Monotonicity of Coproduct Filter: $f_1 \leq f_2 \land g_1 \leq g_2 \Rightarrow f_1 \times^s g_1 \leq f_2 \times^s g_2$

Informal description

For any filters $f_1, f_2$ on type $\alpha$ and $g_1, g_2$ on type $\beta$, if $f_1 \leq f_2$ and $g_1 \leq g_2$, then the coproduct filter $f_1 \times^s g_1$ is less than or equal to $f_2 \times^s g_2$.

Filter.coprod_neBot_iff theorem

: (f.coprod g).NeBot ↔ f.NeBot ∧ Nonempty β ∨ Nonempty α ∧ g.NeBot

Full source

theorem coprod_neBot_iff : (f.coprod g).NeBot ↔ f.NeBot ∧ Nonempty β ∨ Nonempty α ∧ g.NeBot := by
  simp [Filter.coprod]

Characterization of Non-triviality for Coproduct Filter: $(f \times^s g).\text{NeBot} \leftrightarrow (f.\text{NeBot} \land \text{Nonempty } \beta) \lor (\text{Nonempty } \alpha \land g.\text{NeBot})$

Informal description

The coproduct filter $f \times^s g$ on $\alpha \times \beta$ is non-trivial if and only if either: 1. $f$ is non-trivial and $\beta$ is nonempty, or 2. $\alpha$ is nonempty and $g$ is non-trivial.

Filter.coprod_neBot_left theorem

[NeBot f] [Nonempty β] : (f.coprod g).NeBot

Full source

@[instance]
theorem coprod_neBot_left [NeBot f] [Nonempty β] : (f.coprod g).NeBot :=
  coprod_neBot_iff.2 (Or.inl ⟨‹_›, ‹_›⟩)

Non-triviality of Coproduct Filter (Left Case)

Informal description

If $f$ is a non-trivial filter on a type $\alpha$ and $\beta$ is nonempty, then the coproduct filter $f \times^s g$ on $\alpha \times \beta$ is non-trivial.

Filter.coprod_neBot_right theorem

[NeBot g] [Nonempty α] : (f.coprod g).NeBot

Full source

@[instance]
theorem coprod_neBot_right [NeBot g] [Nonempty α] : (f.coprod g).NeBot :=
  coprod_neBot_iff.2 (Or.inr ⟨‹_›, ‹_›⟩)

Non-triviality of Coproduct Filter from Right Factor

Informal description

If the filter $g$ on type $\beta$ is non-trivial and the type $\alpha$ is nonempty, then the coproduct filter $f \coprod g$ on $\alpha \times \beta$ is non-trivial.

Filter.coprod_inf_prod_le theorem

 (f₁ f₂ : Filter α) (g₁ g₂ : Filter β) : f₁.coprod g₁ ⊓ f₂ ×ˢ g₂ ≤ f₁ ×ˢ g₂ ⊔ f₂ ×ˢ g₁

Full source

theorem coprod_inf_prod_le (f₁ f₂ : Filter α) (g₁ g₂ : Filter β) :
    f₁.coprod g₁ ⊓ f₂ ×ˢ g₂ ≤ f₁ ×ˢ g₂ ⊔ f₂ ×ˢ g₁ := calc
  f₁.coprod g₁ ⊓ f₂ ×ˢ g₂
  _ = (f₁ ×ˢ ⊤ ⊔ ⊤ ×ˢ g₁) ⊓ f₂ ×ˢ g₂            := by rw [coprod_eq_prod_top_sup_top_prod]
  _ = f₁ ×ˢ ⊤ ⊓ f₂ ×ˢ g₂f₁ ×ˢ ⊤ ⊓ f₂ ×ˢ g₂ ⊔ ⊤ ×ˢ g₁ ⊓ f₂ ×ˢ g₂   := inf_sup_right _ _ _
  _ = (f₁ ⊓ f₂) ×ˢ g₂ ⊔ f₂ ×ˢ (g₁ ⊓ g₂)         := by simp [prod_inf_prod]
  _ ≤ f₁ ×ˢ g₂ ⊔ f₂ ×ˢ g₁                       :=
    sup_le_sup (prod_mono inf_le_left le_rfl) (prod_mono le_rfl inf_le_left)

Inequality Relating Coproduct and Product Filters: $(f_1 \text{.coprod } g_1) \sqcap (f_2 \timesˢ g_2) \leq (f_1 \timesˢ g_2) \sqcup (f_2 \timesˢ g_1)$

Informal description

For any filters $f_1, f_2$ on a type $\alpha$ and $g_1, g_2$ on a type $\beta$, the infimum of the coproduct filter $f_1 \text{.coprod } g_1$ and the product filter $f_2 \timesˢ g_2$ is less than or equal to the supremum of the product filters $f_1 \timesˢ g_2$ and $f_2 \timesˢ g_1$. In symbols: $$ (f_1 \text{.coprod } g_1) \sqcap (f_2 \timesˢ g_2) \leq (f_1 \timesˢ g_2) \sqcup (f_2 \timesˢ g_1) $$

Filter.principal_coprod_principal theorem

(s : Set α) (t : Set β) : (𝓟 s).coprod (𝓟 t) = 𝓟 (sᶜ ×ˢ tᶜ)ᶜ

Full source

theorem principal_coprod_principal (s : Set α) (t : Set β) :
    (𝓟 s).coprod (𝓟 t) = 𝓟 (sᶜ ×ˢ tᶜ)ᶜ := by
  rw [Filter.coprod, comap_principal, comap_principal, sup_principal, Set.prod_eq, compl_inter,
    preimage_compl, preimage_compl, compl_compl, compl_compl]

Coproduct of Principal Filters as Principal Filter of Complemented Product

Informal description

For any sets $s \subseteq \alpha$ and $t \subseteq \beta$, the coproduct filter of the principal filters generated by $s$ and $t$ is equal to the principal filter generated by the complement of the Cartesian product of the complements of $s$ and $t$. In symbols: $$ \mathcal{P}(s) \coprod \mathcal{P}(t) = \mathcal{P}\big((s^c \times t^c)^c\big) $$

Filter.map_prodMap_coprod_le theorem

 {α₁ : Type u} {α₂ : Type v} {β₁ : Type w} {β₂ : Type x} {f₁ : Filter α₁} {f₂ : Filter α₂} {m₁ : α₁ → β₁}
  {m₂ : α₂ → β₂} : map (Prod.map m₁ m₂) (f₁.coprod f₂) ≤ (map m₁ f₁).coprod (map m₂ f₂)

Full source

theorem map_prodMap_coprod_le.{u, v, w, x} {α₁ : Type u} {α₂ : Type v} {β₁ : Type w} {β₂ : Type x}
    {f₁ : Filter α₁} {f₂ : Filter α₂} {m₁ : α₁ → β₁} {m₂ : α₂ → β₂} :
    map (Prod.map m₁ m₂) (f₁.coprod f₂) ≤ (map m₁ f₁).coprod (map m₂ f₂) := by
  intro s
  simp only [mem_map, mem_coprod_iff]
  rintro ⟨⟨u₁, hu₁, h₁⟩, u₂, hu₂, h₂⟩
  refine ⟨⟨m₁ ⁻¹' u₁, hu₁, fun _ hx => h₁ ?_⟩, ⟨m₂ ⁻¹' u₂, hu₂, fun _ hx => h₂ ?_⟩⟩ <;> convert hx

Image of Coproduct Filter under Product Map is Contained in Coproduct of Image Filters

Informal description

For any types $\alpha_1, \alpha_2, \beta_1, \beta_2$, filters $f_1$ on $\alpha_1$ and $f_2$ on $\alpha_2$, and functions $m_1 : \alpha_1 \to \beta_1$ and $m_2 : \alpha_2 \to \beta_2$, the image filter of the coproduct filter $f_1 \text{.coprod } f_2$ under the product map $\text{Prod.map } m_1 m_2$ is contained in the coproduct of the image filters $\text{map } m_1 f_1$ and $\text{map } m_2 f_2$. In symbols: $$\text{map } (\text{Prod.map } m_1 m_2) (f_1 \text{.coprod } f_2) \leq (\text{map } m_1 f_1) \text{.coprod } (\text{map } m_2 f_2)$$

Filter.map_const_principal_coprod_map_id_principal theorem

 {α β ι : Type*} (a : α) (b : β) (i : ι) :
  (map (fun _ => b) (𝓟 { a })).coprod (map id (𝓟 { i })) = 𝓟 ((({ b } : Set β) ×ˢ univ) ∪ (univ ×ˢ ({ i } : Set ι)))

Full source

/-- Characterization of the coproduct of the `Filter.map`s of two principal filters `𝓟 {a}` and
`𝓟 {i}`, the first under the constant function `fun a => b` and the second under the identity
function. Together with the next lemma, `map_prodMap_const_id_principal_coprod_principal`, this
provides an example showing that the inequality in the lemma `map_prodMap_coprod_le` can be strict.
-/
theorem map_const_principal_coprod_map_id_principal {α β ι : Type*} (a : α) (b : β) (i : ι) :
    (map (fun _ => b) (𝓟 {a})).coprod (map id (𝓟 {i})) =
      𝓟 ((({b} : Set β) ×ˢ univ) ∪ (univ ×ˢ ({i} : Set ι))) := by
  simp only [map_principal, Filter.coprod, comap_principal, sup_principal, image_singleton,
    image_id, prod_univ, univ_prod, id]

Coproduct of Constant and Identity Mapped Principal Filters Equals Principal Filter of Union of Cartesian Products

Informal description

For any types $\alpha$, $\beta$, $\iota$, and elements $a \in \alpha$, $b \in \beta$, $i \in \iota$, the coproduct filter of: 1. The image filter of the principal filter $\{a\}$ under the constant function $\lambda \_, b$, and 2. The image filter of the principal filter $\{i\}$ under the identity function is equal to the principal filter generated by the union of: 1. The Cartesian product $\{b\} \times \iota$, and 2. The Cartesian product $\alpha \times \{i\}$. In symbols: $$\text{coprod}\left(\text{map }(\lambda \_, b) (\mathcal{P}\{a\}), \text{map id }(\mathcal{P}\{i\})\right) = \mathcal{P}\left((\{b\} \times \iota) \cup (\alpha \times \{i\})\right)$$

Filter.map_prodMap_const_id_principal_coprod_principal theorem

 {α β ι : Type*} (a : α) (b : β) (i : ι) :
  map (Prod.map (fun _ : α => b) id) ((𝓟 { a }).coprod (𝓟 { i })) = 𝓟 (({ b } : Set β) ×ˢ (univ : Set ι))

Full source

/-- Characterization of the `Filter.map` of the coproduct of two principal filters `𝓟 {a}` and
`𝓟 {i}`, under the `Prod.map` of two functions, respectively the constant function `fun a => b` and
the identity function.  Together with the previous lemma,
`map_const_principal_coprod_map_id_principal`, this provides an example showing that the inequality
in the lemma `map_prodMap_coprod_le` can be strict. -/
theorem map_prodMap_const_id_principal_coprod_principal {α β ι : Type*} (a : α) (b : β) (i : ι) :
    map (Prod.map (fun _ : α => b) id) ((𝓟 {a}).coprod (𝓟 {i})) =
      𝓟 (({b} : Set β) ×ˢ (univ : Set ι)) := by
  rw [principal_coprod_principal, map_principal]
  congr
  ext ⟨b', i'⟩
  constructor
  · rintro ⟨⟨a'', i''⟩, _, h₂, h₃⟩
    simp
  · rintro ⟨h₁, _⟩
    use (a, i')
    simpa using h₁.symm

Image of Coproduct Principal Filters under Constant-Identity Product Map Equals Principal Filter of $\{b\} \times \iota$

Informal description

For any types $\alpha$, $\beta$, $\iota$, and elements $a \in \alpha$, $b \in \beta$, $i \in \iota$, the image filter of the coproduct filter $\mathcal{P}\{a\} \coprod \mathcal{P}\{i\}$ under the product map $\text{Prod.map } (\lambda \_, b) \text{ id}$ is equal to the principal filter generated by the Cartesian product $\{b\} \times \iota$. In symbols: $$\text{map } (\text{Prod.map } (\lambda \_, b) \text{ id}) (\mathcal{P}\{a\} \coprod \mathcal{P}\{i\}) = \mathcal{P}(\{b\} \times \iota)$$

Filter.Tendsto.prodMap_coprod theorem

 {δ : Type*} {f : α → γ} {g : β → δ} {a : Filter α} {b : Filter β} {c : Filter γ} {d : Filter δ} (hf : Tendsto f a c)
  (hg : Tendsto g b d) : Tendsto (Prod.map f g) (a.coprod b) (c.coprod d)

Full source

theorem Tendsto.prodMap_coprod {δ : Type*} {f : α → γ} {g : β → δ} {a : Filter α} {b : Filter β}
    {c : Filter γ} {d : Filter δ} (hf : Tendsto f a c) (hg : Tendsto g b d) :
    Tendsto (Prod.map f g) (a.coprod b) (c.coprod d) :=
  map_prodMap_coprod_le.trans (coprod_mono hf hg)

Tendsto of Product Map with Respect to Coproduct Filters

Informal description

Let $\alpha, \beta, \gamma, \delta$ be types, and let $f : \alpha \to \gamma$ and $g : \beta \to \delta$ be functions. Given filters $a$ on $\alpha$, $b$ on $\beta$, $c$ on $\gamma$, and $d$ on $\delta$, if $f$ tends to $c$ along $a$ and $g$ tends to $d$ along $b$, then the product map $\text{Prod.map } f g$ tends to the coproduct filter $c \text{.coprod } d$ along the coproduct filter $a \text{.coprod } b$. In symbols: $$\text{Tendsto } f a c \land \text{Tendsto } g b d \implies \text{Tendsto } (\text{Prod.map } f g) (a \text{.coprod } b) (c \text{.coprod } d)$$

Mathlib.Order.Filter.Prod

Implementation details

Notations