mathlib documentation

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.

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
theorem filter.tendsto_eval_pi {ι : Type u_1} {α : ι → Type u_2} (f : Π (i : ι), filter (α i)) (i : ι) :
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)
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)
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) :
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
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
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
@[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 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)} :
filter.pi f 𝓟 (set.univ.pi s) = ∃ (i : ι), f i 𝓟 (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.pi f 𝓟 (I.pi s) = ∃ (i : ι) (H : i I), f i 𝓟 (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)} :
(filter.pi f 𝓟 (set.univ.pi s)).ne_bot ∀ (i : ι), (f i 𝓟 (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.pi f 𝓟 (I.pi s)).ne_bot ∀ (i : ι), i I(f i 𝓟 (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 𝓟 (s i)).ne_bot] {I : set ι} :
@[simp]
theorem filter.pi_eq_bot {ι : Type u_1} {α : ι → Type u_2} {f : Π (i : ι), filter (α i)} :
filter.pi f = ∃ (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
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
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)
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
@[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
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 f) 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)) (filter.Coprod f) (filter.Coprod g)