# 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.

## Notation #

- `f ×ˢ g` : `Filter.prod f g`, localized in `Filter`.

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 ×ˢ g
source
theorem Filter.mem_prod_iff {α : Type u_1} {β : Type u_2} {s : Set (α × β)} {f : Filter α} {g : Filter β} :
s ∈ f ×ˢ g ↔ ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ ×ˢ t₂ ⊆ s
source
@[simp]
theorem Filter.compl_diagonal_mem_prod {α : Type u_1} {l₁ l₂ : Filter α} :
(Set.diagonal α)ᶜ ∈ l₁ ×ˢ l₂ ↔ Disjoint l₁ l₂
source
@[simp]
theorem Filter.prod_mem_prod_iff {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : Filter α} {g : Filter β} [f.NeBot] [g.NeBot] :
s ×ˢ t ∈ f ×ˢ g ↔ s ∈ f ∧ t ∈ g
source
theorem Filter.mem_prod_principal {α : Type u_1} {β : Type u_2} {t : Set β} {f : Filter α} {s : Set (α × β)} :
s ∈ f ×ˢ principal t ↔ {a : α | ∀ b ∈ t, (a, b) ∈ s} ∈ f
source
theorem Filter.mem_prod_top {α : Type u_1} {β : Type u_2} {f : Filter α} {s : Set (α × β)} :
s ∈ f ×ˢ ⊤ ↔ {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 ×ˢ principal s, p x) ↔ ∀ᶠ (x : α) in f, ∀ y ∈ s, p (x, y)
source
theorem Filter.comap_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β × γ) (b : Filter β) (c : Filter γ) :
comap f (b ×ˢ c) = comap (Prod.fst ∘ f) b ⊓ comap (Prod.snd ∘ f) c
source
theorem Filter.comap_prodMap_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α → β) (g : γ → δ) (lb : Filter β) (ld : Filter δ) :
comap (Prod.map f g) (lb ×ˢ ld) = comap f lb ×ˢ comap g ld
source
theorem Filter.prod_top {α : Type u_1} {β : Type u_2} {f : Filter α} :
f ×ˢ ⊤ = comap Prod.fst f
source
theorem Filter.top_prod {α : Type u_1} {β : Type u_2} {g : Filter β} :
⊤ ×ˢ g = comap Prod.snd g
source
theorem Filter.sup_prod {α : Type u_1} {β : Type u_2} (f₁ f₂ : Filter α) (g : Filter β) :
(f₁ ⊔ f₂) ×ˢ g = f₁ ×ˢ g ⊔ f₂ ×ˢ g
source
theorem Filter.prod_sup {α : Type u_1} {β : Type u_2} (f : Filter α) (g₁ g₂ : Filter β) :
f ×ˢ (g₁ ⊔ g₂) = f ×ˢ g₁ ⊔ f ×ˢ g₂
source
theorem Filter.eventually_prod_iff {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β} {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)
source
theorem Filter.tendsto_fst {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β} :
Tendsto Prod.fst (f ×ˢ g) f
source
theorem Filter.tendsto_snd {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β} :
Tendsto Prod.snd (f ×ˢ g) g
source
theorem Filter.Tendsto.fst {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Filter α} {g : Filter β} {h : Filter γ} {m : α → β × γ} (H : Tendsto m f (g ×ˢ h)) :
Tendsto (fun (a : α) => (m a).1) f g

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.

source
theorem Filter.Tendsto.snd {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Filter α} {g : Filter β} {h : Filter γ} {m : α → β × γ} (H : Tendsto m f (g ×ˢ h)) :
Tendsto (fun (a : α) => (m a).2) f h

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.

