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 := _}
Instances for filter.cofinite
If α
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 cofinite
and at_top
coincide.
For an injective function f
, inverse images of finite sets are finite. See also
filter.comap_cofinite_le
and function.injective.comap_cofinite_eq
.
The pullback of the filter.cofinite
under an injective function is equal to filter.cofinite
.
See also filter.comap_cofinite_le
and function.injective.tendsto_cofinite
.
An injective sequence f : ℕ → ℕ
tends to infinity at infinity.