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.

ink

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

• Filter.prod f g = Filter.comap Prod.fst f ⊓ Filter.comap Prod.snd g

ink

def Filter.«term_×ᶠ_» : Lean.TrailingParserDescr

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

Equations

• Filter.«term_×ᶠ_» = Lean.ParserDescr.trailingNode `Filter.term_×ᶠ_ 60 60 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ×ᶠ ") (Lean.ParserDescr.cat `term 61))

ink

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 ∈ Filter.prod f g

ink

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

ink

@[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

ink

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

ink

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

ink

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 ∈ s → p (x, y)) f

ink

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

ink

theorem Filter.prod_top {α : Type u_1} {β : Type u_2} {f : Filter α} : Filter.prod f ⊤ = Filter.comap Prod.fst f

ink

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

ink

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₂

ink

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 y → p (x, y))

ink

theorem Filter.tendsto_fst {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β} : Filter.Tendsto Prod.fst (Filter.prod f g) f

ink

theorem Filter.tendsto_snd {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β} : Filter.Tendsto Prod.snd (Filter.prod f g) g

ink

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)

ink

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)

ink

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)

ink

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)

ink

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)

ink

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) : Prod.map fa fb =ᶠ[Filter.prod la lb] Prod.map ga gb

ink

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) : Prod.map fa fb ≤ᶠ[Filter.prod la lb] Prod.map ga gb

ink

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

ink

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)

ink

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)

ink

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)

ink

theorem Filter.tendsto_diag {α : Type u_1} {f : Filter α} : Filter.Tendsto (fun i => (i, i)) f (Filter.prod f f)

ink

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

ink

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)

ink

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₂

ink

theorem Filter.prod_mono_left {α : Type u_2} {β : Type u_1} (g : Filter β) {f₁ : Filter α} {f₂ : Filter α} (hf : f₁ ≤ f₂) : Filter.prod f₁ g ≤ Filter.prod f₂ g

ink

theorem Filter.prod_mono_right {α : Type u_1} {β : Type u_2} (f : Filter α) {g₁ : Filter β} {g₂ : Filter β} (hf : g₁ ≤ g₂) : Filter.prod f g₁ ≤ Filter.prod f g₂

ink

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₂)

ink

theorem Filter.prod_comm' {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β} : Filter.prod f g = Filter.comap Prod.swap (Filter.prod g f)

ink

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)

ink

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

ink

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

ink

@[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

ink

@[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

ink

@[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₂

ink

@[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₂

ink

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)

ink

theorem Filter.prod_assoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : Filter α) (g : Filter β) (h : Filter γ) : Filter.map (↑(Equiv.prodAssoc α β γ)) (Filter.prod (Filter.prod f g) h) = Filter.prod f (Filter.prod g h)

ink

theorem Filter.prod_assoc_symm {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : Filter α) (g : Filter β) (h : Filter γ) : Filter.map (↑(Equiv.symm (Equiv.prodAssoc α β γ))) (Filter.prod f (Filter.prod g h)) = Filter.prod (Filter.prod f g) h

ink

theorem Filter.tendsto_prodAssoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Filter α} {g : Filter β} {h : Filter γ} : Filter.Tendsto (↑(Equiv.prodAssoc α β γ)) (Filter.prod (Filter.prod f g) h) (Filter.prod f (Filter.prod g h))

ink

theorem Filter.tendsto_prodAssoc_symm {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Filter α} {g : Filter β} {h : Filter γ} : Filter.Tendsto (↑(Equiv.symm (Equiv.prodAssoc α β γ))) (Filter.prod f (Filter.prod g h)) (Filter.prod (Filter.prod f g) h)

ink

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.

ink

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))

ink

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₂)

ink

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.prod (Filter.map f F) (Filter.map g G) = Filter.map (Prod.map f g) (Filter.prod F G)

ink

theorem Filter.prod_map_left {α : Type u_1} {β : Type u_3} {γ : Type u_2} (f : α → β) (F : Filter α) (G : Filter γ) : Filter.prod (Filter.map f F) G = Filter.map (Prod.map f id) (Filter.prod F G)

ink

theorem Filter.prod_map_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : β → γ) (F : Filter α) (G : Filter β) : Filter.prod F (Filter.map f G) = Filter.map (Prod.map id f) (Filter.prod F G)

ink

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)

