Documentation

Mathlib.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_2} {α : ιType u_1} (f : (i : ι) → Filter (α i)) (i : ι) :
theorem Filter.tendsto_pi {ι : Type u_2} {α : ιType u_3} {f : (i : ι) → Filter (α i)} {β : Type u_1} {m : β(i : ι) → α i} {l : Filter β} :
Filter.Tendsto m l (Filter.pi f) ∀ (i : ι), Filter.Tendsto (fun 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_2} {α : ιType u_1} {f₁ : (i : ι) → Filter (α i)} {f₂ : (i : ι) → Filter (α i)} (h : ∀ (i : ι), f₁ i f₂ i) :
theorem Filter.mem_pi_of_mem {ι : Type u_2} {α : ιType u_1} {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 : Set.Finite I) (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.Finite I t, (∀ (i : ι), t i f i) Set.pi I 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 t, (∀ (i : ι), t i f i) Set.pi (I) t s
theorem Filter.mem_of_pi_mem_pi {ι : Type u_2} {α : ιType u_1} {f : (i : ι) → Filter (α i)} {s : (i : ι) → Set (α i)} [inst : ∀ (i : ι), Filter.NeBot (f i)] {I : Set ι} (h : Set.pi I s Filter.pi f) {i : ι} (hi : i I) :
s i f i
@[simp]
theorem Filter.pi_mem_pi_iff {ι : Type u_2} {α : ιType u_1} {f : (i : ι) → Filter (α i)} {s : (i : ι) → Set (α i)} [inst : ∀ (i : ι), Filter.NeBot (f i)] {I : Set ι} (hI : Set.Finite I) :
Set.pi I s Filter.pi f ∀ (i : ι), i Is i f i
theorem Filter.hasBasis_pi {ι : Type u_2} {α : ιType u_1} {f : (i : ι) → Filter (α i)} {ι' : ιType} {s : (i : ι) → ι' iSet (α i)} {p : (i : ι) → ι' iProp} (h : ∀ (i : ι), Filter.HasBasis (f i) (p i) (s i)) :
Filter.HasBasis (Filter.pi f) (fun If => Set.Finite If.fst ((i : ι) → i If.fstp i (Prod.snd (Set ι) ((i : ι) → ι' i) If i))) fun If => Set.pi If.fst fun i => s i (Prod.snd (Set ι) ((i : ι) → ι' i) If 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_2} {α : ιType u_1} {f : (i : ι) → Filter (α i)} {s : (i : ι) → Set (α i)} [inst : ∀ (i : ι), Filter.NeBot (f i)] {I : Set ι} :
@[simp]
theorem Filter.pi_inf_principal_univ_pi_neBot {ι : Type u_2} {α : ιType u_1} {f : (i : ι) → Filter (α i)} {s : (i : ι) → Set (α i)} :
@[simp]
theorem Filter.pi_inf_principal_pi_neBot {ι : Type u_2} {α : ιType u_1} {f : (i : ι) → Filter (α i)} {s : (i : ι) → Set (α i)} [inst : ∀ (i : ι), Filter.NeBot (f i)] {I : Set ι} :
instance Filter.PiInfPrincipalPi.neBot {ι : Type u_1} {α : ιType u_2} {f : (i : ι) → Filter (α i)} {s : (i : ι) → Set (α i)} [h : ∀ (i : ι), Filter.NeBot (f i Filter.principal (s i))] {I : Set ι} :
Equations
@[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_neBot {ι : Type u_2} {α : ιType u_1} {f : (i : ι) → Filter (α i)} :
Filter.NeBot (Filter.pi f) ∀ (i : ι), Filter.NeBot (f i)
instance Filter.instNeBotForAllPi {ι : Type u_1} {α : ιType u_2} {f : (i : ι) → Filter (α i)} [inst : ∀ (i : ι), Filter.NeBot (f i)] :
Equations
@[simp]
theorem Filter.map_eval_pi {ι : Type u_2} {α : ιType u_1} (f : (i : ι) → Filter (α i)) [inst : ∀ (i : ι), Filter.NeBot (f i)] (i : ι) :
@[simp]
theorem Filter.pi_le_pi {ι : Type u_2} {α : ιType u_1} {f₁ : (i : ι) → Filter (α i)} {f₂ : (i : ι) → Filter (α i)} [inst : ∀ (i : ι), Filter.NeBot (f₁ i)] :
Filter.pi f₁ Filter.pi f₂ ∀ (i : ι), f₁ i f₂ i
@[simp]
theorem Filter.pi_inj {ι : Type u_2} {α : ιType u_1} {f₁ : (i : ι) → Filter (α i)} {f₂ : (i : ι) → Filter (α i)} [inst : ∀ (i : ι), Filter.NeBot (f₁ i)] :
Filter.pi f₁ = Filter.pi f₂ f₁ = f₂

n-ary coproducts of filters #

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₁, 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)} :
s Filter.coprodᵢ f ∀ (i : ι), (Function.eval i '' s) f i
theorem Filter.coprodᵢ_neBot_iff' {ι : Type u_2} {α : ιType u_1} {f : (i : ι) → Filter (α i)} :
Filter.NeBot (Filter.coprodᵢ f) (∀ (i : ι), Nonempty (α i)) d, Filter.NeBot (f d)
@[simp]
theorem Filter.coprodᵢ_neBot_iff {ι : Type u_2} {α : ιType u_1} {f : (i : ι) → Filter (α i)} [inst : ∀ (i : ι), Nonempty (α i)] :
theorem Filter.coprodᵢ_eq_bot_iff' {ι : Type u_1} {α : ιType u_2} {f : (i : ι) → Filter (α i)} :
Filter.coprodᵢ f = (i, IsEmpty (α i)) f =
@[simp]
theorem Filter.coprodᵢ_eq_bot_iff {ι : Type u_2} {α : ιType u_1} {f : (i : ι) → Filter (α i)} [inst : ∀ (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} :
theorem Filter.NeBot.coprodᵢ {ι : Type u_2} {α : ιType u_1} {f : (i : ι) → Filter (α i)} [inst : ∀ (i : ι), Nonempty (α i)] {i : ι} (h : Filter.NeBot (f i)) :
theorem Filter.coprodᵢ_neBot {ι : Type u_2} {α : ιType u_1} [inst : ∀ (i : ι), Nonempty (α i)] [inst : Nonempty ι] (f : (i : ι) → Filter (α i)) [H : ∀ (i : ι), Filter.NeBot (f i)] :
theorem Filter.coprodᵢ_mono {ι : Type u_2} {α : ιType u_1} {f₁ : (i : ι) → Filter (α i)} {f₂ : (i : ι) → Filter (α i)} (hf : ∀ (i : ι), f₁ i f₂ i) :
theorem Filter.map_pi_map_coprodᵢ_le {ι : Type u_1} {α : ιType u_3} {f : (i : ι) → Filter (α i)} {β : ιType u_2} {m : (i : ι) → α iβ i} :
Filter.map (fun k i => m i (k i)) (Filter.coprodᵢ f) Filter.coprodᵢ fun i => Filter.map (m i) (f i)
theorem Filter.Tendsto.pi_map_coprodᵢ {ι : Type u_3} {α : ιType u_2} {f : (i : ι) → Filter (α i)} {β : ιType u_1} {m : (i : ι) → α iβ i} {g : (i : ι) → Filter (β i)} (h : ∀ (i : ι), Filter.Tendsto (m i) (f i) (g i)) :
Filter.Tendsto (fun k i => m i (k i)) (Filter.coprodᵢ f) (Filter.coprodᵢ g)