(Co)product of a family of filters #

In this file we define two filters on Π i, α i and prove some basic properties of these filters.

filter.pi (f : Π i, filter (α i)) to be the maximal filter on Π i, α i such that ∀ i, filter.tendsto (function.eval i) (filter.pi f) (f i). It is defined as Π i, filter.comap (function.eval i) (f i). This is a generalization of filter.prod to indexed products.
filter.Coprod (f : Π i, filter (α i)): a generalization of filter.coprod; it is the supremum of comap (eval i) (f i).

source

def filter.pi {ι : Type u_1} {α : ι → Type u_2} (f : Π (i : ι), filter (α i)) :

filter (Π (i : ι), α i)

The product of an indexed family of filters.

Equations

filter.pi f = ⨅ (i : ι), filter.comap (function.eval i) (f i)

source

theorem filter.tendsto_eval_pi {ι : Type u_1} {α : ι → Type u_2} (f : Π (i : ι), filter (α i)) (i : ι) :

filter.tendsto (function.eval i) (filter.pi f) (f i)

source

theorem filter.tendsto_pi {ι : Type u_1} {α : ι → Type u_2} {f : Π (i : ι), filter (α i)} {β : Type u_3} {m : β → Π (i : ι), α i} {l : filter β} :

filter.tendsto m l (filter.pi f) ↔ ∀ (i : ι), filter.tendsto (λ (x : β), m x i) l (f i)

source

theorem filter.le_pi {ι : Type u_1} {α : ι → Type u_2} {f : Π (i : ι), filter (α i)} {g : filter (Π (i : ι), α i)} :

g ≤ filter.pi f ↔ ∀ (i : ι), filter.tendsto (function.eval i) g (f i)

source

theorem filter.pi_mono {ι : Type u_1} {α : ι → Type u_2} {f₁ f₂ : Π (i : ι), filter (α i)} (h : ∀ (i : ι), f₁ i ≤ f₂ i) :

filter.pi f₁ ≤ filter.pi f₂

source

theorem filter.mem_pi_of_mem {ι : Type u_1} {α : ι → Type u_2} {f : Π (i : ι), filter (α i)} (i : ι) {s : set (α i)} (hs : s ∈ f i) :

function.eval i ⁻¹' s ∈ filter.pi f

source

theorem filter.pi_mem_pi {ι : Type u_1} {α : ι → Type u_2} {f : Π (i : ι), filter (α i)} {s : Π (i : ι), set (α i)} {I : set ι} (hI : I.finite) (h : ∀ (i : ι), i ∈ I → s i ∈ f i) :

I.pi s ∈ filter.pi f

source

theorem filter.mem_pi {ι : Type u_1} {α : ι → Type u_2} {f : Π (i : ι), filter (α i)} {s : set (Π (i : ι), α i)} :

s ∈ filter.pi f ↔ ∃ (I : set ι), I.finite ∧ ∃ (t : Π (i : ι), set (α i)), (∀ (i : ι), t i ∈ f i) ∧ I.pi t ⊆ s

source

theorem filter.mem_pi' {ι : Type u_1} {α : ι → Type u_2} {f : Π (i : ι), filter (α i)} {s : set (Π (i : ι), α i)} :

s ∈ filter.pi f ↔ ∃ (I : finset ι) (t : Π (i : ι), set (α i)), (∀ (i : ι), t i ∈ f i) ∧ ↑I.pi t ⊆ s

source

theorem filter.mem_of_pi_mem_pi {ι : Type u_1} {α : ι → Type u_2} {f : Π (i : ι), filter (α i)} {s : Π (i : ι), set (α i)} [∀ (i : ι), (f i).ne_bot] {I : set ι} (h : I.pi s ∈ filter.pi f) {i : ι} (hi : i ∈ I) :

s i ∈ f i

source

@[simp]

