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 their intersection belongs to l as well.

Two main examples are the residual filter defined in Mathlib.Topology.GDelta and the MeasureTheory.Measure.ae filter defined in MeasureTheory.MeasureSpace.

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.

Note that there also exists a typeclass CardinalInterFilter, and thus an alternative spelling of CountableInterFilter as CardinalInterFilter l (aleph 1). The former (defined here) is the preferred spelling; it has the advantage of not requiring the user to import the theory ordinals.

Tags #

filter, countable

class CountableInterFilter {α : Type u_2} (l : Filter α) :

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

  • countable_sInter_mem : ∀ (S : Set (Set α)), Set.Countable S(sS, s l)⋂₀ S l

    For a countable collection of sets s ∈ l, their intersection belongs to l as well.

Instances
    theorem countable_sInter_mem {α : Type u_2} {l : Filter α} [CountableInterFilter l] {S : Set (Set α)} (hSc : Set.Countable S) :
    ⋂₀ S l sS, s l
    theorem countable_iInter_mem {ι : Sort u_1} {α : Type u_2} {l : Filter α} [CountableInterFilter l] [Countable ι] {s : ιSet α} :
    ⋂ (i : ι), s i l ∀ (i : ι), s i l
    theorem countable_bInter_mem {α : Type u_2} {l : Filter α} [CountableInterFilter l] {ι : Type u_4} {S : Set ι} (hS : Set.Countable S) {s : (i : ι) → i SSet α} :
    ⋂ (i : ι), ⋂ (hi : i S), s i hi l ∀ (i : ι) (hi : i S), s i hi l
    theorem eventually_countable_forall {ι : Sort u_1} {α : Type u_2} {l : Filter α} [CountableInterFilter l] [Countable ι] {p : αιProp} :
    (∀ᶠ (x : α) in l, ∀ (i : ι), p x i) ∀ (i : ι), ∀ᶠ (x : α) in l, p x i
    theorem eventually_countable_ball {α : Type u_2} {l : Filter α} [CountableInterFilter l] {ι : Type u_4} {S : Set ι} (hS : Set.Countable S) {p : α(i : ι) → i SProp} :
    (∀ᶠ (x : α) in l, ∀ (i : ι) (hi : i S), p x i hi) ∀ (i : ι) (hi : i S), ∀ᶠ (x : α) in l, p x i hi
    theorem EventuallyLE.countable_iUnion {ι : Sort u_1} {α : Type u_2} {l : Filter α} [CountableInterFilter l] [Countable ι] {s : ιSet α} {t : ιSet α} (h : ∀ (i : ι), s i ≤ᶠ[l] t i) :
    ⋃ (i : ι), s i ≤ᶠ[l] ⋃ (i : ι), t i
    theorem EventuallyEq.countable_iUnion {ι : Sort u_1} {α : Type u_2} {l : Filter α} [CountableInterFilter l] [Countable ι] {s : ιSet α} {t : ιSet α} (h : ∀ (i : ι), s i =ᶠ[l] t i) :
    ⋃ (i : ι), s i =ᶠ[l] ⋃ (i : ι), t i
    theorem EventuallyLE.countable_bUnion {α : Type u_2} {l : Filter α} [CountableInterFilter l] {ι : Type u_4} {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) :
    ⋃ (i : ι), ⋃ (h : i S), s i h ≤ᶠ[l] ⋃ (i : ι), ⋃ (h : i S), t i h
    theorem EventuallyEq.countable_bUnion {α : Type u_2} {l : Filter α} [CountableInterFilter l] {ι : Type u_4} {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) :
    ⋃ (i : ι), ⋃ (h : i S), s i h =ᶠ[l] ⋃ (i : ι), ⋃ (h : i S), t i h
    theorem EventuallyLE.countable_iInter {ι : Sort u_1} {α : Type u_2} {l : Filter α} [CountableInterFilter l] [Countable ι] {s : ιSet α} {t : ιSet α} (h : ∀ (i : ι), s i ≤ᶠ[l] t i) :
    ⋂ (i : ι), s i ≤ᶠ[l] ⋂ (i : ι), t i
    theorem EventuallyEq.countable_iInter {ι : Sort u_1} {α : Type u_2} {l : Filter α} [CountableInterFilter l] [Countable ι] {s : ιSet α} {t : ιSet α} (h : ∀ (i : ι), s i =ᶠ[l] t i) :
    ⋂ (i : ι), s i =ᶠ[l] ⋂ (i : ι), t i
    theorem EventuallyLE.countable_bInter {α : Type u_2} {l : Filter α} [CountableInterFilter l] {ι : Type u_4} {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) :
    ⋂ (i : ι), ⋂ (h : i S), s i h ≤ᶠ[l] ⋂ (i : ι), ⋂ (h : i S), t i h
    theorem EventuallyEq.countable_bInter {α : Type u_2} {l : Filter α} [CountableInterFilter l] {ι : Type u_4} {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) :
    ⋂ (i : ι), ⋂ (h : i S), s i h =ᶠ[l] ⋂ (i : ι), ⋂ (h : i S), t i h
    def Filter.ofCountableInter {α : Type u_2} (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
    Instances For
      instance Filter.countableInter_ofCountableInter {α : Type u_2} (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_2} {l : Set (Set α)} (hp : ∀ (S : Set (Set α)), Set.Countable SS l⋂₀ S l) (h_mono : ∀ (s t : Set α), s ls tt l) {s : Set α} :
      def Filter.ofCountableUnion {α : Type u_2} (p : Set αProp) (hUnion : ∀ (S : Set (Set α)), Set.Countable S(sS, p s)p (⋃₀ S)) (hmono : ∀ (t : Set α), p tst, p s) :

      Construct a filter with countable intersection property. Similarly to Filter.comk, a set belongs to this filter if its complement satisfies the property. Similarly to Filter.ofCountableInter, this constructor deduces some properties from the countable intersection property which becomes the countable union property because we take complements of all sets.

      Another small difference from Filter.ofCountableInter is that this definition takes p : Set α → Prop instead of Set (Set α).

      Equations
      Instances For
        instance Filter.countableInter_ofCountableUnion {α : Type u_2} (p : Set αProp) (h₁ : ∀ (S : Set (Set α)), Set.Countable S(sS, p s)p (⋃₀ S)) (h₂ : ∀ (t : Set α), p tst, p s) :
        Equations
        • =
        @[simp]
        theorem Filter.mem_ofCountableUnion {α : Type u_2} {p : Set αProp} {hunion : ∀ (S : Set (Set α)), Set.Countable S(sS, p s)p (⋃₀ S)} {hmono : ∀ (t : Set α), p tst, p s} {s : Set α} :
        s Filter.ofCountableUnion p hunion hmono p s
        Equations
        • =
        Equations
        • =
        Equations
        • =
        instance instCountableInterFilterComap {α : Type u_2} {β : Type u_3} (l : Filter β) [CountableInterFilter l] (f : αβ) :
        Equations
        • =
        instance instCountableInterFilterMap {α : Type u_2} {β : Type u_3} (l : Filter α) [CountableInterFilter l] (f : αβ) :
        Equations
        • =
        instance countableInterFilter_inf {α : Type u_2} (l₁ : Filter α) (l₂ : Filter α) [CountableInterFilter l₁] [CountableInterFilter l₂] :

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

        Equations
        • =
        instance countableInterFilter_sup {α : Type u_2} (l₁ : Filter α) (l₂ : Filter α) [CountableInterFilter l₁] [CountableInterFilter l₂] :

        Supremum of two CountableInterFilters is a CountableInterFilter.

        Equations
        • =
        inductive Filter.CountableGenerateSets {α : Type u_2} (g : Set (Set α)) :
        Set αProp

        Filter.CountableGenerateSets g is the (sets of the) greatest countableInterFilter containing g.

        Instances For
          def Filter.countableGenerate {α : Type u_2} (g : Set (Set α)) :

          Filter.countableGenerate g is the greatest countableInterFilter containing g.

          Equations
          Instances For
            theorem Filter.mem_countableGenerate_iff {α : Type u_2} {g : Set (Set α)} {s : Set α} :

            A set is in the countableInterFilter generated by g if and only if it contains a countable intersection of elements of g.

            countableGenerate g is the greatest countableInterFilter containing g.