# (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 of `Filter.prod` to indexed products.

- `Filter.coprodᵢ (f : Π i, Filter (α i))`: a generalization of `Filter.coprod`; it is the supremum of `comap (eval i) (f i)`.

source
theorem Filter.tendsto_eval_pi {ι : Type u_1} {α : ι → Type u_2} (f : (i : ι) → Filter (α i)) (i : ι) :
Tendsto (Function.eval i) (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 β} :
Tendsto m l (pi f) ↔ ∀ (i : ι), Tendsto (fun (x : β) => m x i) l (f i)
source
theorem Filter.Tendsto.apply {ι : Type u_1} {α : ι → Type u_2} {f : (i : ι) → Filter (α i)} {β : Type u_3} {m : β → (i : ι) → α i} {l : Filter β} :
Tendsto m l (pi f) → ∀ (i : ι), 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.

source
theorem Filter.le_pi {ι : Type u_1} {α : ι → Type u_2} {f : (i : ι) → Filter (α i)} {g : Filter ((i : ι) → α i)} :
g ≤ pi f ↔ ∀ (i : ι), 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) :
pi f₁ ≤ 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 ∈ 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, s i ∈ f i) :
I.pi s ∈ pi f
source
theorem Filter.mem_pi {ι : Type u_1} {α : ι → Type u_2} {f : (i : ι) → Filter (α i)} {s : Set ((i : ι) → α i)} :
s ∈ 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 ∈ 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).NeBot] {I : Set ι} (h : I.pi s ∈ 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).NeBot] {I : Set ι} (hI : I.Finite) :
I.pi s ∈ pi f ↔ ∀ 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 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 pi f, ∀ (i : ι), p i (x i)
source
theorem Filter.hasBasis_pi {ι : Type u_1} {α : ι → Type u_2} {f : (i : ι) → Filter (α i)} {ι' : ι → Type u_3} {s : (i : ι) → ι' i → Set (α i)} {p : (i : ι) → ι' i → Prop} (h : ∀ (i : ι), (f i).HasBasis (p i) (s i)) :
(pi f).HasBasis (fun (If : Set ι × ((i : ι) → ι' i)) => If.1.Finite ∧ ∀ i ∈ If.1, p i (If.2 i)) fun (If : Set ι × ((i : ι) → ι' i)) => If.1.pi fun (i : ι) => s i (If.2 i)
source
theorem Filter.hasBasis_pi_same_index {ι : Type u_1} {α : ι → Type u_2} {f : (i : ι) → Filter (α i)} {κ : Type u_3} {p : κ → Prop} {s : (i : ι) → κ → Set (α i)} (h : ∀ (i : ι), (f i).HasBasis p (s i)) (h_dir : ∀ (I : Set ι) (k : ι → κ), I.Finite → (∀ i ∈ I, p (k i)) → ∃ (k₀ : κ), p k₀ ∧ ∀ i ∈ I, s i k₀ ⊆ s i (k i)) :
(pi f).HasBasis (fun (Ik : Set ι × κ) => Ik.1.Finite ∧ p Ik.2) fun (Ik : Set ι × κ) => Ik.1.pi fun (i : ι) => s i Ik.2
source
theorem Filter.HasBasis.pi_self {ι : Type u_1} {α : Type u_3} {κ : Type u_4} {f : Filter α} {p : κ → Prop} {s : κ → Set α} (h : f.HasBasis p s) :
(pi fun (x : ι) => f).HasBasis (fun (Ik : Set ι × κ) => Ik.1.Finite ∧ p Ik.2) fun (Ik : Set ι × κ) => Ik.1.pi fun (x : ι) => s Ik.2
source
theorem Filter.le_pi_principal {ι : Type u_1} {α : ι → Type u_2} (s : (i : ι) → Set (α i)) :
principal (Set.univ.pi s) ≤ pi fun (i : ι) => principal (s i)
source
@[simp]
theorem Filter.pi_principal {ι : Type u_1} {α : ι → Type u_2} [Finite ι] (s : (i : ι) → Set (α i)) :
(pi fun (i : ι) => principal (s i)) = principal (Set.univ.pi s)

The indexed product of finitely many principal filters is the principal filter corresponding to the cylinder `Set.univ.pi s`.

If the index type is infinite, then `mem_pi_principal` and `hasBasis_pi_principal` may be useful.

source
theorem Filter.mem_pi_principal {ι : Type u_1} {α : ι → Type u_2} {s : (i : ι) → Set (α i)} {t : Set ((i : ι) → α i)} :
(t ∈ pi fun (i : ι) => principal (s i)) ↔ ∃ (I : Set ι), I.Finite ∧ I.pi s ⊆ t

The indexed product of a (possibly, infinite) family of principal filters is generated by the finite `Set.pi` cylinders.

If the index type is finite, then the indexed product of principal filters is a principal filter, see `pi_principal`.

source
theorem Filter.hasBasis_pi_principal {ι : Type u_1} {α : ι → Type u_2} (s : (i : ι) → Set (α i)) :
(pi fun (i : ι) => principal (s i)).HasBasis Set.Finite fun (x : Set ι) => x.pi s

The indexed product of a (possibly, infinite) family of principal filters is generated by the finite `Set.pi` cylinders.

If the index type is finite, then the indexed product of principal filters is a principal filter, see `pi_principal`.

source
@[simp]
theorem Filter.pi_pure {ι : Type u_1} {α : ι → Type u_2} [Finite ι] (f : (i : ι) → α i) :
(pi fun (x : ι) => pure (f x)) = pure f

The indexed product of finitely many pure filters `pure (f i)` is the pure filter `pure f`.

If the index type is infinite, then `mem_pi_pure` and `hasBasis_pi_pure` below may be useful.

source
theorem Filter.mem_pi_pure {ι : Type u_1} {α : ι → Type u_2} {f : (i : ι) → α i} {s : Set ((i : ι) → α i)} :
(s ∈ pi fun (i : ι) => pure (f i)) ↔ ∃ (I : Set ι), I.Finite ∧ ∀ (g : (i : ι) → α i), (∀ i ∈ I, g i = f i) → g ∈ s

The indexed product of a (possibly, infinite) family of pure filters `pure (f i)` is generated by the sets of functions that are equal to `f` on a finite set.

If the index type is finite, then the indexed product of pure filters is a pure filter, see `pi_pure`.

source
theorem Filter.hasBasis_pi_pure {ι : Type u_1} {α : ι → Type u_2} (f : (i : ι) → α i) :
(pi fun (i : ι) => pure (f i)).HasBasis Set.Finite fun (I : Set ι) => {g : (i : ι) → α i | ∀ i ∈ I, g i = f i}

The indexed product of a (possibly, infinite) family of pure filters `pure (f i)` is generated by the sets of functions that are equal to `f` on a finite set.

If the index type is finite, then the indexed product of pure filters is a pure filter, see `pi_pure`.

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)} :
pi f ⊓ principal (Set.univ.pi s) = ⊥ ↔ ∃ (i : ι), f i ⊓ 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).NeBot] {I : Set ι} :
pi f ⊓ principal (I.pi s) = ⊥ ↔ ∃ i ∈ I, f i ⊓ principal (s i) = ⊥
source
@[simp]
theorem Filter.pi_inf_principal_univ_pi_neBot {ι : Type u_1} {α : ι → Type u_2} {f : (i : ι) → Filter (α i)} {s : (i : ι) → Set (α i)} :
(pi f ⊓ principal (Set.univ.pi s)).NeBot ↔ ∀ (i : ι), (f i ⊓ principal (s i)).NeBot
source
@[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 ι} :
(pi f ⊓ principal (I.pi s)).NeBot ↔ ∀ i ∈ I, (f i ⊓ principal (s i)).NeBot
source
instance Filter.PiInfPrincipalPi.neBot {ι : Type u_1} {α : ι → Type u_2} {f : (i : ι) → Filter (α i)} {s : (i : ι) → Set (α i)} [h : ∀ (i : ι), (f i ⊓ principal (s i)).NeBot] {I : Set ι} :
(pi f ⊓ principal (I.pi s)).NeBot
source
@[simp]
theorem Filter.pi_eq_bot {ι : Type u_1} {α : ι → Type u_2} {f : (i : ι) → Filter (α i)} :
pi f = ⊥ ↔ ∃ (i : ι), f i = ⊥
source
@[simp]
theorem Filter.pi_neBot {ι : Type u_1} {α : ι → Type u_2} {f : (i : ι) → Filter (α i)} :
(pi f).NeBot ↔ ∀ (i : ι), (f i).NeBot
source
instance Filter.instNeBotForallPi {ι : Type u_1} {α : ι → Type u_2} {f : (i : ι) → Filter (α i)} [∀ (i : ι), (f i).NeBot] :
(pi f).NeBot
source
@[simp]
theorem Filter.map_eval_pi {ι : Type u_1} {α : ι → Type u_2} (f : (i : ι) → Filter (α i)) [∀ (i : ι), (f i).NeBot] (i : ι) :
map (Function.eval i) (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).NeBot] :
pi f₁ ≤ 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).NeBot] :
pi f₁ = pi f₂ ↔ f₁ = f₂
source
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 : ι), Tendsto (f i) (l i) (l' i)) :
Tendsto (Pi.map f) (pi l) (pi l')
source
theorem Filter.pi_comap {ι : Type u_1} {α : ι → Type u_2} {β : ι → Type u_3} {f : (i : ι) → α i → β i} {l : (i : ι) → Filter (β i)} :
(pi fun (i : ι) => comap (f i) (l i)) = comap (Pi.map f) (pi l)

### `n`-ary coproducts of filters #

source
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

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₁ ∈ 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ᵢ_neBot_iff' {ι : Type u_1} {α : ι → Type u_2} {f : (i : ι) → Filter (α i)} :
(Filter.coprodᵢ f).NeBot ↔ (∀ (i : ι), Nonempty (α i)) ∧ ∃ (d : ι), (f d).NeBot
source
@[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
source
theorem Filter.coprodᵢ_eq_bot_iff' {ι : Type u_1} {α : ι → Type u_2} {f : (i : ι) → Filter (α i)} :
Filter.coprodᵢ f = ⊥ ↔ (∃ (i : ι), IsEmpty (α 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ᵢ fun (x : ι) => ⊥) = ⊥
source
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
source
instance 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
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} :
map (fun (k : (i : ι) → α i) (i : ι) => m i (k i)) (Filter.coprodᵢ f) ≤ Filter.coprodᵢ fun (i : ι) => 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 : ι), Tendsto (m i) (f i) (g i)) :
Tendsto (fun (k : (i : ι) → α i) (i : ι) => m i (k i)) (Filter.coprodᵢ f) (Filter.coprodᵢ g)