# mathlib3documentation

order.filter.prod

# Product and coproduct filters #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.
@[protected]
def filter.prod {α : Type u_1} {β : Type u_2} (f : filter α) (g : filter β) :
filter × β)

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

Equations
Instances for filter.prod
theorem filter.prod_mem_prod {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} {f : filter α} {g : filter β} (hs : s f) (ht : t g) :
s ×ˢ t f.prod g
theorem filter.mem_prod_iff {α : Type u_1} {β : Type u_2} {s : set × β)} {f : filter α} {g : filter β} :
s f.prod g (t₁ : set α) (H : t₁ f) (t₂ : set β) (H : t₂ g), t₁ ×ˢ t₂ s
@[simp]
theorem filter.prod_mem_prod_iff {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} {f : filter α} {g : filter β} [f.ne_bot] [g.ne_bot] :
s ×ˢ t f.prod g s f t g
theorem filter.mem_prod_principal {α : Type u_1} {β : Type u_2} {f : filter α} {s : set × β)} {t : set β} :
s f.prod {a : α | (b : β), b t (a, b) s} f
theorem filter.mem_prod_top {α : Type u_1} {β : Type u_2} {f : filter α} {s : set × β)} :
s f.prod {a : α | (b : β), (a, b) s} f
theorem filter.eventually_prod_principal_iff {α : Type u_1} {β : Type u_2} {f : filter α} {p : α × β Prop} {s : set β} :
(∀ᶠ (x : α × β) in f.prod , p x) ∀ᶠ (x : α) in f, (y : β), y s p (x, y)
theorem filter.comap_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α β × γ) (b : filter β) (c : filter γ) :
(b.prod c) = b c
theorem filter.prod_top {α : Type u_1} {β : Type u_2} {f : filter α} :
theorem filter.sup_prod {α : Type u_1} {β : Type u_2} (f₁ f₂ : filter α) (g : filter β) :
(f₁ f₂).prod g = f₁.prod g f₂.prod g
theorem filter.prod_sup {α : Type u_1} {β : Type u_2} (f : filter α) (g₁ g₂ : filter β) :
f.prod (g₁ g₂) = f.prod g₁ f.prod g₂
theorem filter.eventually_prod_iff {α : Type u_1} {β : Type u_2} {p : α × β Prop} {f : filter α} {g : filter β} :
(∀ᶠ (x : α × β) in f.prod g, p x) (pa : α Prop) (ha : ∀ᶠ (x : α) in f, pa x) (pb : β Prop) (hb : ∀ᶠ (y : β) in g, pb y), {x : α}, pa x {y : β}, pb y p (x, y)
theorem filter.tendsto_fst {α : Type u_1} {β : Type u_2} {f : filter α} {g : filter β} :
(f.prod g) f
theorem filter.tendsto_snd {α : Type u_1} {β : Type u_2} {f : filter α} {g : filter β} :
(f.prod g) g
theorem filter.tendsto.prod_mk {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : filter α} {g : filter β} {h : filter γ} {m₁ : α β} {m₂ : α γ} (h₁ : f g) (h₂ : f h) :
filter.tendsto (λ (x : α), (m₁ x, m₂ x)) f (g.prod h)
theorem filter.tendsto_prod_swap {α1 : Type u_1} {α2 : Type u_2} {a1 : filter α1} {a2 : filter α2} :
(a1.prod a2) (a2.prod a1)
theorem filter.eventually.prod_inl {α : Type u_1} {β : Type u_2} {la : filter α} {p : α Prop} (h : ∀ᶠ (x : α) in la, p x) (lb : filter β) :
∀ᶠ (x : α × β) in la.prod lb, p x.fst
theorem filter.eventually.prod_inr {α : Type u_1} {β : Type u_2} {lb : filter β} {p : β Prop} (h : ∀ᶠ (x : β) in lb, p x) (la : filter α) :
∀ᶠ (x : α × β) in la.prod lb, p x.snd
theorem filter.eventually.prod_mk {α : Type u_1} {β : Type u_2} {la : filter α} {pa : α Prop} (ha : ∀ᶠ (x : α) in la, pa x) {lb : filter β} {pb : β Prop} (hb : ∀ᶠ (y : β) in lb, pb y) :
∀ᶠ (p : α × β) in la.prod lb, pa p.fst pb p.snd
theorem filter.eventually_eq.prod_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {la : filter α} {fa ga : α γ} (ha : fa =ᶠ[la] ga) {lb : filter β} {fb gb : β δ} (hb : fb =ᶠ[lb] gb) :
prod.map fa fb =ᶠ[la.prod lb] prod.map ga gb
theorem filter.eventually_le.prod_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [has_le γ] [has_le δ] {la : filter α} {fa ga : α γ} (ha : fa ≤ᶠ[la] ga) {lb : filter β} {fb gb : β δ} (hb : fb ≤ᶠ[lb] gb) :
prod.map fa fb ≤ᶠ[la.prod lb] prod.map ga gb
theorem filter.eventually.curry {α : Type u_1} {β : Type u_2} {la : filter α} {lb : filter β} {p : α × β Prop} (h : ∀ᶠ (x : α × β) in la.prod lb, p x) :
∀ᶠ (x : α) in la, ∀ᶠ (y : β) in lb, p (x, y)
theorem filter.eventually.diag_of_prod {α : Type u_1} {f : filter α} {p : α × α Prop} (h : ∀ᶠ (i : α × α) in f.prod 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 : filter α} {g : filter γ} {p : × α) × γ Prop} :
(∀ᶠ (x : × α) × γ) in (f.prod f).prod g, p x) (∀ᶠ (x : α × γ) in f.prod g, p ((x.fst, x.fst), x.snd))
theorem filter.eventually.diag_of_prod_right {α : Type u_1} {γ : Type u_3} {f : filter α} {g : filter γ} {p : α × γ × γ Prop} :
(∀ᶠ (x : α × γ × γ) in f.prod (g.prod g), p x) (∀ᶠ (x : α × γ) in f.prod g, p (x.fst, x.snd, x.snd))
theorem filter.tendsto_diag {α : Type u_1} {f : filter α} :
filter.tendsto (λ (i : α), (i, i)) f (f.prod f)
theorem filter.prod_infi_left {α : Type u_1} {β : Type u_2} {ι : Sort u_5} [nonempty ι] {f : ι } {g : filter β} :
( (i : ι), f i).prod g = (i : ι), (f i).prod g
theorem filter.prod_infi_right {α : Type u_1} {β : Type u_2} {ι : Sort u_5} [nonempty ι] {f : filter α} {g : ι } :
f.prod ( (i : ι), g i) = (i : ι), f.prod (g i)
theorem filter.prod_mono {α : Type u_1} {β : Type u_2} {f₁ f₂ : filter α} {g₁ g₂ : filter β} (hf : f₁ f₂) (hg : g₁ g₂) :
f₁.prod g₁ f₂.prod g₂
theorem filter.prod_mono_left {α : Type u_1} {β : Type u_2} (g : filter β) {f₁ f₂ : filter α} (hf : f₁ f₂) :
f₁.prod g f₂.prod g
theorem filter.prod_mono_right {α : Type u_1} {β : Type u_2} (f : filter α) {g₁ g₂ : filter β} (hf : g₁ g₂) :
f.prod g₁ f.prod 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₁).prod (filter.comap m₂ f₂) = filter.comap (λ (p : β₁ × β₂), (m₁ p.fst, m₂ p.snd)) (f₁.prod f₂)
theorem filter.prod_comm' {α : Type u_1} {β : Type u_2} {f : filter α} {g : filter β} :
f.prod g = (g.prod f)
theorem filter.prod_comm {α : Type u_1} {β : Type u_2} {f : filter α} {g : filter β} :
f.prod g = filter.map (λ (p : β × α), (p.snd, p.fst)) (g.prod f)
@[simp]
theorem filter.map_fst_prod {α : Type u_1} {β : Type u_2} (f : filter α) (g : filter β) [g.ne_bot] :
(f.prod g) = f
@[simp]
theorem filter.map_snd_prod {α : Type u_1} {β : Type u_2} (f : filter α) (g : filter β) [f.ne_bot] :
(f.prod g) = g
@[simp]
theorem filter.prod_le_prod {α : Type u_1} {β : Type u_2} {f₁ f₂ : filter α} {g₁ g₂ : filter β} [f₁.ne_bot] [g₁.ne_bot] :
f₁.prod g₁ f₂.prod g₂ f₁ f₂ g₁ g₂
@[simp]
theorem filter.prod_inj {α : Type u_1} {β : Type u_2} {f₁ f₂ : filter α} {g₁ g₂ : filter β} [f₁.ne_bot] [g₁.ne_bot] :
f₁.prod g₁ = f₂.prod g₂ f₁ = f₂ g₁ = g₂
theorem filter.eventually_swap_iff {α : Type u_1} {β : Type u_2} {f : filter α} {g : filter β} {p : α × β Prop} :
(∀ᶠ (x : α × β) in f.prod g, p x) ∀ᶠ (y : β × α) in g.prod f, p y.swap
theorem filter.prod_assoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : filter α) (g : filter β) (h : filter γ) :
filter.map β γ) ((f.prod g).prod h) = f.prod (g.prod h)
theorem filter.prod_assoc_symm {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : filter α) (g : filter β) (h : filter γ) :
filter.map β γ).symm) (f.prod (g.prod h)) = (f.prod g).prod h
theorem filter.tendsto_prod_assoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : filter α} {g : filter β} {h : filter γ} :
filter.tendsto β γ) ((f.prod g).prod h) (f.prod (g.prod h))
theorem filter.tendsto_prod_assoc_symm {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : filter α} {g : filter β} {h : filter γ} :
filter.tendsto β γ).symm) (f.prod (g.prod h)) ((f.prod g).prod h)
theorem filter.map_swap4_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f : filter α} {g : filter β} {h : filter γ} {k : filter δ} :
filter.map (λ (p : × β) × γ × δ), ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) ((f.prod g).prod (h.prod k)) = (f.prod h).prod (g.prod 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 : filter α} {g : filter β} {h : filter γ} {k : filter δ} :
filter.tendsto (λ (p : × β) × γ × δ), ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) ((f.prod g).prod (h.prod k)) ((f.prod h).prod (g.prod 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₁).prod (filter.map m₂ f₂) = filter.map (λ (p : α₁ × α₂), (m₁ p.fst, m₂ p.snd)) (f₁.prod f₂)
theorem filter.prod_map_map_eq' {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} (f : α₁ α₂) (g : β₁ β₂) (F : filter α₁) (G : filter β₁) :
F).prod G) = filter.map (prod.map f g) (F.prod G)
theorem filter.le_prod_map_fst_snd {α : Type u_1} {β : Type u_2} {f : filter × β)} :
f .prod
theorem filter.tendsto.prod_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f : α γ} {g : β δ} {a : filter α} {b : filter β} {c : filter γ} {d : filter δ} (hf : c) (hg : d) :
filter.tendsto (prod.map f g) (a.prod b) (c.prod d)
@[protected]
theorem filter.map_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} (m : α × β γ) (f : filter α) (g : filter β) :
(f.prod g) = (filter.map (λ (a : α) (b : β), m (a, b)) f).seq g
theorem filter.prod_eq {α : Type u_1} {β : Type u_2} {f : filter α} {g : filter β} :
f.prod g = .seq g
theorem filter.prod_inf_prod {α : Type u_1} {β : Type u_2} {f₁ f₂ : filter α} {g₁ g₂ : filter β} :
f₁.prod g₁ f₂.prod g₂ = (f₁ f₂).prod (g₁ g₂)
@[simp]
theorem filter.prod_bot {α : Type u_1} {β : Type u_2} {f : filter α} :
@[simp]
theorem filter.bot_prod {α : Type u_1} {β : Type u_2} {g : filter β} :
@[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 : filter β} :
.prod f = f
theorem filter.map_pure_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α β γ) (a : α) (B : filter β) :
((has_pure.pure a).prod B) = filter.map (f a) B
@[simp]
theorem filter.prod_pure {α : Type u_1} {β : Type u_2} {f : filter α} {b : β} :
f.prod = filter.map (λ (a : α), (a, b)) f
theorem filter.prod_pure_pure {α : Type u_1} {β : Type u_2} {a : α} {b : β} :
theorem filter.prod_eq_bot {α : Type u_1} {β : Type u_2} {f : filter α} {g : filter β} :
f.prod g = f = g =
theorem filter.prod_ne_bot {α : Type u_1} {β : Type u_2} {f : filter α} {g : filter β} :
theorem filter.ne_bot.prod {α : Type u_1} {β : Type u_2} {f : filter α} {g : filter β} (hf : f.ne_bot) (hg : g.ne_bot) :
(f.prod g).ne_bot
@[protected, instance]
def filter.prod_ne_bot' {α : Type u_1} {β : Type u_2} {f : filter α} {g : filter β} [hf : f.ne_bot] [hg : g.ne_bot] :
(f.prod g).ne_bot
theorem filter.tendsto_prod_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α × β γ} {x : filter α} {y : filter β} {z : filter γ} :
(x.prod y) z (W : set γ), W z ( (U : set α) (H : U x) (V : set β) (H : V y), (x : α) (y : β), x U y V f (x, y) W)
theorem filter.tendsto_prod_iff' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : filter α} {g : filter β} {g' : filter γ} {s : α β × γ} :
(g.prod g') filter.tendsto (λ (n : α), (s n).fst) f g filter.tendsto (λ (n : α), (s n).snd) f g'

### Coproducts of filters #

@[protected]
def filter.coprod {α : Type u_1} {β : Type u_2} (f : filter α) (g : filter β) :
filter × β)

