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.
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]
@[instance]
Equations
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
For natural numbers the filters cofinite and at_top coincide.