The cofinite filter #
In this file we define
Filter.cofinite: the filter of sets with finite complement
and prove its basic properties. In particular, we prove that for
ℕ it is equal to
Define filters for other cardinalities of the complement.
f tends to a countably generated filter
then for all but countably many elements,
f x ∈ l.ker.