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.
The cofinite filter is the filter of subsets whose complements are finite.
- One or more equations did not get rendered due to their size.
α is a preorder with no maximal element, then
atTop ≤ cofinite.
The coproduct of the cofinite filters on two types is the cofinite filter on their product.
For natural numbers the filters
For an injective function
f, inverse images of finite sets are finite. See also
The pullback of the
Filter.cofinite under an injective function is equal to
An injective sequence
f : ℕ → ℕ tends to infinity at infinity.