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.

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
Instances for filter.pi
source
@[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] :
(filter.pi f).is_countably_generated
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.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)
source
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)
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 ⊓ filter.principal (set.univ.pi s) = ⊥ ↔ ∃ (i : ι), f i ⊓ filter.principal (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 ⊓ filter.principal (I.pi s) = ⊥ ↔ ∃ (i : ι) (H : i ∈ I), f i ⊓ filter.principal (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 ⊓ filter.principal (set.univ.pi s)).ne_bot ↔ ∀ (i : ι), (f i ⊓ filter.principal (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 ⊓ filter.principal (I.pi s)).ne_bot ↔ ∀ (i : ι), i ∈ I → (f i ⊓ filter.principal (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 ⊓ filter.principal (s i)).ne_bot] {I : set ι} :
(filter.pi f ⊓ filter.principal (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
source
@[simp]
theorem filter.map_eval_pi {ι : Type u_1} {α : ι → Type u_2} (f : Π (i : ι), filter (α i)) [∀ (i : ι), (f i).ne_bot] (i : ι) :
filter.map (function.eval i) (filter.pi f) = f i
source
@[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
source
@[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 #

source
@[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
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 {ι : Type u_1} {α : ι → Type u_2} {f : Π (i : ι), filter (α i)} {s : set (Π (i : ι), α i)} :
sᶜ ∈ filter.Coprod f ↔ ∀ (i : ι), (function.eval i '' s)ᶜ ∈ f 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.Coprod_eq_bot_iff' {ι : Type u_1} {α : ι → Type u_2} {f : Π (i : ι), filter (α i)} :
filter.Coprod f = ⊥ ↔ (∃ (i : ι), is_empty (α i)) ∨ f = ⊥
source
@[simp]
theorem filter.Coprod_eq_bot_iff {ι : Type u_1} {α : ι → Type u_2} {f : Π (i : ι), filter (α i)} [∀ (i : ι), nonempty (α i)] :
filter.Coprod f = ⊥ ↔ f = ⊥
source
@[simp]
theorem filter.Coprod_bot' {ι : Type u_1} {α : ι → Type u_2} :
filter.Coprod ⊥ = ⊥
source
@[simp]
theorem filter.Coprod_bot {ι : Type u_1} {α : ι → Type u_2} :
filter.Coprod (λ (_x : ι), ⊥) = ⊥
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)