Intervals in ℕ #
This file defines intervals of naturals.
list.Ico m n is the list of integers greater than
and strictly less than
Icc, state basic lemmas about them.
- Also do the versions for integers?
- One could generalise even further, defining 'locally finite partial orders', for which
set.Ico a bis
[finite], and 'locally finite total orders', for which there is a list model.
- Once the above is done, get rid of
Ico n m is the list of natural numbers
n ≤ x < m.
(Ico stands for "interval, closed-open".)