mathlib3 documentation

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 #

source
@[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
source
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
source
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
source
@[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
source
theorem filter.mem_prod_principal {α : Type u_1} {β : Type u_2} {f : filter α} {s : set (α × β)} {t : set β} :
s ∈ f.prod (filter.principal t) ↔ {a : α | ∀ (b : β), b ∈ t → (a, b) ∈ s} ∈ f
source
theorem filter.mem_prod_top {α : Type u_1} {β : Type u_2} {f : filter α} {s : set (α × β)} :
s ∈ f.prod ⊤ ↔ {a : α | ∀ (b : β), (a, b) ∈ s} ∈ f
source
theorem filter.eventually_prod_principal_iff {α : Type u_1} {β : Type u_2} {f : filter α} {p : α × β → Prop} {s : set β} :
(∀ᶠ (x : α × β) in f.prod (filter.principal s), p x) ↔ ∀ᶠ (x : α) in f, ∀ (y : β), y ∈ s → p (x, y)
source
theorem filter.comap_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β × γ) (b : filter β) (c : filter γ) :
filter.comap f (b.prod c) = filter.comap (prod.fst ∘ f) b ⊓ filter.comap (prod.snd ∘ f) c
source
theorem filter.prod_top {α : Type u_1} {β : Type u_2} {f : filter α} :
f.prod ⊤ = filter.comap prod.fst f
source
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
source
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₂
source
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)
source
theorem filter.tendsto_fst {α : Type u_1} {β : Type u_2} {f : filter α} {g : filter β} :
filter.tendsto prod.fst (f.prod g) f
source
theorem filter.tendsto_snd {α : Type u_1} {β : Type u_2} {f : filter α} {g : filter β} :
filter.tendsto prod.snd (f.prod g) g
source
theorem filter.tendsto.prod_mk {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : filter α} {g : filter β} {h : filter γ} {m₁ : α → β} {m₂ : α → γ} (h₁ : filter.tendsto m₁ f g) (h₂ : filter.tendsto m₂ f h) :
filter.tendsto (λ (x : α), (m₁ x, m₂ x)) f (g.prod h)
source
theorem filter.tendsto_prod_swap {α1 : Type u_1} {α2 : Type u_2} {a1 : filter α1} {a2 : filter α2} :
filter.tendsto prod.swap (a1.prod a2) (a2.prod a1)
source
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
source
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
source
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
source
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
source
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
source
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)
source
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)

source
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))
source
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))
source
theorem filter.tendsto_diag {α : Type u_1} {f : filter α} :
filter.tendsto (λ (i : α), (i, i)) f (f.prod f)
source
theorem filter.prod_infi_left {α : Type u_1} {β : Type u_2} {ι : Sort u_5} [nonempty ι] {f : ι → filter α} {g : filter β} :
(⨅ (i : ι), f i).prod g = ⨅ (i : ι), (f i).prod g
source
theorem filter.prod_infi_right {α : Type u_1} {β : Type u_2} {ι : Sort u_5} [nonempty ι] {f : filter α} {g : ι → filter β} :
f.prod (⨅ (i : ι), g i) = ⨅ (i : ι), f.prod (g i)
source
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₂
source
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
source
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₂
source
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₂)
source
theorem filter.prod_comm' {α : Type u_1} {β : Type u_2} {f : filter α} {g : filter β} :
f.prod g = filter.comap prod.swap (g.prod f)
source
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)
source
@[simp]
theorem filter.map_fst_prod {α : Type u_1} {β : Type u_2} (f : filter α) (g : filter β) [g.ne_bot] :
filter.map prod.fst (f.prod g) = f
source
@[simp]
theorem filter.map_snd_prod {α : Type u_1} {β : Type u_2} (f : filter α) (g : filter β) [f.ne_bot] :
filter.map prod.snd (f.prod g) = g
source
@[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₂
source
@[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₂
source
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
source
theorem filter.prod_assoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : filter α) (g : filter β) (h : filter γ) :
filter.map ⇑(equiv.prod_assoc α β γ) ((f.prod g).prod h) = f.prod (g.prod h)
source
theorem filter.prod_assoc_symm {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : filter α) (g : filter β) (h : filter γ) :
filter.map ⇑((equiv.prod_assoc α β γ).symm) (f.prod (g.prod h)) = (f.prod g).prod h
source
theorem filter.tendsto_prod_assoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : filter α} {g : filter β} {h : filter γ} :
filter.tendsto ⇑(equiv.prod_assoc α β γ) ((f.prod g).prod h) (f.prod (g.prod h))
source
theorem filter.tendsto_prod_assoc_symm {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : filter α} {g : filter β} {h : filter γ} :
filter.tendsto ⇑((equiv.prod_assoc α β γ).symm) (f.prod (g.prod h)) ((f.prod g).prod h)
source
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.

