mathlib3 documentation

order.filter.pi

(Co)product of a family of filters #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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
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 : ι) :
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 I s 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 I s i f i
theorem filter.eventually.eval_pi {ι : Type u_1} {α : ι Type u_2} {f : Π (i : ι), filter (α i)} {p : Π (i : ι), α i Prop} {i : ι} (hf : ∀ᶠ (x : α i) in f i, p i x) :
∀ᶠ (x : Π (i : ι), α i) in filter.pi f, p i (x i)
theorem filter.eventually_pi {ι : Type u_1} {α : ι Type u_2} {f : Π (i : ι), filter (α i)} {p : Π (i : ι), α i Prop} [finite ι] (hf : (i : ι), ∀ᶠ (x : α i) in f i, p i x) :
∀ᶠ (x : Π (i : ι), α i) in filter.pi f, (i : ι), p i (x i)
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)))
@[simp]
theorem filter.pi_inf_principal_univ_pi_eq_bot {ι : Type u_1} {α : ι Type u_2} {f : Π (i : ι), filter (α i)} {s : Π (i : ι), set (α 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 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)} :
@[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 ι} :
@[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)} :
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] :
@[simp]
theorem filter.map_eval_pi {ι : Type u_1} {α : ι Type u_2} (f : Π (i : ι), filter (α i)) [ (i : ι), (f i).ne_bot] (i : ι) :
@[simp]
theorem filter.pi_le_pi {ι : Type u_1} {α : ι Type u_2} {f₁ f₂ : Π (i : ι), filter (α i)} [ (i : ι), (f₁ i).ne_bot] :
filter.pi f₁ filter.pi f₂ (i : ι), f₁ i f₂ i
@[simp]
theorem filter.pi_inj {ι : Type u_1} {α : ι Type u_2} {f₁ f₂ : Π (i : ι), filter (α i)} [ (i : ι), (f₁ i).ne_bot] :
filter.pi f₁ = filter.pi f₂ f₁ = f₂

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
Instances for filter.Coprod
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 {ι : Type u_1} {α : ι Type u_2} {f : Π (i : ι), filter (α i)} {s : set (Π (i : ι), α 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.Coprod_eq_bot_iff' {ι : Type u_1} {α : ι Type u_2} {f : Π (i : ι), filter (α i)} :
filter.Coprod f = ( (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)] :
@[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 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)