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 #

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

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

Equations
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) :
theorem Filter.mem_prod_iff {α : Type u_2} {β : Type u_1} {s : Set (α × β)} {f : Filter α} {g : Filter β} :
s Filter.prod 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 : Filter α} {g : Filter β} [inst : Filter.NeBot f] [inst : Filter.NeBot g] :
s ×ˢ t Filter.prod f g s f t g
theorem Filter.mem_prod_principal {α : Type u_1} {β : Type u_2} {f : Filter α} {s : Set (α × β)} {t : Set β} :
s Filter.prod f (Filter.principal t) { a | ∀ (b : β), b t(a, b) s } f
theorem Filter.mem_prod_top {α : Type u_1} {β : Type u_2} {f : Filter α} {s : Set (α × β)} :
s Filter.prod f { a | ∀ (b : β), (a, b) s } f
theorem Filter.eventually_prod_principal_iff {α : Type u_1} {β : Type u_2} {f : Filter α} {p : α × βProp} {s : Set β} :
Filter.Eventually (fun x => p x) (Filter.prod f (Filter.principal s)) Filter.Eventually (fun x => (y : β) → y sp (x, y)) f
theorem Filter.comap_prod {α : Type u_3} {β : Type u_1} {γ : Type u_2} (f : αβ × γ) (b : Filter β) (c : Filter γ) :
Filter.comap f (Filter.prod 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 : Filter α} :
theorem Filter.sup_prod {α : Type u_1} {β : Type u_2} (f₁ : Filter α) (f₂ : Filter α) (g : Filter β) :
Filter.prod (f₁ f₂) g = Filter.prod f₁ g Filter.prod f₂ g
theorem Filter.prod_sup {α : Type u_1} {β : Type u_2} (f : Filter α) (g₁ : Filter β) (g₂ : Filter β) :
Filter.prod f (g₁ g₂) = Filter.prod f g₁ Filter.prod f g₂
theorem Filter.eventually_prod_iff {α : Type u_1} {β : Type u_2} {p : α × βProp} {f : Filter α} {g : Filter β} :
Filter.Eventually (fun x => p x) (Filter.prod f g) pa, Filter.Eventually (fun x => pa x) f pb, Filter.Eventually (fun y => pb y) g ({x : α} → pa x{y : β} → pb yp (x, y))
theorem Filter.tendsto_fst {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β} :
Filter.Tendsto Prod.fst (Filter.prod f g) f
theorem Filter.tendsto_snd {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β} :
Filter.Tendsto Prod.snd (Filter.prod f 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₁ : Filter.Tendsto m₁ f g) (h₂ : Filter.Tendsto m₂ f h) :
Filter.Tendsto (fun x => (m₁ x, m₂ x)) f (Filter.prod g h)
theorem Filter.tendsto_prod_swap {α1 : Type u_1} {α2 : Type u_2} {a1 : Filter α1} {a2 : Filter α2} :
Filter.Tendsto Prod.swap (Filter.prod a1 a2) (Filter.prod a2 a1)
theorem Filter.Eventually.prod_inl {α : Type u_1} {β : Type u_2} {la : Filter α} {p : αProp} (h : Filter.Eventually (fun x => p x) la) (lb : Filter β) :
Filter.Eventually (fun x => p x.fst) (Filter.prod la lb)
theorem Filter.Eventually.prod_inr {α : Type u_2} {β : Type u_1} {lb : Filter β} {p : βProp} (h : Filter.Eventually (fun x => p x) lb) (la : Filter α) :
Filter.Eventually (fun x => p x.snd) (Filter.prod la lb)
theorem Filter.Eventually.prod_mk {α : Type u_1} {β : Type u_2} {la : Filter α} {pa : αProp} (ha : Filter.Eventually (fun x => pa x) la) {lb : Filter β} {pb : βProp} (hb : Filter.Eventually (fun y => pb y) lb) :
Filter.Eventually (fun p => pa p.fst pb p.snd) (Filter.prod la lb)
theorem Filter.EventuallyEq.prod_map {α : Type u_2} {β : Type u_4} {γ : Type u_3} {δ : Type u_1} {la : Filter α} {fa : αγ} {ga : αγ} (ha : fa =ᶠ[la] ga) {lb : Filter β} {fb : βδ} {gb : βδ} (hb : fb =ᶠ[lb] gb) :
theorem Filter.EventuallyLE.prod_map {α : Type u_3} {β : Type u_4} {γ : Type u_2} {δ : Type u_1} [inst : LE γ] [inst : LE δ] {la : Filter α} {fa : αγ} {ga : αγ} (ha : fa ≤ᶠ[la] ga) {lb : Filter β} {fb : βδ} {gb : βδ} (hb : fb ≤ᶠ[lb] gb) :
theorem Filter.Eventually.curry {α : Type u_1} {β : Type u_2} {la : Filter α} {lb : Filter β} {p : α × βProp} (h : Filter.Eventually (fun x => p x) (Filter.prod la lb)) :
Filter.Eventually (fun x => Filter.Eventually (fun y => p (x, y)) lb) la
theorem Filter.Eventually.diag_of_prod {α : Type u_1} {f : Filter α} {p : α × αProp} (h : Filter.Eventually (fun i => p i) (Filter.prod f f)) :
Filter.Eventually (fun i => p (i, i)) f

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_2} {f : Filter α} {g : Filter γ} {p : (α × α) × γProp} :
Filter.Eventually (fun x => p x) (Filter.prod (Filter.prod f f) g)Filter.Eventually (fun x => p ((x.fst, x.fst), x.snd)) (Filter.prod f g)
theorem Filter.Eventually.diag_of_prod_right {α : Type u_1} {γ : Type u_2} {f : Filter α} {g : Filter γ} {p : α × γ × γProp} :
Filter.Eventually (fun x => p x) (Filter.prod f (Filter.prod g g))Filter.Eventually (fun x => p (x.fst, x.snd, x.snd)) (Filter.prod f g)
theorem Filter.tendsto_diag {α : Type u_1} {f : Filter α} :
Filter.Tendsto (fun i => (i, i)) f (Filter.prod f f)
theorem Filter.prod_infᵢ_left {α : Type u_2} {β : Type u_3} {ι : Sort u_1} [inst : Nonempty ι] {f : ιFilter α} {g : Filter β} :
Filter.prod (i, f i) g = i, Filter.prod (f i) g
theorem Filter.prod_infᵢ_right {α : Type u_2} {β : Type u_3} {ι : Sort u_1} [inst : Nonempty ι] {f : Filter α} {g : ιFilter β} :
Filter.prod f (i, g i) = i, Filter.prod f (g i)
theorem Filter.prod_mono {α : Type u_1} {β : Type u_2} {f₁ : Filter α} {f₂ : Filter α} {g₁ : Filter β} {g₂ : Filter β} (hf : f₁ f₂) (hg : g₁ g₂) :
Filter.prod f₁ g₁ Filter.prod f₂ g₂
theorem Filter.prod_mono_left {α : Type u_2} {β : Type u_1} (g : Filter β) {f₁ : Filter α} {f₂ : Filter α} (hf : f₁ f₂) :
theorem Filter.prod_mono_right {α : Type u_1} {β : Type u_2} (f : Filter α) {g₁ : Filter β} {g₂ : Filter β} (hf : g₁ g₂) :
theorem Filter.prod_comap_comap_eq {α₁ : Type u} {α₂ : Type v} {β₁ : Type w} {β₂ : Type x} {f₁ : Filter α₁} {f₂ : Filter α₂} {m₁ : β₁α₁} {m₂ : β₂α₂} :
Filter.prod (Filter.comap m₁ f₁) (Filter.comap m₂ f₂) = Filter.comap (fun p => (m₁ p.fst, m₂ p.snd)) (Filter.prod f₁ f₂)
theorem Filter.prod_comm' {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β} :
theorem Filter.prod_comm {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β} :
Filter.prod f g = Filter.map (fun p => (p.snd, p.fst)) (Filter.prod g f)
theorem Filter.mem_prod_iff_left {α : Type u_2} {β : Type u_1} {s : Set (α × β)} {f : Filter α} {g : Filter β} :
s Filter.prod f g t, t f Filter.Eventually (fun y => ∀ (x : α), x t(x, y) s) g
theorem Filter.mem_prod_iff_right {α : Type u_2} {β : Type u_1} {s : Set (α × β)} {f : Filter α} {g : Filter β} :
s Filter.prod f g t, t g Filter.Eventually (fun x => ∀ (y : β), y t(x, y) s) f
@[simp]
theorem Filter.map_fst_prod {α : Type u_1} {β : Type u_2} (f : Filter α) (g : Filter β) [inst : Filter.NeBot g] :
Filter.map Prod.fst (Filter.prod f g) = f
@[simp]
theorem Filter.map_snd_prod {α : Type u_1} {β : Type u_2} (f : Filter α) (g : Filter β) [inst : Filter.NeBot f] :
Filter.map Prod.snd (Filter.prod f g) = g
@[simp]
theorem Filter.prod_le_prod {α : Type u_1} {β : Type u_2} {f₁ : Filter α} {f₂ : Filter α} {g₁ : Filter β} {g₂ : Filter β} [inst : Filter.NeBot f₁] [inst : Filter.NeBot g₁] :
Filter.prod f₁ g₁ Filter.prod f₂ g₂ f₁ f₂ g₁ g₂
@[simp]
theorem Filter.prod_inj {α : Type u_1} {β : Type u_2} {f₁ : Filter α} {f₂ : Filter α} {g₁ : Filter β} {g₂ : Filter β} [inst : Filter.NeBot f₁] [inst : Filter.NeBot g₁] :
Filter.prod f₁ g₁ = Filter.prod f₂ g₂ f₁ = f₂ g₁ = g₂
theorem Filter.eventually_swap_iff {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β} {p : α × βProp} :
Filter.Eventually (fun x => p x) (Filter.prod f g) Filter.Eventually (fun y => p (Prod.swap y)) (Filter.prod g f)
theorem Filter.prod_assoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : Filter α) (g : Filter β) (h : Filter γ) :
theorem Filter.prod_assoc_symm {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : Filter α) (g : Filter β) (h : Filter γ) :
theorem Filter.tendsto_prodAssoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Filter α} {g : Filter β} {h : Filter γ} :
theorem Filter.tendsto_prodAssoc_symm {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Filter α} {g : Filter β} {h : Filter γ} :
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 (fun p => ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) (Filter.prod (Filter.prod f g) (Filter.prod h k)) = Filter.prod (Filter.prod f h) (Filter.prod 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 : Filter α} {g : Filter β} {h : Filter γ} {k : Filter δ} :
Filter.Tendsto (fun p => ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) (Filter.prod (Filter.prod f g) (Filter.prod h k)) (Filter.prod (Filter.prod f h) (Filter.prod g k))
theorem Filter.prod_map_map_eq {α₁ : Type u} {α₂ : Type v} {β₁ : Type w} {β₂ : Type x} {f₁ : Filter α₁} {f₂ : Filter α₂} {m₁ : α₁β₁} {m₂ : α₂β₂} :
Filter.prod (Filter.map m₁ f₁) (Filter.map m₂ f₂) = Filter.map (fun p => (m₁ p.fst, m₂ p.snd)) (Filter.prod f₁ 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 β₁) :
theorem Filter.prod_map_left {α : Type u_1} {β : Type u_3} {γ : Type u_2} (f : αβ) (F : Filter α) (G : Filter γ) :
theorem Filter.prod_map_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : βγ) (F : Filter α) (G : Filter β) :
theorem Filter.le_prod_map_fst_snd {α : Type u_2} {β : Type u_1} {f : Filter (α × β)} :
f Filter.prod (Filter.map Prod.fst f) (Filter.map Prod.snd f)
theorem Filter.Tendsto.prod_map {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_1} {f : αγ} {g : βδ} {a : Filter α} {b : Filter β} {c : Filter γ} {d : Filter δ} (hf : Filter.Tendsto f a c) (hg : Filter.Tendsto g b d) :
theorem Filter.map_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} (m : α × βγ) (f : Filter α) (g : Filter β) :
Filter.map m (Filter.prod 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 : Filter α} {g : Filter β} :
theorem Filter.prod_inf_prod {α : Type u_1} {β : Type u_2} {f₁ : Filter α} {f₂ : Filter α} {g₁ : Filter β} {g₂ : Filter β} :
Filter.prod f₁ g₁ Filter.prod f₂ g₂ = Filter.prod (f₁ f₂) (g₁ g₂)
theorem Filter.inf_prod {α : Type u_1} {β : Type u_2} {f₁ : Filter α} {f₂ : Filter α} {g : Filter β} :
Filter.prod (f₁ f₂) g = Filter.prod f₁ g Filter.prod f₂ g
theorem Filter.prod_inf {α : Type u_1} {β : Type u_2} {f : Filter α} {g₁ : Filter β} {g₂ : Filter β} :
Filter.prod f (g₁ g₂) = Filter.prod f g₁ Filter.prod 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_2} {β : Type u_1} {a : α} {f : Filter β} :
theorem Filter.map_pure_prod {α : Type u_3} {β : Type u_1} {γ : Type u_2} (f : αβγ) (a : α) (B : Filter β) :
@[simp]
theorem Filter.prod_pure {α : Type u_1} {β : Type u_2} {f : Filter α} {b : β} :
Filter.prod f (pure b) = Filter.map (fun a => (a, b)) f
theorem Filter.prod_pure_pure {α : Type u_1} {β : Type u_2} {a : α} {b : β} :
Filter.prod (pure a) (pure b) = pure (a, b)
theorem Filter.prod_eq_bot {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β} :
@[simp]
theorem Filter.prod_bot {α : Type u_1} {β : Type u_2} {f : Filter α} :
@[simp]
theorem Filter.bot_prod {α : Type u_2} {β : Type u_1} {g : Filter β} :
theorem Filter.prod_neBot {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β} :
theorem Filter.NeBot.prod {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β} (hf : Filter.NeBot f) (hg : Filter.NeBot g) :
theorem Filter.tendsto_prod_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α × βγ} {x : Filter α} {y : Filter β} {z : Filter γ} :
Filter.Tendsto f (Filter.prod x y) z ∀ (W : Set γ), W zU, U x V, V y ∀ (x : α) (y : β), x Uy Vf (x, y) W
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 (Filter.prod 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 : Filter α) (g : Filter β) :
Filter (α × β)

