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 (fun (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
    theorem Finset.eventually_cocardinal_notMem {α : Type u} {c : Cardinal.{u}} {hreg : c.IsRegular} (s : Finset α) :
    ∀ᶠ (x : α) in Filter.cocardinal α hreg, x ∉ s
    source
    theorem Filter.eventually_cocardinal_ne {α : Type u} {c : Cardinal.{u}} {hreg : c.IsRegular} (x : α) :
    ∀ᶠ (a : α) in cocardinal α hreg, a ≠ x
    source
    @[reducible, inline]
    noncomputable 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