# Documentation

Mathlib.Order.Filter.Prod

# Product and coproduct filters #

In this file we define Filter.prod f g (notation: f ×ˢ g) and Filter.coprod f g. The product of two filters is the largest filter l such that Filter.Tendsto Prod.fst l f and Filter.Tendsto Prod.snd l g.

## Implementation details #

The product filter cannot be defined using the monad structure on filters. For example:

F := do {x ← seq, y ← top, return (x, y)}
G := do {y ← top, x ← seq, return (x, y)}


hence:

s ∈ F  ↔  ∃ n, [n..∞] × univ ⊆ s
s ∈ G  ↔  ∀ i:ℕ, ∃ n, [n..∞] × {i} ⊆ s


Now ⋃ i, [i..∞] × {i} is in G but not in F. As product filter we want to have F as result.

## Notations #

• f ×ˢ g : Filter.prod f g, localized in Filter.
def Filter.prod {α : Type u_1} {β : Type u_2} (f : ) (g : ) :
Filter (α × β)

Product of filters. This is the filter generated by cartesian products of elements of the component filters.

Instances For
instance Filter.instSProd {α : Type u_1} {β : Type u_2} :
SProd () () (Filter (α × β))
theorem Filter.prod_mem_prod {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : } {g : } (hs : s f) (ht : t g) :
s ×ˢ t f ×ˢ g
theorem Filter.mem_prod_iff {α : Type u_1} {β : Type u_2} {s : Set (α × β)} {f : } {g : } :
s f ×ˢ g t₁, t₁ f t₂, t₂ g t₁ ×ˢ t₂ s
@[simp]
theorem Filter.prod_mem_prod_iff {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : } {g : } [] [] :
s ×ˢ t f ×ˢ g s f t g
theorem Filter.mem_prod_principal {α : Type u_1} {β : Type u_2} {f : } {s : Set (α × β)} {t : Set β} :
s {a | ∀ (b : β), b t(a, b) s} f
theorem Filter.mem_prod_top {α : Type u_1} {β : Type u_2} {f : } {s : Set (α × β)} :
s f ×ˢ {a | ∀ (b : β), (a, b) s} f
theorem Filter.eventually_prod_principal_iff {α : Type u_1} {β : Type u_2} {f : } {p : α × βProp} {s : Set β} :
(∀ᶠ (x : α × β) in , p x) ∀ᶠ (x : α) in f, (y : β) → y sp (x, y)
theorem Filter.comap_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβ × γ) (b : ) (c : ) :
Filter.comap f (b ×ˢ c) = Filter.comap (Prod.fst f) b Filter.comap (Prod.snd f) c
theorem Filter.prod_top {α : Type u_1} {β : Type u_2} {f : } :
f ×ˢ = Filter.comap Prod.fst f
theorem Filter.sup_prod {α : Type u_1} {β : Type u_2} (f₁ : ) (f₂ : ) (g : ) :
(f₁ f₂) ×ˢ g = f₁ ×ˢ g f₂ ×ˢ g
theorem Filter.prod_sup {α : Type u_1} {β : Type u_2} (f : ) (g₁ : ) (g₂ : ) :
f ×ˢ (g₁ g₂) = f ×ˢ g₁ f ×ˢ g₂
theorem Filter.eventually_prod_iff {α : Type u_1} {β : Type u_2} {p : α × βProp} {f : } {g : } :
(∀ᶠ (x : α × β) in f ×ˢ g, p x) pa, (∀ᶠ (x : α) in f, pa x) pb, (∀ᶠ (y : β) in g, pb y) ({x : α} → pa x{y : β} → pb yp (x, y))
theorem Filter.tendsto_fst {α : Type u_1} {β : Type u_2} {f : } {g : } :
Filter.Tendsto Prod.fst (f ×ˢ g) f
theorem Filter.tendsto_snd {α : Type u_1} {β : Type u_2} {f : } {g : } :
Filter.Tendsto Prod.snd (f ×ˢ g) g
theorem Filter.Tendsto.prod_mk {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : } {g : } {h : } {m₁ : αβ} {m₂ : αγ} (h₁ : Filter.Tendsto m₁ f g) (h₂ : Filter.Tendsto m₂ f h) :
Filter.Tendsto (fun x => (m₁ x, m₂ x)) f (g ×ˢ h)
theorem Filter.tendsto_prod_swap {α1 : Type u_6} {α2 : Type u_7} {a1 : Filter α1} {a2 : Filter α2} :
Filter.Tendsto Prod.swap (a1 ×ˢ a2) (a2 ×ˢ a1)
theorem Filter.Eventually.prod_inl {α : Type u_1} {β : Type u_2} {la : } {p : αProp} (h : ∀ᶠ (x : α) in la, p x) (lb : ) :
∀ᶠ (x : α × β) in la ×ˢ lb, p x.fst
theorem Filter.Eventually.prod_inr {α : Type u_1} {β : Type u_2} {lb : } {p : βProp} (h : ∀ᶠ (x : β) in lb, p x) (la : ) :
∀ᶠ (x : α × β) in la ×ˢ lb, p x.snd
theorem Filter.Eventually.prod_mk {α : Type u_1} {β : Type u_2} {la : } {pa : αProp} (ha : ∀ᶠ (x : α) in la, pa x) {lb : } {pb : βProp} (hb : ∀ᶠ (y : β) in lb, pb y) :
∀ᶠ (p : α × β) in la ×ˢ lb, pa p.fst pb p.snd
theorem Filter.EventuallyEq.prod_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_6} {la : } {fa : αγ} {ga : αγ} (ha : fa =ᶠ[la] ga) {lb : } {fb : βδ} {gb : βδ} (hb : fb =ᶠ[lb] gb) :
Prod.map fa fb =ᶠ[la ×ˢ lb] Prod.map ga gb
theorem Filter.EventuallyLE.prod_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_6} [LE γ] [LE δ] {la : } {fa : αγ} {ga : αγ} (ha : fa ≤ᶠ[la] ga) {lb : } {fb : βδ} {gb : βδ} (hb : fb ≤ᶠ[lb] gb) :
Prod.map fa fb ≤ᶠ[la ×ˢ lb] Prod.map ga gb
theorem Filter.Eventually.curry {α : Type u_1} {β : Type u_2} {la : } {lb : } {p : α × βProp} (h : ∀ᶠ (x : α × β) in la ×ˢ lb, p x) :
∀ᶠ (x : α) in la, ∀ᶠ (y : β) in lb, p (x, y)
theorem Filter.Eventually.diag_of_prod {α : Type u_1} {f : } {p : α × αProp} (h : ∀ᶠ (i : α × α) in f ×ˢ f, p i) :
∀ᶠ (i : α) in f, p (i, i)

