order.filter.pi

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

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
• = ⨅ (i : ι), (f i)
Instances for filter.pi
@[protected, instance]
def filter.pi.is_countably_generated {ι : Type u_1} {α : ι → Type u_2} {f : Π (i : ι), filter (α i)} [countable ι] [∀ (i : ι), (f i).is_countably_generated] :
theorem filter.tendsto_eval_pi {ι : Type u_1} {α : ι → Type u_2} (f : Π (i : ι), filter (α i)) (i : ι) :
(filter.pi f) (f i)
theorem filter.tendsto_pi {ι : Type u_1} {α : ι → Type u_2} {f : Π (i : ι), filter (α i)} {β : Type u_3} {m : β → Π (i : ι), α i} {l : filter β} :
(filter.pi f) ∀ (i : ι), filter.tendsto (λ (x : β), m x i) l (f i)
theorem filter.le_pi {ι : Type u_1} {α : ι → Type u_2} {f : Π (i : ι), filter (α i)} {g : filter (Π (i : ι), α i)} :
g ∀ (i : ι), (f i)
theorem filter.pi_mono {ι : Type u_1} {α : ι → Type u_2} {f₁ f₂ : Π (i : ι), filter (α i)} (h : ∀ (i : ι), f₁ i f₂ i) :
theorem filter.mem_pi_of_mem {ι : Type u_1} {α : ι → Type u_2} {f : Π (i : ι), filter (α i)} (i : ι) {s : set (α i)} (hs : s f i) :
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 Is i f i) :
I.pi s
theorem filter.mem_pi {ι : Type u_1} {α : ι → Type u_2} {f : Π (i : ι), filter (α i)} {s : set (Π (i : ι), α i)} :
s ∃ (I : set ι), I.finite ∃ (t : Π (i : ι), set (α i)), (∀ (i : ι), t i f i) I.pi t s
theorem filter.mem_pi' {ι : Type u_1} {α : ι → Type u_2} {f : Π (i : ι), filter (α i)} {s : set (Π (i : ι), α i)} :
s ∃ (I : finset ι) (t : Π (i : ι), set (α i)), (∀ (i : ι), t i f i) I.pi t s
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 ) {i : ι} (hi : i I) :
s i f i
@[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 ∀ (i : ι), i Is i f i
theorem filter.has_basis_pi {ι : Type u_1} {α : ι → Type u_2} {f : Π (i : ι), filter (α i)} {ι' : ι → Type} {s : Π (i : ι), ι' iset (α 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.fstp i (If.snd i)) (λ (If : set ι × Π (i : ι), ι' i), If.fst.pi (λ (i : ι), s i (If.snd i)))
@[simp]
theorem filter.pi_inf_principal_univ_pi_eq_bot {ι : Type u_1} {α : ι → Type u_2} {f : Π (i : ι), filter (α i)} {s : Π (i : ι), set (α i)} :
= ∃ (i : ι), f i filter.principal (s i) =
@[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.principal (I.pi s) = ∃ (i : ι) (H : i I), f i filter.principal (s i) =
@[simp]
theorem filter.pi_inf_principal_univ_pi_ne_bot {ι : Type u_1} {α : ι → Type u_2} {f : Π (i : ι), filter (α i)} {s : Π (i : ι), set (α i)} :
.ne_bot ∀ (i : ι), (f i filter.principal (s i)).ne_bot
@[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.principal (I.pi s)).ne_bot ∀ (i : ι), i I(f i filter.principal (s i)).ne_bot
@[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 filter.principal (s i)).ne_bot] {I : set ι} :
@[simp]
theorem filter.pi_eq_bot {ι : Type u_1} {α : ι → Type u_2} {f : Π (i : ι), filter (α i)} :
∃ (i : ι), f i =
@[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
@[protected, instance]
def filter.pi.ne_bot {ι : Type u_1} {α : ι → Type u_2} {f : Π (i : ι), filter (α i)} [∀ (i : ι), (f i).ne_bot] :

### n-ary coproducts of filters #

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

Coproduct of filters.

Equations
• = ⨆ (i : ι), (f i)
Instances for filter.Coprod
theorem filter.mem_Coprod_iff {ι : Type u_1} {α : ι → Type u_2} {f : Π (i : ι), filter (α i)} {s : set (Π (i : ι), α i)} :
∀ (i : ι), ∃ (t₁ : set (α i)) (H : t₁ f i), ⁻¹' t₁ s
theorem filter.compl_mem_Coprod {ι : Type u_1} {α : ι → Type u_2} {f : Π (i : ι), filter (α i)} {s : set (Π (i : ι), α i)} :
∀ (i : ι), '' s) f i
theorem filter.Coprod_ne_bot_iff' {ι : Type u_1} {α : ι → Type u_2} {f : Π (i : ι), filter (α i)} :
.ne_bot (∀ (i : ι), nonempty (α i)) ∃ (d : ι), (f d).ne_bot
@[simp]
theorem filter.Coprod_ne_bot_iff {ι : Type u_1} {α : ι → Type u_2} {f : Π (i : ι), filter (α i)} [∀ (i : ι), nonempty (α i)] :
.ne_bot ∃ (d : ι), (f d).ne_bot
theorem filter.Coprod_eq_bot_iff' {ι : Type u_1} {α : ι → Type u_2} {f : Π (i : ι), filter (α i)} :
(∃ (i : ι), is_empty (α i)) f =
@[simp]
theorem filter.Coprod_eq_bot_iff {ι : Type u_1} {α : ι → Type u_2} {f : Π (i : ι), filter (α i)} [∀ (i : ι), nonempty (α i)] :
f =
@[simp]
theorem filter.Coprod_bot' {ι : Type u_1} {α : ι → Type u_2} :
@[simp]
theorem filter.Coprod_bot {ι : Type u_1} {α : ι → Type u_2} :
filter.Coprod (λ (_x : ι), ) =
theorem filter.ne_bot.Coprod {ι : Type u_1} {α : ι → Type u_2} {f : Π (i : ι), filter (α i)} [∀ (i : ι), nonempty (α i)] {i : ι} (h : (f i).ne_bot) :
@[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] :
theorem filter.Coprod_mono {ι : Type u_1} {α : ι → Type u_2} {f₁ f₂ : Π (i : ι), filter (α i)} (hf : ∀ (i : ι), f₁ i f₂ i) :
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 (λ (i : ι), filter.map (m i) (f i))
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))