ink

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) : Filter.Tendsto (Prod.map f g) (Filter.prod a b) (Filter.prod c d)

ink

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

ink

theorem Filter.prod_eq {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β} : Filter.prod f g = Filter.seq (Filter.map Prod.mk f) g

ink

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₂)

ink

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

ink

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₂

ink

@[simp]

theorem Filter.prod_principal_principal {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} : Filter.prod (Filter.principal s) (Filter.principal t) = Filter.principal (s ×ˢ t)

ink

@[simp]

theorem Filter.pure_prod {α : Type u_2} {β : Type u_1} {a : α} {f : Filter β} : Filter.prod (pure a) f = Filter.map (Prod.mk a) f

ink

theorem Filter.map_pure_prod {α : Type u_3} {β : Type u_1} {γ : Type u_2} (f : α → β → γ) (a : α) (B : Filter β) : Filter.map (Function.uncurry f) (Filter.prod (pure a) B) = Filter.map (f a) B

ink

@[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

ink

theorem Filter.prod_pure_pure {α : Type u_1} {β : Type u_2} {a : α} {b : β} : Filter.prod (pure a) (pure b) = pure (a, b)

ink

theorem Filter.prod_eq_bot {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β} : Filter.prod f g = ⊥ ↔ f = ⊥ ∨ g = ⊥

ink

@[simp]

theorem Filter.prod_bot {α : Type u_1} {β : Type u_2} {f : Filter α} : Filter.prod f ⊥ = ⊥

ink

@[simp]

theorem Filter.bot_prod {α : Type u_2} {β : Type u_1} {g : Filter β} : Filter.prod ⊥ g = ⊥

ink

theorem Filter.prod_neBot {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β} : Filter.NeBot (Filter.prod f g) ↔ Filter.NeBot f ∧ Filter.NeBot g

ink

theorem Filter.NeBot.prod {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β} (hf : Filter.NeBot f) (hg : Filter.NeBot g) : Filter.NeBot (Filter.prod f g)

ink

instance Filter.prod_neBot' {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β} [hf : Filter.NeBot f] [hg : Filter.NeBot g] : Filter.NeBot (Filter.prod f g)

Equations

• @Filter.prod_neBot' = @Filter.prod_neBot'.proof_1

ink

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 ∈ z → ∃ U, U ∈ x ∧ ∃ V, V ∈ y ∧ ∀ (x : α) (y : β), x ∈ U → y ∈ V → f (x, y) ∈ W

ink

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

ink

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

Coproduct of filters.

Equations

• Filter.coprod f g = Filter.comap Prod.fst f ⊔ Filter.comap Prod.snd g

ink

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

ink

@[simp]

theorem Filter.bot_coprod {α : Type u_2} {β : Type u_1} (l : Filter β) : Filter.coprod ⊥ l = Filter.comap Prod.snd l

ink

@[simp]

theorem Filter.coprod_bot {α : Type u_1} {β : Type u_2} (l : Filter α) : Filter.coprod l ⊥ = Filter.comap Prod.fst l

ink

theorem Filter.bot_coprod_bot {α : Type u_1} {β : Type u_2} : Filter.coprod ⊥ ⊥ = ⊥

ink

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

ink

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₂

ink

theorem Filter.coprod_neBot_iff {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β} : Filter.NeBot (Filter.coprod f g) ↔ Filter.NeBot f ∧ Nonempty β ∨ Nonempty α ∧ Filter.NeBot g

ink

theorem Filter.coprod_neBot_left {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β} [inst : Filter.NeBot f] [inst : Nonempty β] : Filter.NeBot (Filter.coprod f g)

ink

theorem Filter.coprod_neBot_right {α : Type u_2} {β : Type u_1} {f : Filter α} {g : Filter β} [inst : Filter.NeBot g] [inst : Nonempty α] : Filter.NeBot (Filter.coprod f g)

ink

theorem Filter.principal_coprod_principal {α : Type u_1} {β : Type u_2} (s : Set α) (t : Set β) : Filter.coprod (Filter.principal s) (Filter.principal t) = Filter.principal ((sᶜ ×ˢ tᶜ)ᶜ)

ink

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₂)

ink

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.

ink

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 (fun x => b) id) (Filter.coprod (Filter.principal {a}) (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.

ink

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) : Filter.Tendsto (Prod.map f g) (Filter.coprod a b) (Filter.coprod c d)