Coproduct of filters.

Equations
Instances for filter.coprod
theorem filter.mem_coprod_iff {α : Type u_1} {β : Type u_2} {s : set × β)} {f : filter α} {g : filter β} :
s f.coprod g ( (t₁ : set α) (H : t₁ f), s) (t₂ : set β) (H : t₂ g), s
@[simp]
theorem filter.bot_coprod {α : Type u_1} {β : Type u_2} (l : filter β) :
@[simp]
theorem filter.coprod_bot {α : Type u_1} {β : Type u_2} (l : filter α) :
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 : filter α} {lb : filter β} :
theorem filter.coprod_mono {α : Type u_1} {β : Type u_2} {f₁ f₂ : filter α} {g₁ g₂ : filter β} (hf : f₁ f₂) (hg : g₁ g₂) :
f₁.coprod g₁ f₂.coprod g₂
theorem filter.coprod_ne_bot_iff {α : Type u_1} {β : Type u_2} {f : filter α} {g : filter β} :
@[instance]
theorem filter.coprod_ne_bot_left {α : Type u_1} {β : Type u_2} {f : filter α} {g : filter β} [f.ne_bot] [nonempty β] :
@[instance]
theorem filter.coprod_ne_bot_right {α : Type u_1} {β : Type u_2} {f : filter α} {g : filter β} [g.ne_bot] [nonempty α] :
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₂) (f₁.coprod f₂) (filter.map m₁ f₁).coprod (filter.map m₂ f₂)
theorem filter.map_const_principal_coprod_map_id_principal {α : Type u_1} {β : Type u_2} {ι : Type u_3} (a : α) (b : β) (i : ι) :

Characterization of the coproduct of the filter.maps of two principal filters 𝓟 {a} and 𝓟 {i}, the first under the constant function λ 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_1} {β : Type u_2} {ι : Type u_3} (a : α) (b : β) (i : ι) :

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 λ 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_4} {f : α γ} {g : β δ} {a : filter α} {b : filter β} {c : filter γ} {d : filter δ} (hf : c) (hg : d) :