(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).

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

• Filter.pi f = ⨅ (i : ι), Filter.comap (Function.eval i) (f i)

instance Filter.pi.isCountablyGenerated {ι : Type u_1} {α : ι → Type u_2} {f : (i : ι) → Filter (α i)} [Countable ι] [∀ (i : ι), Filter.IsCountablyGenerated (f i)] : Filter.IsCountablyGenerated (Filter.pi f)

Equations

• @Filter.pi.isCountablyGenerated = @Filter.pi.isCountablyGenerated.proof_1

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.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₁ : (i : ι) → Filter (α i)} {f₂ : (i : ι) → Filter (α i)} (h : ∀ (i : ι), f₁ i ≤ f₂ i) : Filter.pi f₁ ≤ Filter.pi f₂

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

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 ∈ I → s i ∈ f i) : Set.pi I s ∈ Filter.pi f

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_1} {α : ι → Type u_2} {f : (i : ι) → Filter (α i)} {s : (i : ι) → Set (α i)} [∀ (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_1} {α : ι → Type u_2} {f : (i : ι) → Filter (α i)} {s : (i : ι) → Set (α i)} [∀ (i : ι), Filter.NeBot (f i)] {I : Set ι} (hI : Set.Finite I) : Set.pi I s ∈ Filter.pi f ↔ ∀ (i : ι), i ∈ I → s i ∈ f i

theorem Filter.hasBasis_pi {ι : Type u_1} {α : ι → Type u_2} {f : (i : ι) → Filter (α i)} {ι' : ι → Type} {s : (i : ι) → ι' i → Set (α i)} {p : (i : ι) → ι' i → Prop} (h : ∀ (i : ι), Filter.HasBasis (f i) (p i) (s i)) : Filter.HasBasis (Filter.pi f) (fun If => Set.Finite If.fst ∧ ((i : ι) → i ∈ If.fst → p 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)} : Filter.pi f ⊓ Filter.principal (Set.pi Set.univ s) = ⊥ ↔ ∃ i, f i ⊓ Filter.principal (s 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 : ι), Filter.NeBot (f i)] {I : Set ι} : Filter.pi f ⊓ Filter.principal (Set.pi I s) = ⊥ ↔ ∃ i, i ∈ I ∧ f i ⊓ Filter.principal (s i) = ⊥

@[simp]

theorem Filter.pi_inf_principal_univ_pi_neBot {ι : Type u_1} {α : ι → Type u_2} {f : (i : ι) → Filter (α i)} {s : (i : ι) → Set (α i)} : Filter.NeBot (Filter.pi f ⊓ Filter.principal (Set.pi Set.univ s)) ↔ ∀ (i : ι), Filter.NeBot (f i ⊓ Filter.principal (s i))

@[simp]

theorem Filter.pi_inf_principal_pi_neBot {ι : Type u_1} {α : ι → Type u_2} {f : (i : ι) → Filter (α i)} {s : (i : ι) → Set (α i)} [∀ (i : ι), Filter.NeBot (f i)] {I : Set ι} : Filter.NeBot (Filter.pi f ⊓ Filter.principal (Set.pi I s)) ↔ ∀ (i : ι), i ∈ I → Filter.NeBot (f i ⊓ Filter.principal (s i))

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 ι} : Filter.NeBot (Filter.pi f ⊓ Filter.principal (Set.pi I s))

Equations

• @Filter.PiInfPrincipalPi.neBot = @Filter.PiInfPrincipalPi.neBot.proof_1

@[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_1} {α : ι → Type u_2} {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)} [∀ (i : ι), Filter.NeBot (f i)] : Filter.NeBot (Filter.pi f)

Equations

• @Filter.instNeBotForAllPi = @Filter.instNeBotForAllPi.proof_1

@[simp]

theorem Filter.map_eval_pi {ι : Type u_1} {α : ι → Type u_2} (f : (i : ι) → Filter (α i)) [∀ (i : ι), Filter.NeBot (f i)] (i : ι) : Filter.map (Function.eval i) (Filter.pi f) = f i

@[simp]

theorem Filter.pi_le_pi {ι : Type u_1} {α : ι → Type u_2} {f₁ : (i : ι) → Filter (α i)} {f₂ : (i : ι) → Filter (α i)} [∀ (i : ι), Filter.NeBot (f₁ i)] : Filter.pi f₁ ≤ Filter.pi f₂ ↔ ∀ (i : ι), f₁ i ≤ f₂ i

@[simp]

theorem Filter.pi_inj {ι : Type u_1} {α : ι → Type u_2} {f₁ : (i : ι) → Filter (α i)} {f₂ : (i : ι) → Filter (α i)} [∀ (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

• Filter.coprodᵢ f = ⨆ (i : ι), Filter.comap (Function.eval i) (f i)

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_1} {α : ι → Type u_2} {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_1} {α : ι → Type u_2} {f : (i : ι) → Filter (α i)} [∀ (i : ι), Nonempty (α i)] : Filter.NeBot (Filter.coprodᵢ f) ↔ ∃ d, Filter.NeBot (f d)

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_1} {α : ι → Type u_2} {f : (i : ι) → Filter (α i)} [∀ (i : ι), Nonempty (α i)] : Filter.coprodᵢ f = ⊥ ↔ f = ⊥

@[simp]

theorem Filter.coprodᵢ_bot' {ι : Type u_1} {α : ι → Type u_2} : Filter.coprodᵢ ⊥ = ⊥

@[simp]

theorem Filter.coprodᵢ_bot {ι : Type u_1} {α : ι → Type u_2} : (Filter.coprodᵢ fun x => ⊥) = ⊥

theorem Filter.NeBot.coprodᵢ {ι : Type u_1} {α : ι → Type u_2} {f : (i : ι) → Filter (α i)} [∀ (i : ι), Nonempty (α i)] {i : ι} (h : Filter.NeBot (f i)) : Filter.NeBot (Filter.coprodᵢ f)

theorem Filter.coprodᵢ_neBot {ι : Type u_1} {α : ι → Type u_2} [∀ (i : ι), Nonempty (α i)] [Nonempty ι] (f : (i : ι) → Filter (α i)) [H : ∀ (i : ι), Filter.NeBot (f i)] : Filter.NeBot (Filter.coprodᵢ f)

theorem Filter.coprodᵢ_mono {ι : Type u_1} {α : ι → Type u_2} {f₁ : (i : ι) → Filter (α i)} {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 => 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 => m i (k i)) (Filter.coprodᵢ f) (Filter.coprodᵢ g)