A fact that is eventually true about all pairs l ×ˢ l is eventually true about all diagonal pairs (i, i)

theorem Filter.Eventually.diag_of_prod_left {α : Type u_1} {γ : Type u_3} {f : } {g : } {p : (α × α) × γProp} :
(∀ᶠ (x : (α × α) × γ) in (f ×ˢ f) ×ˢ g, p x) → ∀ᶠ (x : α × γ) in f ×ˢ g, p ((x.fst, x.fst), x.snd)
theorem Filter.Eventually.diag_of_prod_right {α : Type u_1} {γ : Type u_3} {f : } {g : } {p : α × γ × γProp} :
(∀ᶠ (x : α × γ × γ) in f ×ˢ g ×ˢ g, p x) → ∀ᶠ (x : α × γ) in f ×ˢ g, p (x.fst, x.snd, x.snd)
theorem Filter.tendsto_diag {α : Type u_1} {f : } :
Filter.Tendsto (fun i => (i, i)) f (f ×ˢ f)
theorem Filter.prod_iInf_left {α : Type u_1} {β : Type u_2} {ι : Sort u_5} [] {f : ι} {g : } :
(⨅ (i : ι), f i) ×ˢ g = ⨅ (i : ι), f i ×ˢ g
theorem Filter.prod_iInf_right {α : Type u_1} {β : Type u_2} {ι : Sort u_5} [] {f : } {g : ι} :
f ×ˢ ⨅ (i : ι), g i = ⨅ (i : ι), f ×ˢ g i
theorem Filter.prod_mono {α : Type u_1} {β : Type u_2} {f₁ : } {f₂ : } {g₁ : } {g₂ : } (hf : f₁ f₂) (hg : g₁ g₂) :
f₁ ×ˢ g₁ f₂ ×ˢ g₂
theorem Filter.prod_mono_left {α : Type u_1} {β : Type u_2} (g : ) {f₁ : } {f₂ : } (hf : f₁ f₂) :
f₁ ×ˢ g f₂ ×ˢ g
theorem Filter.prod_mono_right {α : Type u_1} {β : Type u_2} (f : ) {g₁ : } {g₂ : } (hf : g₁ g₂) :
f ×ˢ g₁ f ×ˢ g₂
theorem Filter.prod_comap_comap_eq {α₁ : Type u} {α₂ : Type v} {β₁ : Type w} {β₂ : Type x} {f₁ : Filter α₁} {f₂ : Filter α₂} {m₁ : β₁α₁} {m₂ : β₂α₂} :
Filter.comap m₁ f₁ ×ˢ Filter.comap m₂ f₂ = Filter.comap (fun p => (m₁ p.fst, m₂ p.snd)) (f₁ ×ˢ f₂)
theorem Filter.prod_comm' {α : Type u_1} {β : Type u_2} {f : } {g : } :
f ×ˢ g = Filter.comap Prod.swap (g ×ˢ f)
theorem Filter.prod_comm {α : Type u_1} {β : Type u_2} {f : } {g : } :
f ×ˢ g = Filter.map (fun p => (p.snd, p.fst)) (g ×ˢ f)
theorem Filter.mem_prod_iff_left {α : Type u_1} {β : Type u_2} {s : Set (α × β)} {f : } {g : } :
s f ×ˢ g t, t f ∀ᶠ (y : β) in g, ∀ (x : α), x t(x, y) s
theorem Filter.mem_prod_iff_right {α : Type u_1} {β : Type u_2} {s : Set (α × β)} {f : } {g : } :
s f ×ˢ g t, t g ∀ᶠ (x : α) in f, ∀ (y : β), y t(x, y) s
@[simp]
theorem Filter.map_fst_prod {α : Type u_1} {β : Type u_2} (f : ) (g : ) [] :
Filter.map Prod.fst (f ×ˢ g) = f
@[simp]
theorem Filter.map_snd_prod {α : Type u_1} {β : Type u_2} (f : ) (g : ) [] :
Filter.map Prod.snd (f ×ˢ g) = g
@[simp]
theorem Filter.prod_le_prod {α : Type u_1} {β : Type u_2} {f₁ : } {f₂ : } {g₁ : } {g₂ : } [] [] :
f₁ ×ˢ g₁ f₂ ×ˢ g₂ f₁ f₂ g₁ g₂
@[simp]
theorem Filter.prod_inj {α : Type u_1} {β : Type u_2} {f₁ : } {f₂ : } {g₁ : } {g₂ : } [] [] :
f₁ ×ˢ g₁ = f₂ ×ˢ g₂ f₁ = f₂ g₁ = g₂
theorem Filter.eventually_swap_iff {α : Type u_1} {β : Type u_2} {f : } {g : } {p : α × βProp} :
(∀ᶠ (x : α × β) in f ×ˢ g, p x) ∀ᶠ (y : β × α) in g ×ˢ f, p ()
theorem Filter.prod_assoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : ) (g : ) (h : ) :
Filter.map (↑()) ((f ×ˢ g) ×ˢ h) = f ×ˢ g ×ˢ h
theorem Filter.prod_assoc_symm {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : ) (g : ) (h : ) :
Filter.map (().symm) (f ×ˢ g ×ˢ h) = (f ×ˢ g) ×ˢ h
theorem Filter.tendsto_prodAssoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : } {g : } {h : } :
Filter.Tendsto (↑()) ((f ×ˢ g) ×ˢ h) (f ×ˢ g ×ˢ h)
theorem Filter.tendsto_prodAssoc_symm {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : } {g : } {h : } :
Filter.Tendsto (().symm) (f ×ˢ g ×ˢ h) ((f ×ˢ g) ×ˢ h)
theorem Filter.map_swap4_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f : } {g : } {h : } {k : } :
Filter.map (fun p => ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) ((f ×ˢ g) ×ˢ h ×ˢ k) = (f ×ˢ h) ×ˢ g ×ˢ k