Coproduct of filters.

Equations
theorem Filter.mem_coprod_iff {α : Type u_2} {β : Type u_1} {s : Set (α × β)} {f : Filter α} {g : Filter β} :
s Filter.coprod f g (t₁, t₁ f Prod.fst ⁻¹' t₁ s) t₂, t₂ g Prod.snd ⁻¹' t₂ s
@[simp]
theorem Filter.bot_coprod {α : Type u_2} {β : Type u_1} (l : Filter β) :
@[simp]
theorem Filter.coprod_bot {α : Type u_1} {β : Type u_2} (l : Filter α) :
theorem Filter.compl_mem_coprod {α : Type u_2} {β : Type u_1} {s : Set (α × β)} {la : Filter α} {lb : Filter β} :
s Filter.coprod la lb (Prod.fst '' s) la (Prod.snd '' s) lb
theorem Filter.coprod_mono {α : Type u_1} {β : Type u_2} {f₁ : Filter α} {f₂ : Filter α} {g₁ : Filter β} {g₂ : Filter β} (hf : f₁ f₂) (hg : g₁ g₂) :
Filter.coprod f₁ g₁ Filter.coprod f₂ g₂
theorem Filter.coprod_neBot_left {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β} [inst : Filter.NeBot f] [inst : Nonempty β] :
theorem Filter.coprod_neBot_right {α : Type u_2} {β : Type u_1} {f : Filter α} {g : Filter β} [inst : Filter.NeBot g] [inst : Nonempty α] :
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_1} {β : Type u_2} {ι : Type u_3} (a : α) (b : β) (i : ι) :
Filter.coprod (Filter.map (fun x => b) (Filter.principal {a})) (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.

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_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_1} {f : αγ} {g : βδ} {a : Filter α} {b : Filter β} {c : Filter γ} {d : Filter δ} (hf : Filter.Tendsto f a c) (hg : Filter.Tendsto g b d) :