source
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))
source
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₂)
source
theorem filter.prod_map_map_eq' {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} (f : α₁ → α₂) (g : β₁ → β₂) (F : filter α₁) (G : filter β₁) :
(filter.map f F).prod (filter.map g G) = filter.map (prod.map f g) (F.prod G)
source
theorem filter.le_prod_map_fst_snd {α : Type u_1} {β : Type u_2} {f : filter (α × β)} :
f ≤ (filter.map prod.fst f).prod (filter.map prod.snd f)
source
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 : filter.tendsto f a c) (hg : filter.tendsto g b d) :
filter.tendsto (prod.map f g) (a.prod b) (c.prod d)
source
@[protected]
theorem filter.map_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} (m : α × β → γ) (f : filter α) (g : filter β) :
filter.map m (f.prod g) = (filter.map (λ (a : α) (b : β), m (a, b)) f).seq g
source
theorem filter.prod_eq {α : Type u_1} {β : Type u_2} {f : filter α} {g : filter β} :
f.prod g = (filter.map prod.mk f).seq g
source
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₂)
source
@[simp]
theorem filter.prod_bot {α : Type u_1} {β : Type u_2} {f : filter α} :
f.prod ⊥ = ⊥
source
@[simp]
theorem filter.bot_prod {α : Type u_1} {β : Type u_2} {g : filter β} :
⊥.prod g = ⊥
source
@[simp]
theorem filter.prod_principal_principal {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} :
(filter.principal s).prod (filter.principal t) = filter.principal (s ×ˢ t)
source
@[simp]
theorem filter.pure_prod {α : Type u_1} {β : Type u_2} {a : α} {f : filter β} :
(has_pure.pure a).prod f = filter.map (prod.mk a) f
source
theorem filter.map_pure_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (a : α) (B : filter β) :
filter.map (function.uncurry f) ((has_pure.pure a).prod B) = filter.map (f a) B
source
@[simp]
theorem filter.prod_pure {α : Type u_1} {β : Type u_2} {f : filter α} {b : β} :
f.prod (has_pure.pure b) = filter.map (λ (a : α), (a, b)) f
source
theorem filter.prod_pure_pure {α : Type u_1} {β : Type u_2} {a : α} {b : β} :
(has_pure.pure a).prod (has_pure.pure b) = has_pure.pure (a, b)
source
theorem filter.prod_eq_bot {α : Type u_1} {β : Type u_2} {f : filter α} {g : filter β} :
f.prod g = ⊥ ↔ f = ⊥ ∨ g = ⊥
source
theorem filter.prod_ne_bot {α : Type u_1} {β : Type u_2} {f : filter α} {g : filter β} :
(f.prod g).ne_bot ↔ f.ne_bot ∧ g.ne_bot
source
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
source
@[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
source
theorem filter.tendsto_prod_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α × β → γ} {x : filter α} {y : filter β} {z : filter γ} :
filter.tendsto f (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)
source
theorem filter.tendsto_prod_iff' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : filter α} {g : filter β} {g' : filter γ} {s : α → β × γ} :
filter.tendsto s f (g.prod g') ↔ filter.tendsto (λ (n : α), (s n).fst) f g ∧ filter.tendsto (λ (n : α), (s n).snd) f g'

Coproducts of filters #

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

Coproduct of filters.

Equations
Instances for filter.coprod
source
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), prod.fst ⁻¹' t₁ ⊆ s) ∧ ∃ (t₂ : set β) (H : t₂ ∈ g), prod.snd ⁻¹' t₂ ⊆ s
source
@[simp]
theorem filter.bot_coprod {α : Type u_1} {β : Type u_2} (l : filter β) :
⊥.coprod l = filter.comap prod.snd l
source
@[simp]
theorem filter.coprod_bot {α : Type u_1} {β : Type u_2} (l : filter α) :
l.coprod ⊥ = filter.comap prod.fst l
source
theorem filter.bot_coprod_bot {α : Type u_1} {β : Type u_2} :
⊥.coprod ⊥ = ⊥
source
theorem filter.compl_mem_coprod {α : Type u_1} {β : Type u_2} {s : set (α × β)} {la : filter α} {lb : filter β} :
sᶜ ∈ la.coprod lb ↔ (prod.fst '' s)ᶜ ∈ la ∧ (prod.snd '' s)ᶜ ∈ lb
source
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₂
source
theorem filter.coprod_ne_bot_iff {α : Type u_1} {β : Type u_2} {f : filter α} {g : filter β} :
(f.coprod g).ne_bot ↔ f.ne_bot ∧ nonempty β ∨ nonempty α ∧ g.ne_bot
source
@[instance]
theorem filter.coprod_ne_bot_left {α : Type u_1} {β : Type u_2} {f : filter α} {g : filter β} [f.ne_bot] [nonempty β] :
(f.coprod g).ne_bot
source
@[instance]
theorem filter.coprod_ne_bot_right {α : Type u_1} {β : Type u_2} {f : filter α} {g : filter β} [g.ne_bot] [nonempty α] :
(f.coprod g).ne_bot
source
theorem filter.principal_coprod_principal {α : Type u_1} {β : Type u_2} (s : set α) (t : set β) :
(filter.principal s).coprod (filter.principal t) = filter.principal (sᶜ ×ˢ tᶜ)ᶜ
source
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₂)
source
theorem filter.map_const_principal_coprod_map_id_principal {α : Type u_1} {β : Type u_2} {ι : Type u_3} (a : α) (b : β) (i : ι) :
(filter.map (λ (_x : α), b) (filter.principal {a})).coprod (filter.map id (filter.principal {i})) = 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 λ 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.

source
theorem filter.map_prod_map_const_id_principal_coprod_principal {α : Type u_1} {β : Type u_2} {ι : Type u_3} (a : α) (b : β) (i : ι) :
filter.map (prod.map (λ (_x : α), b) id) ((filter.principal {a}).coprod (filter.principal {i})) = 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 λ 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.

source
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 : filter.tendsto f a c) (hg : filter.tendsto g b d) :
filter.tendsto (prod.map f g) (a.coprod b) (c.coprod d)