Documentation

Mathlib.Order.Filter.Cocardinal

The cocardinal filter #

In this file we define Filter.cocardinal hc: the filter of sets with cardinality less than a regular cardinal c that satisfies Cardinal.aleph0 < c. Such filters are CardinalInterFilter with cardinality c.

source
def Filter.cocardinal (α : Type u) {c : Cardinal.{u}} (hreg : c.IsRegular) :
Filter α

The filter defined by all sets that have a complement with at most cardinality c. For a union of c sets of c elements to have c elements, we need that c is a regular cardinal.

Equations
    Instances For
      source
      @[simp]
      theorem Filter.mem_cocardinal {α : Type u} {c : Cardinal.{u}} {hreg : c.IsRegular} {s : Set α} :
      s ∈ cocardinal α hreg ↔ Cardinal.mk ↑sᶜ < c
      source
      @[simp]
      theorem Filter.cocardinal_aleph0_eq_cofinite {α : Type u} :
      cocardinal α Cardinal.isRegular_aleph0 = cofinite
      source
      instance Filter.instCardinalInterFilter_cocardinal {α : Type u} {c : Cardinal.{u}} {hreg : c.IsRegular} :
      CardinalInterFilter (cocardinal α hreg) c
      source
      @[simp]
      theorem Filter.eventually_cocardinal {α : Type u} {c : Cardinal.{u}} {hreg : c.IsRegular} {p : α → Prop} :
      (∀ᶠ (x : α) in cocardinal α hreg, p x) ↔ Cardinal.mk ↑{x : α | ¬p x} < c
      source
      theorem Filter.hasBasis_cocardinal {α : Type u} {c : Cardinal.{u}} {hreg : c.IsRegular} :
      (cocardinal α hreg).HasBasis {s : Set α | Cardinal.mk ↑s < c} compl
      source
      theorem Filter.frequently_cocardinal {α : Type u} {c : Cardinal.{u}} {hreg : c.IsRegular} {p : α → Prop} :
      (∃ᶠ (x : α) in cocardinal α hreg, p x) ↔ c ≤ Cardinal.mk ↑{x : α | p x}
      source
      theorem Filter.frequently_cocardinal_mem {α : Type u} {c : Cardinal.{u}} {hreg : c.IsRegular} {s : Set α} :
      (∃ᶠ (x : α) in cocardinal α hreg, x ∈ s) ↔ c ≤ Cardinal.mk ↑s
      source
      @[simp]
      theorem Filter.cocardinal_inf_principal_neBot_iff {α : Type u} {c : Cardinal.{u}} {hreg : c.IsRegular} {s : Set α} :
      (cocardinal α hreg ⊓ principal s).NeBot ↔ c ≤ Cardinal.mk ↑s
      source
      theorem Filter.compl_mem_cocardinal_of_card_lt {α : Type u} {c : Cardinal.{u}} {hreg : c.IsRegular} {s : Set α} (hs : Cardinal.mk ↑s < c) :
      sᶜ ∈ cocardinal α hreg
      source
      theorem Set.Finite.compl_mem_cocardinal {α : Type u} {c : Cardinal.{u}} {hreg : c.IsRegular} {s : Set α} (hs : s.Finite) :
      sᶜ ∈ Filter.cocardinal α hreg
      source
      theorem Filter.eventually_cocardinal_notMem_of_card_lt {α : Type u} {c : Cardinal.{u}} {hreg : c.IsRegular} {s : Set α} (hs : Cardinal.mk ↑s < c) :
      ∀ᶠ (x : α) in cocardinal α hreg, x ∉ s
      source
      @[deprecated Filter.eventually_cocardinal_notMem_of_card_lt (since := "2025-05-24")]
      theorem Filter.eventually_cocardinal_nmem_of_card_lt {α : Type u} {c : Cardinal.{u}} {hreg : c.IsRegular} {s : Set α} (hs : Cardinal.mk ↑s < c) :
      ∀ᶠ (x : α) in cocardinal α hreg, x ∉ s

      Alias of Filter.eventually_cocardinal_notMem_of_card_lt.

      source
      theorem Finset.eventually_cocardinal_notMem {α : Type u} {c : Cardinal.{u}} {hreg : c.IsRegular} (s : Finset α) :
      ∀ᶠ (x : α) in Filter.cocardinal α hreg, x ∉ s
      source
      @[deprecated Finset.eventually_cocardinal_notMem (since := "2025-05-24")]
      theorem Finset.eventually_cocardinal_nmem {α : Type u} {c : Cardinal.{u}} {hreg : c.IsRegular} (s : Finset α) :
      ∀ᶠ (x : α) in Filter.cocardinal α hreg, x ∉ s

      Alias of Finset.eventually_cocardinal_notMem.

      source
      theorem Filter.eventually_cocardinal_ne {α : Type u} {c : Cardinal.{u}} {hreg : c.IsRegular} (x : α) :
      ∀ᶠ (a : α) in cocardinal α hreg, a ≠ x
      source
      @[reducible, inline]
      abbrev Filter.cocountable {α : Type u} :
      Filter α

      The filter defined by all sets that have countable complements.

      Equations
        Instances For
          source
          theorem Filter.mem_cocountable {α : Type u} {s : Set α} :
          s ∈ cocountable ↔ sᶜ.Countable