source
theorem Filter.Tendsto.prodMk {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Filter α} {g : Filter β} {h : Filter γ} {m₁ : α → β} {m₂ : α → γ} (h₁ : Tendsto m₁ f g) (h₂ : Tendsto m₂ f h) :
Tendsto (fun (x : α) => (m₁ x, m₂ x)) f (g ×ˢ h)
source
theorem Filter.tendsto_prod_swap {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β} :
Tendsto Prod.swap (f ×ˢ g) (g ×ˢ f)
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 ×ˢ lb, p x.1
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 ×ˢ lb, p x.2
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 ×ˢ lb, pa p.1 ∧ pb p.2
source
theorem Filter.EventuallyEq.prodMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_6} {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
source
theorem Filter.EventuallyLE.prodMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_6} [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
source
theorem Filter.Eventually.curry {α : Type u_1} {β : Type u_2} {la : Filter α} {lb : Filter β} {p : α × β → Prop} (h : ∀ᶠ (x : α × β) in la ×ˢ lb, p x) :
∀ᶠ (x : α) in la, ∀ᶠ (y : β) in lb, p (x, y)
source
theorem Filter.Frequently.uncurry {α : Type u_1} {β : Type u_2} {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
source
theorem Filter.Frequently.of_curry {α : Type u_1} {β : Type u_2} {la : Filter α} {lb : Filter β} {p : α × β → Prop} (h : ∃ᶠ (x : α) in la, ∃ᶠ (y : β) in lb, p (x, y)) :
∃ᶠ (xy : α × β) in la ×ˢ lb, p xy
source
theorem Filter.Eventually.image_of_prod {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β} {y : α → β} {r : α → β → Prop} (hy : Tendsto y f g) (hr : ∀ᶠ (p : α × β) in f ×ˢ g, r p.1 p.2) :
∀ᶠ (x : α) in f, r x (y x)
source
theorem Filter.Eventually.diag_of_prod {α : Type u_1} {f : Filter α} {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)`

source
theorem Filter.Eventually.diag_of_prod_left {α : Type u_1} {γ : Type u_3} {f : Filter α} {g : Filter γ} {p : (α × α) × γ → Prop} :
(∀ᶠ (x : (α × α) × γ) in (f ×ˢ f) ×ˢ g, p x) → ∀ᶠ (x : α × γ) in f ×ˢ g, p ((x.1, x.1), x.2)
source
theorem Filter.Eventually.diag_of_prod_right {α : Type u_1} {γ : Type u_3} {f : Filter α} {g : Filter γ} {p : α × γ × γ → Prop} :
(∀ᶠ (x : α × γ × γ) in f ×ˢ g ×ˢ g, p x) → ∀ᶠ (x : α × γ) in f ×ˢ g, p (x.1, x.2, x.2)
source
theorem Filter.tendsto_diag {α : Type u_1} {f : Filter α} :
Tendsto (fun (i : α) => (i, i)) f (f ×ˢ f)
source
theorem Filter.prod_iInf_left {α : Type u_1} {β : Type u_2} {ι : Sort u_5} [Nonempty ι] {f : ι → Filter α} {g : Filter β} :
(⨅ (i : ι), f i) ×ˢ g = ⨅ (i : ι), f i ×ˢ g
source
theorem Filter.prod_iInf_right {α : Type u_1} {β : Type u_2} {ι : Sort u_5} [Nonempty ι] {f : Filter α} {g : ι → Filter β} :
f ×ˢ ⨅ (i : ι), g i = ⨅ (i : ι), f ×ˢ 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₁ ×ˢ g₁ ≤ f₂ ×ˢ g₂
source
theorem Filter.prod_mono_left {α : Type u_1} {β : Type u_2} (g : Filter β) {f₁ f₂ : Filter α} (hf : f₁ ≤ f₂) :
f₁ ×ˢ g ≤ f₂ ×ˢ g
source
theorem Filter.prod_mono_right {α : Type u_1} {β : Type u_2} (f : Filter α) {g₁ g₂ : Filter β} (hf : g₁ ≤ g₂) :
f ×ˢ g₁ ≤ f ×ˢ g₂
source
theorem Filter.prod_comap_comap_eq {α₁ : 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₂)
source
theorem Filter.prod_comm' {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β} :
f ×ˢ g = comap Prod.swap (g ×ˢ f)
source
theorem Filter.prod_comm {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β} :
f ×ˢ g = map Prod.swap (g ×ˢ f)
source
theorem Filter.mem_prod_iff_left {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β} {s : Set (α × β)} :
s ∈ f ×ˢ g ↔ ∃ t ∈ f, ∀ᶠ (y : β) in g, ∀ x ∈ t, (x, y) ∈ s
source
theorem Filter.mem_prod_iff_right {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β} {s : Set (α × β)} :
s ∈ f ×ˢ g ↔ ∃ t ∈ g, ∀ᶠ (x : α) in f, ∀ y ∈ t, (x, y) ∈ s
source
@[simp]
theorem Filter.map_fst_prod {α : Type u_1} {β : Type u_2} (f : Filter α) (g : Filter β) [g.NeBot] :
map Prod.fst (f ×ˢ g) = f
source
@[simp]
theorem Filter.map_snd_prod {α : Type u_1} {β : Type u_2} (f : Filter α) (g : Filter β) [f.NeBot] :
map Prod.snd (f ×ˢ g) = g
source
@[simp]
theorem Filter.prod_le_prod {α : Type u_1} {β : Type u_2} {f₁ f₂ : Filter α} {g₁ g₂ : Filter β} [f₁.NeBot] [g₁.NeBot] :
f₁ ×ˢ g₁ ≤ f₂ ×ˢ g₂ ↔ f₁ ≤ f₂ ∧ g₁ ≤ g₂
source
@[simp]
theorem Filter.prod_inj {α : Type u_1} {β : Type u_2} {f₁ f₂ : Filter α} {g₁ g₂ : Filter β} [f₁.NeBot] [g₁.NeBot] :
f₁ ×ˢ g₁ = f₂ ×ˢ 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 ×ˢ g, p x) ↔ ∀ᶠ (y : β × α) in g ×ˢ f, p y.swap
source
theorem Filter.Eventually.eventually_prod_of_eventually_swap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Filter α} {g : Filter β} {h : Filter γ} [g.NeBot] {p : α → β → Prop} {q : β → γ → Prop} {r : α → γ → Prop} (hp : ∀ᶠ (x : α) in f, ∀ᶠ (y : β) in g, p x y) (hq : ∀ᶠ (z : γ) in h, ∀ᶠ (y : β) in g, q y z) (hpqr : ∀ (x : α) (y : β) (z : γ), p x y → q y z → r x z) :
∀ᶠ (xz : α × γ) in f ×ˢ h, r xz.1 xz.2

A technical lemma which is a generalization of `Filter.Eventually.trans_prod`.

source
theorem Filter.Eventually.trans_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Filter α} {g : Filter β} {h : Filter γ} [g.NeBot] {p : α → β → Prop} {q : β → γ → Prop} {r : α → γ → Prop} (hp : ∀ᶠ (xy : α × β) in f ×ˢ g, p xy.1 xy.2) (hq : ∀ᶠ (yz : β × γ) in g ×ˢ h, q yz.1 yz.2) (hpqr : ∀ (x : α) (y : β) (z : γ), p x y → q y z → r x z) :
∀ᶠ (xz : α × γ) in f ×ˢ h, r xz.1 xz.2
source
theorem Filter.prod_assoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : Filter α) (g : Filter β) (h : Filter γ) :
map (⇑(Equiv.prodAssoc α β γ)) ((f ×ˢ g) ×ˢ h) = f ×ˢ g ×ˢ h
source
theorem Filter.prod_assoc_symm {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : Filter α) (g : Filter β) (h : Filter γ) :
map (⇑(Equiv.prodAssoc α β γ).symm) (f ×ˢ g ×ˢ h) = (f ×ˢ g) ×ˢ h
source
theorem Filter.tendsto_prodAssoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Filter α} {g : Filter β} {h : Filter γ} :
Tendsto (⇑(Equiv.prodAssoc α β γ)) ((f ×ˢ g) ×ˢ h) (f ×ˢ g ×ˢ h)
source
theorem Filter.tendsto_prodAssoc_symm {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Filter α} {g : Filter β} {h : Filter γ} :
Tendsto (⇑(Equiv.prodAssoc α β γ).symm) (f ×ˢ g ×ˢ h) ((f ×ˢ g) ×ˢ 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 δ} :
map (fun (p : (α × β) × γ × δ) => ((p.1.1, p.2.1), p.1.2, p.2.2)) ((f ×ˢ g) ×ˢ h ×ˢ k) = (f ×ˢ h) ×ˢ g ×ˢ 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 δ} :
Tendsto (fun (p : (α × β) × γ × δ) => ((p.1.1, p.2.1), p.1.2, p.2.2)) ((f ×ˢ g) ×ˢ h ×ˢ k) ((f ×ˢ h) ×ˢ g ×ˢ k)
source
theorem Filter.prod_map_map_eq {α₁ : 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₂)
source
theorem Filter.prod_map_map_eq' {α₁ : Type u_6} {α₂ : Type u_7} {β₁ : Type u_8} {β₂ : Type u_9} (f : α₁ → α₂) (g : β₁ → β₂) (F : Filter α₁) (G : Filter β₁) :
map f F ×ˢ map g G = map (Prod.map f g) (F ×ˢ G)
source
theorem Filter.prod_map_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β) (F : Filter α) (G : Filter γ) :
map f F ×ˢ G = map (Prod.map f id) (F ×ˢ G)
source
theorem Filter.prod_map_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : β → γ) (F : Filter α) (G : Filter β) :
F ×ˢ map f G = map (Prod.map id f) (F ×ˢ G)
source
theorem Filter.le_prod_map_fst_snd {α : Type u_1} {β : Type u_2} {f : Filter (α × β)} :
f ≤ map Prod.fst f ×ˢ map Prod.snd f
source
theorem Filter.Tendsto.prodMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_6} {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)
source
theorem Filter.map_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} (m : α × β → γ) (f : Filter α) (g : Filter β) :
map m (f ×ˢ g) = (map (fun (a : α) (b : β) => m (a, b)) f).seq g
source
theorem Filter.prod_eq {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β} :
f ×ˢ g = (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₁ ×ˢ g₁ ⊓ f₂ ×ˢ g₂ = (f₁ ⊓ f₂) ×ˢ (g₁ ⊓ g₂)
source
theorem Filter.inf_prod {α : Type u_1} {β : Type u_2} {g : Filter β} {f₁ f₂ : Filter α} :
(f₁ ⊓ f₂) ×ˢ g = f₁ ×ˢ g ⊓ f₂ ×ˢ g
source
theorem Filter.prod_inf {α : Type u_1} {β : Type u_2} {f : Filter α} {g₁ g₂ : Filter β} :
f ×ˢ (g₁ ⊓ g₂) = f ×ˢ g₁ ⊓ f ×ˢ g₂
source
@[simp]
theorem Filter.prod_principal_principal {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} :
principal s ×ˢ principal t = principal (s ×ˢ t)
source
@[simp]
theorem Filter.pure_prod {α : Type u_1} {β : Type u_2} {a : α} {f : Filter β} :
pure a ×ˢ f = map (Prod.mk a) f
source
theorem Filter.map_pure_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (a : α) (B : Filter β) :
map (Function.uncurry f) (pure a ×ˢ B) = map (f a) B
source
@[simp]
theorem Filter.prod_pure {α : Type u_1} {β : Type u_2} {f : Filter α} {b : β} :
f ×ˢ pure b = map (fun (a : α) => (a, b)) f
source
theorem Filter.prod_pure_pure {α : Type u_1} {β : Type u_2} {a : α} {b : β} :
pure a ×ˢ pure b = pure (a, b)
source
@[simp]
theorem Filter.prod_eq_bot {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β} :
f ×ˢ g = ⊥ ↔ f = ⊥ ∨ g = ⊥
source
@[simp]
theorem Filter.prod_bot {α : Type u_1} {β : Type u_2} {f : Filter α} :
f ×ˢ ⊥ = ⊥
source
@[simp]
theorem Filter.bot_prod {α : Type u_1} {β : Type u_2} {g : Filter β} :
⊥ ×ˢ g = ⊥
source
theorem Filter.prod_neBot {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β} :
(f ×ˢ g).NeBot ↔ f.NeBot ∧ g.NeBot
source
theorem Filter.NeBot.prod {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β} (hf : f.NeBot) (hg : g.NeBot) :
(f ×ˢ g).NeBot
source
instance Filter.prod.instNeBot {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β} [hf : f.NeBot] [hg : g.NeBot] :
(f ×ˢ g).NeBot
source
@[simp]
theorem Filter.disjoint_prod {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β} {f' : Filter α} {g' : Filter β} :
Disjoint (f ×ˢ g) (f' ×ˢ g') ↔ Disjoint f f' ∨ Disjoint g g'
source
theorem Filter.frequently_prod_and {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β} {p : α → Prop} {q : β → Prop} :
(∃ᶠ (x : α × β) in f ×ˢ g, p x.1 ∧ q x.2) ↔ (∃ᶠ (a : α) in f, p a) ∧ ∃ᶠ (b : β) in g, q b

`p ∧ q` occurs frequently along the product of two filters iff both `p` and `q` occur frequently along the corresponding filters.

source
theorem Filter.tendsto_prod_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {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
source
theorem Filter.tendsto_prod_iff' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Filter α} {g : Filter β} {g' : Filter γ} {s : α → β × γ} :
Tendsto s f (g ×ˢ g') ↔ Tendsto (fun (n : α) => (s n).1) f g ∧ Tendsto (fun (n : α) => (s n).2) f g'
source
theorem Filter.le_prod {α : Type u_1} {β : Type u_2} {f : Filter (α × β)} {g : Filter α} {g' : Filter β} :
f ≤ g ×ˢ g' ↔ Tendsto Prod.fst f g ∧ Tendsto Prod.snd f g'

### Coproducts of filters #

source
theorem Filter.coprod_eq_prod_top_sup_top_prod {α : Type u_1} {β : Type u_2} (f : Filter α) (g : Filter β) :
f.coprod g = f ×ˢ ⊤ ⊔ ⊤ ×ˢ g
source
theorem Filter.mem_coprod_iff {α : Type u_1} {β : Type u_2} {s : Set (α × β)} {f : Filter α} {g : Filter β} :
s ∈ f.coprod g ↔ (∃ t₁ ∈ f, Prod.fst ⁻¹' t₁ ⊆ s) ∧ ∃ t₂ ∈ g, Prod.snd ⁻¹' t₂ ⊆ s
source
@[simp]
theorem Filter.bot_coprod {α : Type u_1} {β : Type u_2} (l : Filter β) :
⊥.coprod l = comap Prod.snd l
source
@[simp]
theorem Filter.coprod_bot {α : Type u_1} {β : Type u_2} (l : Filter α) :
l.coprod ⊥ = 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_neBot_iff {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β} :
(f.coprod g).NeBot ↔ f.NeBot ∧ Nonempty β ∨ Nonempty α ∧ g.NeBot
source
instance Filter.coprod_neBot_left {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β} [f.NeBot] [Nonempty β] :
(f.coprod g).NeBot
source
instance Filter.coprod_neBot_right {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β} [g.NeBot] [Nonempty α] :
(f.coprod g).NeBot
source
theorem Filter.coprod_inf_prod_le {α : Type u_1} {β : Type u_2} (f₁ f₂ : Filter α) (g₁ g₂ : Filter β) :
f₁.coprod g₁ ⊓ f₂ ×ˢ g₂ ≤ f₁ ×ˢ g₂ ⊔ f₂ ×ˢ g₁
source
theorem Filter.principal_coprod_principal {α : Type u_1} {β : Type u_2} (s : Set α) (t : Set β) :
(principal s).coprod (principal t) = principal (s ᶜ ×ˢ t ᶜ)ᶜ
source
theorem Filter.map_prodMap_coprod_le {α₁ : 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₂)
source
theorem Filter.map_const_principal_coprod_map_id_principal {α : Type u_6} {β : Type u_7} {ι : Type u_8} (a : α) (b : β) (i : ι) :
(map (fun (x : α) => b) (principal {a})).coprod (map id (principal {i})) = principal ({b} ×ˢ Set.univ ∪ Set.univ ×ˢ {i})

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.

source
theorem Filter.map_prodMap_const_id_principal_coprod_principal {α : Type u_6} {β : Type u_7} {ι : Type u_8} (a : α) (b : β) (i : ι) :
map (Prod.map (fun (x : α) => b) id) ((principal {a}).coprod (principal {i})) = 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_prodMap_coprod_le` can be strict.

source
theorem Filter.Tendsto.prodMap_coprod {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_6} {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)
source
theorem Filter.Tendsto.coprod_of_prod_top_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α × β → γ} {la : Filter α} {lb : Filter β} {lc : Filter γ} (h₁ : ∀ s ∈ la, Tendsto f (principal s ᶜ ×ˢ lb) lc) (h₂ : Tendsto f (la ×ˢ ⊤) lc) :
Tendsto f (la.coprod lb) lc
source
theorem Filter.Tendsto.coprod_of_prod_top_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α × β → γ} {la : Filter α} {lb : Filter β} {lc : Filter γ} (h₁ : ∀ s ∈ lb, Tendsto f (la ×ˢ principal s ᶜ) lc) (h₂ : Tendsto f (⊤ ×ˢ lb) lc) :
Tendsto f (la.coprod lb) lc