theorem filter.pi_mem_pi_iff {ι : Type u_1} {α : ι → Type u_2} {f : Π (i : ι), filter (α i)} {s : Π (i : ι), set (α i)} [∀ (i : ι), (f i).ne_bot] {I : set ι} (hI : I.finite) :

I.pi s ∈ filter.pi f ↔ ∀ (i : ι), i ∈ I → s i ∈ f i

source

theorem filter.has_basis_pi {ι : Type u_1} {α : ι → Type u_2} {f : Π (i : ι), filter (α i)} {ι' : ι → Type} {s : Π (i : ι), ι' i → set (α i)} {p : Π (i : ι), ι' i → Prop} (h : ∀ (i : ι), (f i).has_basis (p i) (s i)) :

(filter.pi f).has_basis (λ (If : set ι × Π (i : ι), ι' i), If.fst.finite ∧ ∀ (i : ι), i ∈ If.fst → p i (If.snd i)) (λ (If : set ι × Π (i : ι), ι' i), If.fst.pi (λ (i : ι), s i (If.snd i)))

source

@[simp]

theorem filter.pi_inf_principal_univ_pi_eq_bot {ι : Type u_1} {α : ι → Type u_2} {f : Π (i : ι), filter (α i)} {s : Π (i : ι), set (α i)} :

filter.pi f ⊓ 𝓟 (set.univ.pi s) = ⊥ ↔ ∃ (i : ι), f i ⊓ 𝓟 (s i) = ⊥

source

@[simp]

theorem filter.pi_inf_principal_pi_eq_bot {ι : Type u_1} {α : ι → Type u_2} {f : Π (i : ι), filter (α i)} {s : Π (i : ι), set (α i)} [∀ (i : ι), (f i).ne_bot] {I : set ι} :

filter.pi f ⊓ 𝓟 (I.pi s) = ⊥ ↔ ∃ (i : ι) (H : i ∈ I), f i ⊓ 𝓟 (s i) = ⊥

source

@[simp]

theorem filter.pi_inf_principal_univ_pi_ne_bot {ι : Type u_1} {α : ι → Type u_2} {f : Π (i : ι), filter (α i)} {s : Π (i : ι), set (α i)} :

(filter.pi f ⊓ 𝓟 (set.univ.pi s)).ne_bot ↔ ∀ (i : ι), (f i ⊓ 𝓟 (s i)).ne_bot

source

@[simp]

theorem filter.pi_inf_principal_pi_ne_bot {ι : Type u_1} {α : ι → Type u_2} {f : Π (i : ι), filter (α i)} {s : Π (i : ι), set (α i)} [∀ (i : ι), (f i).ne_bot] {I : set ι} :

(filter.pi f ⊓ 𝓟 (I.pi s)).ne_bot ↔ ∀ (i : ι), i ∈ I → (f i ⊓ 𝓟 (s i)).ne_bot

source

@[protected, instance]

def filter.pi_inf_principal_pi.ne_bot {ι : Type u_1} {α : ι → Type u_2} {f : Π (i : ι), filter (α i)} {s : Π (i : ι), set (α i)} [h : ∀ (i : ι), (f i ⊓ 𝓟 (s i)).ne_bot] {I : set ι} :

(filter.pi f ⊓ 𝓟 (I.pi s)).ne_bot

source

@[simp]

theorem filter.pi_eq_bot {ι : Type u_1} {α : ι → Type u_2} {f : Π (i : ι), filter (α i)} :

filter.pi f = ⊥ ↔ ∃ (i : ι), f i = ⊥

source

@[simp]

theorem filter.pi_ne_bot {ι : Type u_1} {α : ι → Type u_2} {f : Π (i : ι), filter (α i)} :

(filter.pi f).ne_bot ↔ ∀ (i : ι), (f i).ne_bot

source

@[protected, instance]

def filter.pi.ne_bot {ι : Type u_1} {α : ι → Type u_2} {f : Π (i : ι), filter (α i)} [∀ (i : ι), (f i).ne_bot] :

(filter.pi f).ne_bot

`n`-ary coproducts of filters #

source

@[protected]

def filter.Coprod {ι : Type u_1} {α : ι → Type u_2} (f : Π (i : ι), filter (α i)) :

filter (Π (i : ι), α i)

Coproduct of filters.

Equations

filter.Coprod f = ⨆ (i : ι), filter.comap (function.eval i) (f i)

source

theorem filter.mem_Coprod_iff {ι : Type u_1} {α : ι → Type u_2} {f : Π (i : ι), filter (α i)} {s : set (Π (i : ι), α i)} :

s ∈ filter.Coprod f ↔ ∀ (i : ι), ∃ (t₁ : set (α i)) (H : t₁ ∈ f i), function.eval i ⁻¹' t₁ ⊆ s

source

theorem filter.compl_mem_Coprod_iff {ι : Type u_1} {α : ι → Type u_2} {f : Π (i : ι), filter (α i)} {s : set (Π (i : ι), α i)} :

sᶜ ∈ filter.Coprod f ↔ ∃ (t : Π (i : ι), set (α i)), (∀ (i : ι), (t i)ᶜ ∈ f i) ∧ s ⊆ set.univ.pi (λ (i : ι), t i)

source

theorem filter.Coprod_ne_bot_iff' {ι : Type u_1} {α : ι → Type u_2} {f : Π (i : ι), filter (α i)} :

(filter.Coprod f).ne_bot ↔ (∀ (i : ι), nonempty (α i)) ∧ ∃ (d : ι), (f d).ne_bot

source

@[simp]

theorem filter.Coprod_ne_bot_iff {ι : Type u_1} {α : ι → Type u_2} {f : Π (i : ι), filter (α i)} [∀ (i : ι), nonempty (α i)] :

(filter.Coprod f).ne_bot ↔ ∃ (d : ι), (f d).ne_bot

source

theorem filter.ne_bot.Coprod {ι : Type u_1} {α : ι → Type u_2} {f : Π (i : ι), filter (α i)} [∀ (i : ι), nonempty (α i)] {i : ι} (h : (f i).ne_bot) :

(filter.Coprod f).ne_bot

source

@[instance]

theorem filter.Coprod_ne_bot {ι : Type u_1} {α : ι → Type u_2} [∀ (i : ι), nonempty (α i)] [nonempty ι] (f : Π (i : ι), filter (α i)) [H : ∀ (i : ι), (f i).ne_bot] :

(filter.Coprod f).ne_bot

source

theorem filter.Coprod_mono {ι : Type u_1} {α : ι → Type u_2} {f₁ f₂ : Π (i : ι), filter (α i)} (hf : ∀ (i : ι), f₁ i ≤ f₂ i) :

filter.Coprod f₁ ≤ filter.Coprod f₂

source

theorem filter.map_pi_map_Coprod_le {ι : Type u_1} {α : ι → Type u_2} {f : Π (i : ι), filter (α i)} {β : ι → Type u_3} {m : Π (i : ι), α i → β i} :

filter.map (λ (k : Π (i : ι), α i) (i : ι), m i (k i)) (filter.Coprod f) ≤ filter.Coprod (λ (i : ι), filter.map (m i) (f i))

source

theorem filter.tendsto.pi_map_Coprod {ι : Type u_1} {α : ι → Type u_2} {f : Π (i : ι), filter (α i)} {β : ι → Type u_3} {m : Π (i : ι), α i → β i} {g : Π (i : ι), filter (β i)} (h : ∀ (i : ι), filter.tendsto (m i) (f i) (g i)) :

filter.tendsto (λ (k : Π (i : ι), α i) (i : ι), m i (k i)) (filter.Coprod f) (filter.Coprod g)

(Co)product of a family of filters #

n-ary coproducts of filters #

`n`-ary coproducts of filters #