Intervals in ℕ #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
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 b is
[finite], and 'locally finite total orders', for which there is a list model.
- Once the above is done, get rid of
data.int.range (and maybe
Ico n m is the list of natural numbers
n ≤ x < m.
(Ico stands for "interval, closed-open".)
set.Ico, modelling intervals in general preorders, and
n ≤ x < m as a multiset or as a finset.
For any natural numbers n, a, and b, one of the following holds:
- n < a
- n ≥ b
- n ∈ Ico a b