A useful lemma when dealing with uniformities.

theorem Filter.tendsto_swap4_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f : } {g : } {h : } {k : } :
Filter.Tendsto (fun p => ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) ((f ×ˢ g) ×ˢ h ×ˢ k) ((f ×ˢ h) ×ˢ g ×ˢ k)
theorem Filter.prod_map_map_eq {α₁ : Type u} {α₂ : Type v} {β₁ : Type w} {β₂ : Type x} {f₁ : Filter α₁} {f₂ : Filter α₂} {m₁ : α₁β₁} {m₂ : α₂β₂} :
Filter.map m₁ f₁ ×ˢ Filter.map m₂ f₂ = Filter.map (fun p => (m₁ p.fst, m₂ p.snd)) (f₁ ×ˢ f₂)
theorem Filter.prod_map_map_eq' {α₁ : Type u_6} {α₂ : Type u_7} {β₁ : Type u_8} {β₂ : Type u_9} (f : α₁α₂) (g : β₁β₂) (F : Filter α₁) (G : Filter β₁) :
theorem Filter.prod_map_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβ) (F : ) (G : ) :
×ˢ G = Filter.map (Prod.map f id) (F ×ˢ G)
theorem Filter.prod_map_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : βγ) (F : ) (G : ) :
F ×ˢ = Filter.map (Prod.map id f) (F ×ˢ G)
theorem Filter.le_prod_map_fst_snd {α : Type u_1} {β : Type u_2} {f : Filter (α × β)} :
f Filter.map Prod.fst f ×ˢ Filter.map Prod.snd f
theorem Filter.Tendsto.prod_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_6} {f : αγ} {g : βδ} {a : } {b : } {c : } {d : } (hf : ) (hg : ) :
Filter.Tendsto (Prod.map f g) (a ×ˢ b) (c ×ˢ d)
theorem Filter.map_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} (m : α × βγ) (f : ) (g : ) :
Filter.map m (f ×ˢ g) = Filter.seq (Filter.map (fun a b => m (a, b)) f) g
theorem Filter.prod_eq {α : Type u_1} {β : Type u_2} {f : } {g : } :
f ×ˢ g = Filter.seq (Filter.map Prod.mk f) g
theorem Filter.prod_inf_prod {α : Type u_1} {β : Type u_2} {f₁ : } {f₂ : } {g₁ : } {g₂ : } :
f₁ ×ˢ g₁ f₂ ×ˢ g₂ = (f₁ f₂) ×ˢ (g₁ g₂)
theorem Filter.inf_prod {α : Type u_1} {β : Type u_2} {f₁ : } {f₂ : } {g : } :
(f₁ f₂) ×ˢ g = f₁ ×ˢ g f₂ ×ˢ g
theorem Filter.prod_inf {α : Type u_1} {β : Type u_2} {f : } {g₁ : } {g₂ : } :
f ×ˢ (g₁ g₂) = f ×ˢ g₁ f ×ˢ g₂
@[simp]
theorem Filter.prod_principal_principal {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} :
@[simp]
theorem Filter.pure_prod {α : Type u_1} {β : Type u_2} {a : α} {f : } :
theorem Filter.map_pure_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβγ) (a : α) (B : ) :
Filter.map () (pure a ×ˢ B) = Filter.map (f a) B
@[simp]
theorem Filter.prod_pure {α : Type u_1} {β : Type u_2} {f : } {b : β} :
f ×ˢ pure b = Filter.map (fun a => (a, b)) f
theorem Filter.prod_pure_pure {α : Type u_1} {β : Type u_2} {a : α} {b : β} :
pure a ×ˢ pure b = pure (a, b)
theorem Filter.prod_eq_bot {α : Type u_1} {β : Type u_2} {f : } {g : } :
f ×ˢ g = f = g =
@[simp]
theorem Filter.prod_bot {α : Type u_1} {β : Type u_2} {f : } :
@[simp]
theorem Filter.bot_prod {α : Type u_1} {β : Type u_2} {g : } :
theorem Filter.prod_neBot {α : Type u_1} {β : Type u_2} {f : } {g : } :
theorem Filter.NeBot.prod {α : Type u_1} {β : Type u_2} {f : } {g : } (hf : ) (hg : ) :
instance Filter.prod_neBot' {α : Type u_1} {β : Type u_2} {f : } {g : } [hf : ] [hg : ] :
theorem Filter.tendsto_prod_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α × βγ} {x : } {y : } {z : } :
Filter.Tendsto f (x ×ˢ y) z ∀ (W : Set γ), W zU, U x V, V y ∀ (x : α) (y : β), x Uy Vf (x, y) W
theorem Filter.le_prod {α : Type u_1} {β : Type u_2} {f : Filter (α × β)} {g : } {g' : } :
f g ×ˢ g' Filter.Tendsto Prod.fst f g Filter.Tendsto Prod.snd f g'
theorem Filter.tendsto_prod_iff' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : } {g : } {g' : } {s : αβ × γ} :
Filter.Tendsto s f (g ×ˢ g') Filter.Tendsto (fun n => (s n).fst) f g Filter.Tendsto (fun n => (s n).snd) f g'

### Coproducts of filters #

def Filter.coprod {α : Type u_1} {β : Type u_2} (f : ) (g : ) :
Filter (α × β)

Coproduct of filters.

Instances For
theorem Filter.mem_coprod_iff {α : Type u_1} {β : Type u_2} {s : Set (α × β)} {f : } {g : } :
s (t₁, t₁ f Prod.fst ⁻¹' t₁ s) t₂, t₂ g Prod.snd ⁻¹' t₂ s
@[simp]
theorem Filter.bot_coprod {α : Type u_1} {β : Type u_2} (l : ) :
= Filter.comap Prod.snd l
@[simp]
theorem Filter.coprod_bot {α : Type u_1} {β : Type u_2} (l : ) :
= Filter.comap Prod.fst l
theorem Filter.bot_coprod_bot {α : Type u_1} {β : Type u_2} :
theorem Filter.compl_mem_coprod {α : Type u_1} {β : Type u_2} {s : Set (α × β)} {la : } {lb : } :
s Filter.coprod la lb (Prod.fst '' s) la (Prod.snd '' s) lb
theorem Filter.coprod_mono {α : Type u_1} {β : Type u_2} {f₁ : } {f₂ : } {g₁ : } {g₂ : } (hf : f₁ f₂) (hg : g₁ g₂) :
Filter.coprod f₁ g₁ Filter.coprod f₂ g₂
theorem Filter.coprod_neBot_iff {α : Type u_1} {β : Type u_2} {f : } {g : } :
theorem Filter.coprod_neBot_left {α : Type u_1} {β : Type u_2} {f : } {g : } [] [] :
theorem Filter.coprod_neBot_right {α : Type u_1} {β : Type u_2} {f : } {g : } [] [] :
theorem Filter.principal_coprod_principal {α : Type u_1} {β : Type u_2} (s : Set α) (t : Set β) :
theorem Filter.map_prod_map_coprod_le {α₁ : Type u} {α₂ : Type v} {β₁ : Type w} {β₂ : Type x} {f₁ : Filter α₁} {f₂ : Filter α₂} {m₁ : α₁β₁} {m₂ : α₂β₂} :
Filter.map (Prod.map m₁ m₂) (Filter.coprod f₁ f₂) Filter.coprod (Filter.map m₁ f₁) (Filter.map m₂ f₂)
theorem Filter.map_const_principal_coprod_map_id_principal {α : Type u_6} {β : Type u_7} {ι : Type u_8} (a : α) (b : β) (i : ι) :
Filter.coprod (Filter.map (fun x => b) ()) (Filter.map id ()) = Filter.principal ({b} ×ˢ Set.univ Set.univ ×ˢ {i})

Characterization of the coproduct of the Filter.maps 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_prod_map_const_id_principal_coprod_principal, this provides an example showing that the inequality in the lemma map_prod_map_coprod_le can be strict.

theorem Filter.map_prod_map_const_id_principal_coprod_principal {α : Type u_6} {β : Type u_7} {ι : Type u_8} (a : α) (b : β) (i : ι) :
Filter.map (Prod.map (fun x => b) id) (Filter.coprod () ()) = Filter.principal ({b} ×ˢ Set.univ)

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_prod_map_coprod_le can be strict.

theorem Filter.Tendsto.prod_map_coprod {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_6} {f : αγ} {g : βδ} {a : } {b : } {c : } {d : } (hf : ) (hg : ) :