(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 ofFilter.prod
to indexed products.Filter.coprodᵢ (f : Π i, Filter (α i))
: a generalization ofFilter.coprod
; it is the supremum ofcomap (eval i) (f i)
.
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)
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 (fun (x : β) => m x i) l (f i)
theorem
Filter.Tendsto.apply
{ι : 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 (fun (x : β) => m x i) l (f i)
If a function tends to a product Filter.pi f
of filters, then its i
-th component tends to
f i
. See also Filter.Tendsto.apply_nhds
for the special case of converging to a point in a
product of topological spaces.
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.le_pi_principal
{ι : Type u_1}
{α : ι → Type u_2}
(s : (i : ι) → Set (α i))
:
Filter.principal (Set.univ.pi s) ≤ Filter.pi fun (i : ι) => Filter.principal (s i)
@[simp]
theorem
Filter.pi_principal
{ι : Type u_1}
{α : ι → Type u_2}
[Finite ι]
(s : (i : ι) → Set (α i))
:
(Filter.pi fun (i : ι) => Filter.principal (s i)) = Filter.principal (Set.univ.pi s)
@[simp]
theorem
Filter.pi_inf_principal_univ_pi_neBot
{ι : Type u_1}
{α : ι → Type u_2}
{f : (i : ι) → Filter (α i)}
{s : (i : ι) → Set (α i)}
:
(Filter.pi f ⊓ Filter.principal (Set.univ.pi s)).NeBot ↔ ∀ (i : ι), (f i ⊓ Filter.principal (s i)).NeBot
@[simp]
theorem
Filter.pi_inf_principal_pi_neBot
{ι : Type u_1}
{α : ι → Type u_2}
{f : (i : ι) → Filter (α i)}
{s : (i : ι) → Set (α i)}
[∀ (i : ι), (f i).NeBot]
{I : Set ι}
:
(Filter.pi f ⊓ Filter.principal (I.pi s)).NeBot ↔ ∀ i ∈ I, (f i ⊓ Filter.principal (s i)).NeBot
theorem
Filter.PiInfPrincipalPi.neBot
{ι : Type u_1}
{α : ι → Type u_2}
{f : (i : ι) → Filter (α i)}
{s : (i : ι) → Set (α i)}
[h : ∀ (i : ι), (f i ⊓ Filter.principal (s i)).NeBot]
{I : Set ι}
:
(Filter.pi f ⊓ Filter.principal (I.pi s)).NeBot
@[simp]
theorem
Filter.map_eval_pi
{ι : Type u_1}
{α : ι → Type u_2}
(f : (i : ι) → Filter (α i))
[∀ (i : ι), (f i).NeBot]
(i : ι)
:
Filter.map (Function.eval i) (Filter.pi f) = f i
theorem
Filter.tendsto_piMap_pi
{ι : Type u_1}
{α : ι → Type u_2}
{β : ι → Type u_3}
{f : (i : ι) → α i → β i}
{l : (i : ι) → Filter (α i)}
{l' : (i : ι) → Filter (β i)}
(h : ∀ (i : ι), Filter.Tendsto (f i) (l i) (l' i))
:
Filter.Tendsto (Pi.map f) (Filter.pi l) (Filter.pi l')
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
- Filter.coprodᵢ f = ⨆ (i : ι), Filter.comap (Function.eval i) (f i)
Instances For
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₁ ∈ 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_1}
{α : ι → Type u_2}
{f : (i : ι) → Filter (α i)}
:
(Filter.coprodᵢ f).NeBot ↔ (∀ (i : ι), Nonempty (α i)) ∧ ∃ (d : ι), (f d).NeBot
@[simp]
theorem
Filter.coprodᵢ_neBot_iff
{ι : Type u_1}
{α : ι → Type u_2}
{f : (i : ι) → Filter (α i)}
[∀ (i : ι), Nonempty (α i)]
:
(Filter.coprodᵢ f).NeBot ↔ ∃ (d : ι), (f d).NeBot
@[simp]
theorem
Filter.NeBot.coprodᵢ
{ι : Type u_1}
{α : ι → Type u_2}
{f : (i : ι) → Filter (α i)}
[∀ (i : ι), Nonempty (α i)]
{i : ι}
(h : (f i).NeBot)
:
(Filter.coprodᵢ f).NeBot
theorem
Filter.coprodᵢ_neBot
{ι : Type u_1}
{α : ι → Type u_2}
[∀ (i : ι), Nonempty (α i)]
[Nonempty ι]
(f : (i : ι) → Filter (α i))
[H : ∀ (i : ι), (f i).NeBot]
:
(Filter.coprodᵢ f).NeBot
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₂
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 (fun (k : (i : ι) → α i) (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_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 (fun (k : (i : ι) → α i) (i : ι) => m i (k i)) (Filter.coprodᵢ f) (Filter.coprodᵢ g)