Finite intervals of integers #
This file proves that ℤ
is a LocallyFiniteOrder
and calculates the cardinality of its
intervals as finsets and fintypes.
Equations
- One or more equations did not get rendered due to their size.
This file proves that ℤ
is a LocallyFiniteOrder
and calculates the cardinality of its
intervals as finsets and fintypes.