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
Instances For
    instance Filter.pi.isCountablyGenerated {ι : Type u_1} {α : ιType u_2} {f : (i : ι) → Filter (α i)} [Countable ι] [∀ (i : ι), (f i).IsCountablyGenerated] :
    (Filter.pi f).IsCountablyGenerated
    Equations
    • =
    theorem Filter.tendsto_eval_pi {ι : Type u_1} {α : ιType u_2} (f : (i : ι) → Filter (α i)) (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.pi_mono {ι : Type u_1} {α : ιType u_2} {f₁ : (i : ι) → Filter (α i)} {f₂ : (i : ι) → Filter (α i)} (h : ∀ (i : ι), f₁ i f₂ i) :
    theorem Filter.mem_pi_of_mem {ι : Type u_1} {α : ιType u_2} {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 : I.Finite) (h : iI, s i f i) :
    I.pi 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 ι), I.Finite ∃ (t : (i : ι) → Set (α i)), (∀ (i : ι), t i f i) I.pi 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 : Finset ι) (t : (i : ι) → Set (α i)), (∀ (i : ι), t i f i) (↑I).pi t s
    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 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 : ι), (f i).NeBot] {I : Set ι} (hI : I.Finite) :
    I.pi s Filter.pi f iI, s i f i
    theorem Filter.Eventually.eval_pi {ι : Type u_1} {α : ιType u_2} {f : (i : ι) → Filter (α i)} {p : (i : ι) → α iProp} {i : ι} (hf : ∀ᶠ (x : α i) in f i, p i x) :
    ∀ᶠ (x : (i : ι) → α i) in Filter.pi f, p i (x i)
    theorem Filter.eventually_pi {ι : Type u_1} {α : ιType u_2} {f : (i : ι) → Filter (α i)} {p : (i : ι) → α iProp} [Finite ι] (hf : ∀ (i : ι), ∀ᶠ (x : α i) in f i, p i x) :
    ∀ᶠ (x : (i : ι) → α i) in Filter.pi f, ∀ (i : ι), p i (x i)
    theorem Filter.hasBasis_pi {ι : Type u_1} {α : ιType u_2} {f : (i : ι) → Filter (α i)} {ι' : ιType u_3} {s : (i : ι) → ι' iSet (α i)} {p : (i : ι) → ι' iProp} (h : ∀ (i : ι), (f i).HasBasis (p i) (s i)) :
    (Filter.pi f).HasBasis (fun (If : Set ι × ((i : ι) → ι' i)) => If.1.Finite iIf.1, p i (If.2 i)) fun (If : Set ι × ((i : ι) → ι' i)) => If.1.pi fun (i : ι) => s i (If.2 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_pure {ι : Type u_1} {α : ιType u_2} [Finite ι] (f : (i : ι) → α i) :
    (Filter.pi fun (x : ι) => pure (f x)) = pure f
    @[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) =
    @[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 ι} :
    Filter.pi f Filter.principal (I.pi s) = iI, 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.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 iI, (f i Filter.principal (s i)).NeBot
    instance 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
    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_1} {α : ιType u_2} {f : (i : ι) → Filter (α i)} :
    (Filter.pi f).NeBot ∀ (i : ι), (f i).NeBot
    instance Filter.instNeBotForallPi {ι : Type u_1} {α : ιType u_2} {f : (i : ι) → Filter (α i)} [∀ (i : ι), (f i).NeBot] :
    (Filter.pi f).NeBot
    Equations
    • =
    @[simp]
    theorem Filter.map_eval_pi {ι : Type u_1} {α : ιType u_2} (f : (i : ι) → Filter (α i)) [∀ (i : ι), (f i).NeBot] (i : ι) :
    @[simp]
    theorem Filter.pi_le_pi {ι : Type u_1} {α : ιType u_2} {f₁ : (i : ι) → Filter (α i)} {f₂ : (i : ι) → Filter (α i)} [∀ (i : ι), (f₁ i).NeBot] :
    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 : ι), (f₁ i).NeBot] :
    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
    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
      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)] :
      @[simp]
      theorem Filter.coprodᵢ_bot' {ι : Type u_1} {α : ιType u_2} :
      @[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 : (f i).NeBot) :
      theorem Filter.coprodᵢ_neBot {ι : Type u_1} {α : ιType u_2} [∀ (i : ι), Nonempty (α i)] [Nonempty ι] (f : (i : ι) → Filter (α i)) [H : ∀ (i : ι), (f i).NeBot] :
      theorem Filter.coprodᵢ_mono {ι : Type u_1} {α : ιType u_2} {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_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)