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.

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

• Filter.cocardinal α hreg = Filter.ofCardinalUnion {s : Set α | Cardinal.mk ↑s < c} ⋯ ⋯ ⋯

@[simp]

theorem Filter.mem_cocardinal {α : Type u} {c : Cardinal.{u}} {hreg : c.IsRegular} {s : Set α} : s ∈ Filter.cocardinal α hreg ↔ Cardinal.mk ↑sᶜ < c

@[simp]

theorem Filter.cocardinal_aleph0_eq_cofinite {α : Type u} : Filter.cocardinal α Cardinal.isRegular_aleph0 = Filter.cofinite

instance Filter.instCardinalInterFilter_cocardinal {α : Type u} {c : Cardinal.{u}} {hreg : c.IsRegular} : CardinalInterFilter (Filter.cocardinal α hreg) c

@[simp]

theorem Filter.eventually_cocardinal {α : Type u} {c : Cardinal.{u}} {hreg : c.IsRegular} {p : α → Prop} : (∀ᶠ (x : α) in Filter.cocardinal α hreg, p x) ↔ Cardinal.mk ↑{x : α | ¬p x} < c

theorem Filter.hasBasis_cocardinal {α : Type u} {c : Cardinal.{u}} {hreg : c.IsRegular} : (Filter.cocardinal α hreg).HasBasis {s : Set α | Cardinal.mk ↑s < c} compl

theorem Filter.frequently_cocardinal {α : Type u} {c : Cardinal.{u}} {hreg : c.IsRegular} {p : α → Prop} : (∃ᶠ (x : α) in Filter.cocardinal α hreg, p x) ↔ c ≤ Cardinal.mk ↑{x : α | p x}

theorem Filter.frequently_cocardinal_mem {α : Type u} {c : Cardinal.{u}} {hreg : c.IsRegular} {s : Set α} : (∃ᶠ (x : α) in Filter.cocardinal α hreg, x ∈ s) ↔ c ≤ Cardinal.mk ↑s

@[simp]

theorem Filter.cocardinal_inf_principal_neBot_iff {α : Type u} {c : Cardinal.{u}} {hreg : c.IsRegular} {s : Set α} : (Filter.cocardinal α hreg ⊓ Filter.principal s).NeBot ↔ c ≤ Cardinal.mk ↑s

theorem Filter.compl_mem_cocardinal_of_card_lt {α : Type u} {c : Cardinal.{u}} {hreg : c.IsRegular} {s : Set α} (hs : Cardinal.mk ↑s < c) : sᶜ ∈ Filter.cocardinal α hreg

theorem Set.Finite.compl_mem_cocardinal {α : Type u} {c : Cardinal.{u}} {hreg : c.IsRegular} {s : Set α} (hs : s.Finite) : sᶜ ∈ Filter.cocardinal α hreg

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 Filter.cocardinal α hreg, x ∉ s

theorem Finset.eventually_cocardinal_nmem {α : Type u} {c : Cardinal.{u}} {hreg : c.IsRegular} (s : Finset α) : ∀ᶠ (x : α) in Filter.cocardinal α hreg, x ∉ s

theorem Filter.eventually_cocardinal_ne {α : Type u} {c : Cardinal.{u}} {hreg : c.IsRegular} (x : α) : ∀ᶠ (a : α) in Filter.cocardinal α hreg, a ≠ x

@[reducible, inline]

abbrev Filter.cocountable {α : Type u} : Filter α

The filter defined by all sets that have countable complements.

Equations

• Filter.cocountable = Filter.cocardinal α Cardinal.isRegular_aleph_one

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