The cofinite filter #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
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
Define filters for other cardinalities of the complement.
The cofinite filter is the filter of subsets whose complements are finite.
α is a preorder with no maximal element, then
at_top ≤ cofinite.
The coproduct of the cofinite filters on two types is the cofinite filter on their product.
Finite product of finite sets is finite
For natural numbers the filters
An injective sequence
f : ℕ → ℕ tends to infinity at infinity.