mathlib documentation

order.filter.cofinite

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.

TODO

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.

Equations

filter.cofinite = {sets := {s : set α | sᶜ.finite}, univ_sets := _, sets_of_superset := _, inter_sets := _}

@[simp]

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

s ∈ filter.cofinite ↔ sᶜ.finite

@[instance]

def filter.cofinite_ne_bot {α : Type u_1} [infinite α] :

filter.cofinite.ne_bot

theorem filter.frequently_cofinite_iff_infinite {α : Type u_1} {p : α → Prop} :

(∃ᶠ (x : α) in filter.cofinite, p x) ↔ {x : α | p x}.infinite

theorem set.infinite_iff_frequently_cofinite {α : Type u_1} {s : set α} :

s.infinite ↔ ∃ᶠ (x : α) in filter.cofinite, x ∈ s

theorem nat.cofinite_eq_at_top :

filter.cofinite = filter.at_top

For natural numbers the filters cofinite and at_top coincide.