Documentation

Mathlib.Order.Filter.CountableInter

Filters with countable intersection property #

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

Two main examples are the residual filter defined in Mathlib.Topology.MetricSpace.Baire and the measure.ae filter defined in measure_theory.measure_space.

We reformulate the definition in terms of indexed intersection and in terms of filter.eventually and provide instances for some basic constructions (⊥⊥, ⊤⊤, Filter.principal, Filter.map, Filter.comap, Inf.inf). We also provide a custom constructor Filter.ofCountableInter that deduces two axioms of a Filter from the countable intersection property.

Tags #

filter, countable

class CountableInterFilter {α : Type u_1} (l : Filter α) :
  • For a countable collection of sets s ∈ l∈ l, their intersection belongs to l as well.

    countable_interₛ_mem : ∀ (S : Set (Set α)), Set.Countable S(∀ (s : Set α), s Ss l) → ⋂₀ S l

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

Instances
    theorem countable_interₛ_mem {α : Type u_1} {l : Filter α} [inst : CountableInterFilter l] {S : Set (Set α)} (hSc : Set.Countable S) :
    ⋂₀ S l ∀ (s : Set α), s Ss l
    theorem countable_interᵢ_mem {ι : Sort u_1} {α : Type u_2} {l : Filter α} [inst : CountableInterFilter l] [inst : Countable ι] {s : ιSet α} :
    (Set.interᵢ fun i => s i) l ∀ (i : ι), s i l
    theorem countable_bInter_mem {α : Type u_2} {l : Filter α} [inst : CountableInterFilter l] {ι : Type u_1} {S : Set ι} (hS : Set.Countable S) {s : (i : ι) → i SSet α} :
    (Set.interᵢ fun i => Set.interᵢ fun hi => s i hi) l ∀ (i : ι) (hi : i S), s i hi l
    theorem eventually_countable_forall {ι : Sort u_1} {α : Type u_2} {l : Filter α} [inst : CountableInterFilter l] [inst : Countable ι] {p : αιProp} :
    Filter.Eventually (fun x => (i : ι) → p x i) l ∀ (i : ι), Filter.Eventually (fun x => p x i) l
    theorem eventually_countable_ball {α : Type u_2} {l : Filter α} [inst : CountableInterFilter l] {ι : Type u_1} {S : Set ι} (hS : Set.Countable S) {p : α(i : ι) → i SProp} :
    Filter.Eventually (fun x => (i : ι) → (hi : i S) → p x i hi) l ∀ (i : ι) (hi : i S), Filter.Eventually (fun x => p x i hi) l
    theorem EventuallyLE.countable_unionᵢ {ι : Sort u_1} {α : Type u_2} {l : Filter α} [inst : CountableInterFilter l] [inst : Countable ι] {s : ιSet α} {t : ιSet α} (h : ∀ (i : ι), s i ≤ᶠ[l] t i) :
    (Set.unionᵢ fun i => s i) ≤ᶠ[l] Set.unionᵢ fun i => t i
    theorem EventuallyEq.countable_unionᵢ {ι : Sort u_1} {α : Type u_2} {l : Filter α} [inst : CountableInterFilter l] [inst : Countable ι] {s : ιSet α} {t : ιSet α} (h : ∀ (i : ι), s i =ᶠ[l] t i) :
    (Set.unionᵢ fun i => s i) =ᶠ[l] Set.unionᵢ fun i => t i
    theorem EventuallyLE.countable_bUnion {α : Type u_2} {l : Filter α} [inst : CountableInterFilter l] {ι : Type u_1} {S : Set ι} (hS : Set.Countable S) {s : (i : ι) → i SSet α} {t : (i : ι) → i SSet α} (h : ∀ (i : ι) (hi : i S), s i hi ≤ᶠ[l] t i hi) :
    (Set.unionᵢ fun i => Set.unionᵢ fun h => s i h) ≤ᶠ[l] Set.unionᵢ fun i => Set.unionᵢ fun h => t i h
    theorem EventuallyEq.countable_bUnion {α : Type u_2} {l : Filter α} [inst : CountableInterFilter l] {ι : Type u_1} {S : Set ι} (hS : Set.Countable S) {s : (i : ι) → i SSet α} {t : (i : ι) → i SSet α} (h : ∀ (i : ι) (hi : i S), s i hi =ᶠ[l] t i hi) :
    (Set.unionᵢ fun i => Set.unionᵢ fun h => s i h) =ᶠ[l] Set.unionᵢ fun i => Set.unionᵢ fun h => t i h
    theorem EventuallyLE.countable_interᵢ {ι : Sort u_1} {α : Type u_2} {l : Filter α} [inst : CountableInterFilter l] [inst : Countable ι] {s : ιSet α} {t : ιSet α} (h : ∀ (i : ι), s i ≤ᶠ[l] t i) :
    (Set.interᵢ fun i => s i) ≤ᶠ[l] Set.interᵢ fun i => t i
    theorem EventuallyEq.countable_interᵢ {ι : Sort u_1} {α : Type u_2} {l : Filter α} [inst : CountableInterFilter l] [inst : Countable ι] {s : ιSet α} {t : ιSet α} (h : ∀ (i : ι), s i =ᶠ[l] t i) :
    (Set.interᵢ fun i => s i) =ᶠ[l] Set.interᵢ fun i => t i
    theorem EventuallyLE.countable_bInter {α : Type u_2} {l : Filter α} [inst : CountableInterFilter l] {ι : Type u_1} {S : Set ι} (hS : Set.Countable S) {s : (i : ι) → i SSet α} {t : (i : ι) → i SSet α} (h : ∀ (i : ι) (hi : i S), s i hi ≤ᶠ[l] t i hi) :
    (Set.interᵢ fun i => Set.interᵢ fun h => s i h) ≤ᶠ[l] Set.interᵢ fun i => Set.interᵢ fun h => t i h
    theorem EventuallyEq.countable_bInter {α : Type u_2} {l : Filter α} [inst : CountableInterFilter l] {ι : Type u_1} {S : Set ι} (hS : Set.Countable S) {s : (i : ι) → i SSet α} {t : (i : ι) → i SSet α} (h : ∀ (i : ι) (hi : i S), s i hi =ᶠ[l] t i hi) :
    (Set.interᵢ fun i => Set.interᵢ fun h => s i h) =ᶠ[l] Set.interᵢ fun i => Set.interᵢ fun h => t i h
    def Filter.ofCountableInter {α : Type u_1} (l : Set (Set α)) (hp : ∀ (S : Set (Set α)), Set.Countable SS l⋂₀ S l) (h_mono : ∀ (s t : Set α), s ls tt l) :

    Construct a filter with countable intersection property. This constructor deduces Filter.univ_sets and Filter.inter_sets from the countable intersection property.

    Equations
    • One or more equations did not get rendered due to their size.
    instance Filter.countable_Inter_ofCountableInter {α : Type u_1} (l : Set (Set α)) (hp : ∀ (S : Set (Set α)), Set.Countable SS l⋂₀ S l) (h_mono : ∀ (s t : Set α), s ls tt l) :
    Equations
    @[simp]
    theorem Filter.mem_ofCountableInter {α : Type u_1} {l : Set (Set α)} (hp : ∀ (S : Set (Set α)), Set.Countable SS l⋂₀ S l) (h_mono : ∀ (s t : Set α), s ls tt l) {s : Set α} :
    instance countableInterFilter_inf {α : Type u_1} (l₁ : Filter α) (l₂ : Filter α) [inst : CountableInterFilter l₁] [inst : CountableInterFilter 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⊓ 𝓟 s.

    Equations
    instance countableInterFilter_sup {α : Type u_1} (l₁ : Filter α) (l₂ : Filter α) [inst : CountableInterFilter l₁] [inst : CountableInterFilter l₂] :

    Supremum of two countable_Inter_filters is a countable_Inter_filter.

    Equations