Documentation

Mathlib.Order.Filter.CardinalInter

Filters with a cardinal intersection property #

In this file we define CardinalInterFilter l c to be the class of filters with the following property: for any collection of sets s ∈ l with cardinality strictly less than c, their intersection belongs to l as well.

Main results #

Tags #

filter, cardinal

class CardinalInterFilter {α : Type u} (l : Filter α) (c : Cardinal.{u}) :

A filter l has the cardinal c intersection property if for any collection of less than c sets s ∈ l, their intersection belongs to l as well.

  • cardinal_sInter_mem : ∀ (S : Set (Set α)), Cardinal.mk S < c(sS, s l)⋂₀ S l

    For a collection of sets s ∈ l with cardinality below c, their intersection belongs to l as well.

Instances
    theorem CardinalInterFilter.cardinal_sInter_mem {α : Type u} {l : Filter α} {c : Cardinal.{u}} [self : CardinalInterFilter l c] (S : Set (Set α)) :
    Cardinal.mk S < c(sS, s l)⋂₀ S l

    For a collection of sets s ∈ l with cardinality below c, their intersection belongs to l as well.

    theorem cardinal_sInter_mem {α : Type u} {c : Cardinal.{u}} {l : Filter α} {S : Set (Set α)} [CardinalInterFilter l c] (hSc : Cardinal.mk S < c) :
    ⋂₀ S l sS, s l

    Every filter is a CardinalInterFilter with c = aleph0

    Every CardinalInterFilter with c > aleph0 is a CountableInterFilter

    Every CountableInterFilter is a CardinalInterFilter with c = aleph 1

    Equations
    • =

    Every CardinalInterFilter for some c also is a CardinalInterFilter for some a ≤ c

    theorem Filter.cardinal_iInter_mem {ι : Type u} {α : Type u} {c : Cardinal.{u}} {l : Filter α} [CardinalInterFilter l c] {s : ιSet α} (hic : Cardinal.mk ι < c) :
    ⋂ (i : ι), s i l ∀ (i : ι), s i l
    theorem Filter.cardinal_bInter_mem {ι : Type u} {α : Type u} {c : Cardinal.{u}} {l : Filter α} [CardinalInterFilter l c] {S : Set ι} (hS : Cardinal.mk S < c) {s : (i : ι) → i SSet α} :
    ⋂ (i : ι), ⋂ (hi : i S), s i hi l ∀ (i : ι) (hi : i S), s i hi l
    theorem Filter.eventually_cardinal_forall {ι : Type u} {α : Type u} {c : Cardinal.{u}} {l : Filter α} [CardinalInterFilter l c] {p : αιProp} (hic : Cardinal.mk ι < c) :
    (∀ᶠ (x : α) in l, ∀ (i : ι), p x i) ∀ (i : ι), ∀ᶠ (x : α) in l, p x i
    theorem Filter.eventually_cardinal_ball {ι : Type u} {α : Type u} {c : Cardinal.{u}} {l : Filter α} [CardinalInterFilter l c] {S : Set ι} (hS : Cardinal.mk S < c) {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 Filter.EventuallyLE.cardinal_iUnion {ι : Type u} {α : Type u} {c : Cardinal.{u}} {l : Filter α} [CardinalInterFilter l c] {s : ιSet α} {t : ιSet α} (hic : Cardinal.mk ι < c) (h : ∀ (i : ι), s i ≤ᶠ[l] t i) :
    ⋃ (i : ι), s i ≤ᶠ[l] ⋃ (i : ι), t i
    theorem Filter.EventuallyEq.cardinal_iUnion {ι : Type u} {α : Type u} {c : Cardinal.{u}} {l : Filter α} [CardinalInterFilter l c] {s : ιSet α} {t : ιSet α} (hic : Cardinal.mk ι < c) (h : ∀ (i : ι), s i =ᶠ[l] t i) :
    ⋃ (i : ι), s i =ᶠ[l] ⋃ (i : ι), t i
    theorem Filter.EventuallyLE.cardinal_bUnion {ι : Type u} {α : Type u} {c : Cardinal.{u}} {l : Filter α} [CardinalInterFilter l c] {S : Set ι} (hS : Cardinal.mk S < c) {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 Filter.EventuallyEq.cardinal_bUnion {ι : Type u} {α : Type u} {c : Cardinal.{u}} {l : Filter α} [CardinalInterFilter l c] {S : Set ι} (hS : Cardinal.mk S < c) {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 Filter.EventuallyLE.cardinal_iInter {ι : Type u} {α : Type u} {c : Cardinal.{u}} {l : Filter α} [CardinalInterFilter l c] {s : ιSet α} {t : ιSet α} (hic : Cardinal.mk ι < c) (h : ∀ (i : ι), s i ≤ᶠ[l] t i) :
    ⋂ (i : ι), s i ≤ᶠ[l] ⋂ (i : ι), t i
    theorem Filter.EventuallyEq.cardinal_iInter {ι : Type u} {α : Type u} {c : Cardinal.{u}} {l : Filter α} [CardinalInterFilter l c] {s : ιSet α} {t : ιSet α} (hic : Cardinal.mk ι < c) (h : ∀ (i : ι), s i =ᶠ[l] t i) :
    ⋂ (i : ι), s i =ᶠ[l] ⋂ (i : ι), t i
    theorem Filter.EventuallyLE.cardinal_bInter {ι : Type u} {α : Type u} {c : Cardinal.{u}} {l : Filter α} [CardinalInterFilter l c] {S : Set ι} (hS : Cardinal.mk S < c) {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 Filter.EventuallyEq.cardinal_bInter {ι : Type u} {α : Type u} {c : Cardinal.{u}} {l : Filter α} [CardinalInterFilter l c] {S : Set ι} (hS : Cardinal.mk S < c) {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.ofCardinalInter {α : Type u} {c : Cardinal.{u}} (l : Set (Set α)) (hc : 2 < c) (hl : ∀ (S : Set (Set α)), Cardinal.mk S < cS l⋂₀ S l) (h_mono : ∀ (s t : Set α), s ls tt l) :

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

    Equations
    • Filter.ofCardinalInter l hc hl h_mono = { sets := l, univ_sets := , sets_of_superset := , inter_sets := }
    Instances For
      instance Filter.cardinalInter_ofCardinalInter {α : Type u} {c : Cardinal.{u}} (l : Set (Set α)) (hc : 2 < c) (hl : ∀ (S : Set (Set α)), Cardinal.mk S < cS l⋂₀ S l) (h_mono : ∀ (s t : Set α), s ls tt l) :
      Equations
      • =
      @[simp]
      theorem Filter.mem_ofCardinalInter {α : Type u} {c : Cardinal.{u}} {l : Set (Set α)} (hc : 2 < c) (hl : ∀ (S : Set (Set α)), Cardinal.mk S < cS l⋂₀ S l) (h_mono : ∀ (s t : Set α), s ls tt l) {s : Set α} :
      s Filter.ofCardinalInter l hc hl h_mono s l
      def Filter.ofCardinalUnion {α : Type u} {c : Cardinal.{u}} (l : Set (Set α)) (hc : 2 < c) (hUnion : ∀ (S : Set (Set α)), Cardinal.mk S < c(sS, s l)⋃₀ S l) (hmono : tl, st, s l) :

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

      Equations
      Instances For
        instance Filter.cardinalInter_ofCardinalUnion {α : Type u} {c : Cardinal.{u}} (l : Set (Set α)) (hc : 2 < c) (h₁ : ∀ (S : Set (Set α)), Cardinal.mk S < c(sS, s l)⋃₀ S l) (h₂ : tl, st, s l) :
        Equations
        • =
        @[simp]
        theorem Filter.mem_ofCardinalUnion {α : Type u} {c : Cardinal.{u}} {l : Set (Set α)} (hc : 2 < c) {hunion : ∀ (S : Set (Set α)), Cardinal.mk S < c(sS, s l)⋃₀ S l} {hmono : tl, st, s l} {s : Set α} :
        s Filter.ofCardinalUnion l hc hunion hmono l s
        instance Filter.instCardinalInterFilterComap {α : Type u} {β : Type u} {c : Cardinal.{u}} (l : Filter β) [CardinalInterFilter l c] (f : αβ) :
        Equations
        • =
        instance Filter.instCardinalInterFilterMap {α : Type u} {β : Type u} {c : Cardinal.{u}} (l : Filter α) [CardinalInterFilter l c] (f : αβ) :
        Equations
        • =
        instance Filter.cardinalInterFilter_inf_eq {α : Type u} {c : Cardinal.{u}} (l₁ : Filter α) (l₂ : Filter α) [CardinalInterFilter l₁ c] [CardinalInterFilter l₂ c] :
        CardinalInterFilter (l₁ l₂) c

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

        Equations
        • =
        instance Filter.cardinalInterFilter_inf {α : Type u} (l₁ : Filter α) (l₂ : Filter α) {c₁ : Cardinal.{u}} {c₂ : Cardinal.{u}} [CardinalInterFilter l₁ c₁] [CardinalInterFilter l₂ c₂] :
        CardinalInterFilter (l₁ l₂) (c₁ c₂)
        Equations
        • =
        instance Filter.cardinalInterFilter_sup_eq {α : Type u} {c : Cardinal.{u}} (l₁ : Filter α) (l₂ : Filter α) [CardinalInterFilter l₁ c] [CardinalInterFilter l₂ c] :
        CardinalInterFilter (l₁ l₂) c

        Supremum of two CardinalInterFilters is a CardinalInterFilter.

        Equations
        • =
        instance Filter.cardinalInterFilter_sup {α : Type u} (l₁ : Filter α) (l₂ : Filter α) {c₁ : Cardinal.{u}} {c₂ : Cardinal.{u}} [CardinalInterFilter l₁ c₁] [CardinalInterFilter l₂ c₂] :
        CardinalInterFilter (l₁ l₂) (c₁ c₂)
        Equations
        • =
        inductive Filter.CardinalGenerateSets {α : Type u} {c : Cardinal.{u}} (g : Set (Set α)) :
        Set αProp

        Filter.CardinalGenerateSets c g is the (sets of the) greatest cardinalInterFilter c containing g.

        Instances For
          def Filter.cardinalGenerate {α : Type u} {c : Cardinal.{u}} (g : Set (Set α)) (hc : 2 < c) :

          Filter.cardinalGenerate c g is the greatest cardinalInterFilter c containing g.

          Equations
          Instances For
            theorem Filter.mem_cardinaleGenerate_iff {α : Type u} {c : Cardinal.{u}} {g : Set (Set α)} {s : Set α} {hreg : c.IsRegular} :
            s Filter.cardinalGenerate g Sg, Cardinal.mk S < c ⋂₀ S s

            A set is in the cardinalInterFilter generated by g if and only if it contains an intersection of c elements of g.

            theorem Filter.cardinalGenerate_isGreatest {α : Type u} {c : Cardinal.{u}} {g : Set (Set α)} (hc : 2 < c) :

            cardinalGenerate g hc is the greatest cardinalInterFilter c containing g.