mathlib documentation

order.filter.countable_Inter

Filters with countable intersection property

In this file we define countable_Inter_filter to be the class of filters with the following property: for any countable collection of sets s ∈ l their intersection belongs to l as well.

Two main examples are the residual filter defined in topology.metric_space.baire and the measure.ae filter defined in measure_theory.measure_space.

@[class]
structure countable_Inter_filter {α : Type u_2} (l : filter α) :
Prop

A filter l has the countable intersection property if for any countable collection of sets s ∈ l their intersection belongs to l as well.

Instances
theorem countable_sInter_mem_sets {α : Type u_2} {l : filter α} [countable_Inter_filter l] {S : set (set α)} (hSc : S.countable) :
⋂₀S l ∀ (s : set α), s Ss l

theorem countable_Inter_mem_sets {ι : Type u_1} {α : Type u_2} {l : filter α} [countable_Inter_filter l] [encodable ι] {s : ι → set α} :
(⋂ (i : ι), s i) l ∀ (i : ι), s i l

theorem countable_bInter_mem_sets {ι : Type u_1} {α : Type u_2} {l : filter α} [countable_Inter_filter l] {S : set ι} (hS : S.countable) {s : Π (i : ι), i Sset α} :
(⋂ (i : ι) (H : i S), s i H) l ∀ (i : ι) (H : i S), s i H l

theorem eventually_countable_forall {ι : Type u_1} {α : Type u_2} {l : filter α} [countable_Inter_filter l] [encodable ι] {p : α → ι → Prop} :
(∀ᶠ (x : α) in l, ∀ (i : ι), p x i) ∀ (i : ι), ∀ᶠ (x : α) in l, p x i

theorem eventually_countable_ball {ι : Type u_1} {α : Type u_2} {l : filter α} [countable_Inter_filter l] {S : set ι} (hS : S.countable) {p : α → Π (i : ι), i S → Prop} :
(∀ᶠ (x : α) in l, ∀ (i : ι) (H : i S), p x i H) ∀ (i : ι) (H : i S), ∀ᶠ (x : α) in l, p x i H

theorem eventually_le.countable_Union {ι : Type u_1} {α : Type u_2} {l : filter α} [countable_Inter_filter l] [encodable ι] {s t : ι → set α} (h : ∀ (i : ι), s i ≤ᶠ[l] t i) :
(⋃ (i : ι), s i) ≤ᶠ[l] ⋃ (i : ι), t i

theorem eventually_eq.countable_Union {ι : Type u_1} {α : Type u_2} {l : filter α} [countable_Inter_filter l] [encodable ι] {s t : ι → set α} (h : ∀ (i : ι), s i =ᶠ[l] t i) :
(⋃ (i : ι), s i) =ᶠ[l] ⋃ (i : ι), t i

theorem eventually_le.countable_bUnion {ι : Type u_1} {α : Type u_2} {l : filter α} [countable_Inter_filter l] {S : set ι} (hS : S.countable) {s t : Π (i : ι), i Sset α} (h : ∀ (i : ι) (H : i S), s i H ≤ᶠ[l] t i H) :
(⋃ (i : ι) (H : i S), s i H) ≤ᶠ[l] ⋃ (i : ι) (H : i S), t i H

theorem eventually_eq.countable_bUnion {ι : Type u_1} {α : Type u_2} {l : filter α} [countable_Inter_filter l] {S : set ι} (hS : S.countable) {s t : Π (i : ι), i Sset α} (h : ∀ (i : ι) (H : i S), s i H =ᶠ[l] t i H) :
(⋃ (i : ι) (H : i S), s i H) =ᶠ[l] ⋃ (i : ι) (H : i S), t i H

theorem eventually_le.countable_Inter {ι : Type u_1} {α : Type u_2} {l : filter α} [countable_Inter_filter l] [encodable ι] {s t : ι → set α} (h : ∀ (i : ι), s i ≤ᶠ[l] t i) :
(⋂ (i : ι), s i) ≤ᶠ[l] ⋂ (i : ι), t i

theorem eventually_eq.countable_Inter {ι : Type u_1} {α : Type u_2} {l : filter α} [countable_Inter_filter l] [encodable ι] {s t : ι → set α} (h : ∀ (i : ι), s i =ᶠ[l] t i) :
(⋂ (i : ι), s i) =ᶠ[l] ⋂ (i : ι), t i

theorem eventually_le.countable_bInter {ι : Type u_1} {α : Type u_2} {l : filter α} [countable_Inter_filter l] {S : set ι} (hS : S.countable) {s t : Π (i : ι), i Sset α} (h : ∀ (i : ι) (H : i S), s i H ≤ᶠ[l] t i H) :
(⋂ (i : ι) (H : i S), s i H) ≤ᶠ[l] ⋂ (i : ι) (H : i S), t i H

theorem eventually_eq.countable_bInter {ι : Type u_1} {α : Type u_2} {l : filter α} [countable_Inter_filter l] {S : set ι} (hS : S.countable) {s t : Π (i : ι), i Sset α} (h : ∀ (i : ι) (H : i S), s i H =ᶠ[l] t i H) :
(⋂ (i : ι) (H : i S), s i H) =ᶠ[l] ⋂ (i : ι) (H : i S), t i H

@[instance]
def countable_Inter_filter_principal {α : Type u_2} (s : set α) :

@[instance]

@[instance]

@[instance]
def countable_Inter_filter_inf {α : Type u_2} (l₁ l₂ : filter α) [countable_Inter_filter l₁] [countable_Inter_filter l₂] :

Infimum of two countable_Inter_filters is a countable_Inter_filter. This is useful, e.g., to automatically get an instance for residual α ⊓ 𝓟 s.

@[instance]
def countable_Inter_filter_sup {α : Type u_2} (l₁ l₂ : filter α) [countable_Inter_filter l₁] [countable_Inter_filter l₂] :

Supremum of two countable_Inter_filters is a countable_Inter_filter.