mathlib documentation


The cofinite filter

In this file we define

cofinite: the filter of sets with finite complement

and prove its basic properties. In particular, we prove that for it is equal to at_top.


Define filters for other cardinalities of the complement.

def filter.cofinite {α : Type u_1} :

The cofinite filter is the filter of subsets whose complements are finite.

theorem filter.mem_cofinite {α : Type u_1} {s : set α} :


theorem filter.frequently_cofinite_iff_infinite {α : Type u_1} {p : α → Prop} :
(∃ᶠ (x : α) in filter.cofinite, p x) {x : α | p x}.infinite

theorem set.finite.compl_mem_cofinite {α : Type u_1} {s : set α} :

theorem set.finite.eventually_cofinite_nmem {α : Type u_1} {s : set α} :
s.finite(∀ᶠ (x : α) in filter.cofinite, x s)

theorem finset.eventually_cofinite_nmem {α : Type u_1} (s : finset α) :
∀ᶠ (x : α) in filter.cofinite, x s

theorem set.infinite_iff_frequently_cofinite {α : Type u_1} {s : set α} :
s.infinite ∃ᶠ (x : α) in filter.cofinite, x s

theorem filter.eventually_cofinite_ne {α : Type u_1} (x : α) :
∀ᶠ (a : α) in filter.cofinite, a x

For natural numbers the filters cofinite and at_top coincide.