# mathlibdocumentation

data.list.intervals

# Intervals in ℕ #

This file defines intervals of naturals. list.Ico m n is the list of integers greater than m and strictly less than n.

## TODO #

• Define Ioo and 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 list.range'?).
def list.Ico (n m : ) :

Ico n m is the list of natural numbers n ≤ x < m. (Ico stands for "interval, closed-open".)

See also data/set/intervals.lean for set.Ico, modelling intervals in general preorders, and multiset.Ico and finset.Ico for n ≤ x < m as a multiset or as a finset.

Equations
• m = (m - n)
theorem list.Ico.zero_bot (n : ) :
n =
@[simp]
theorem list.Ico.length (n m : ) :
(list.Ico n m).length = m - n
theorem list.Ico.pairwise_lt (n m : ) :
theorem list.Ico.nodup (n m : ) :
@[simp]
theorem list.Ico.mem {n m l : } :
l m n l l < m
theorem list.Ico.eq_nil_of_le {n m : } (h : m n) :
theorem list.Ico.map_add (n m k : ) :
(list.Ico n m) = list.Ico (n + k) (m + k)
theorem list.Ico.map_sub (n m k : ) (h₁ : k n) :
list.map (λ (x : ), x - k) (list.Ico n m) = list.Ico (n - k) (m - k)
@[simp]
theorem list.Ico.self_empty {n : } :
@[simp]
theorem list.Ico.eq_empty_iff {n m : } :
m n
theorem list.Ico.append_consecutive {n m l : } (hnm : n m) (hml : m l) :
m ++ l = l
@[simp]
theorem list.Ico.inter_consecutive (n m l : ) :
@[simp]
@[simp]
theorem list.Ico.succ_singleton {n : } :
(n + 1) = [n]
theorem list.Ico.succ_top {n m : } (h : n m) :
(m + 1) = m ++ [m]
theorem list.Ico.eq_cons {n m : } (h : n < m) :
m = n :: list.Ico (n + 1) m
@[simp]
theorem list.Ico.pred_singleton {m : } (h : 0 < m) :
list.Ico (m - 1) m = [m - 1]
theorem list.Ico.chain'_succ (n m : ) :
list.chain' (λ (a b : ), b = a.succ) (list.Ico n m)
@[simp]
theorem list.Ico.not_mem_top {n m : } :
m m
theorem list.Ico.filter_lt_of_top_le {n m l : } (hml : m l) :
list.filter (λ (x : ), x < l) (list.Ico n m) = m
theorem list.Ico.filter_lt_of_le_bot {n m l : } (hln : l n) :
list.filter (λ (x : ), x < l) (list.Ico n m) = list.nil
theorem list.Ico.filter_lt_of_ge {n m l : } (hlm : l m) :
list.filter (λ (x : ), x < l) (list.Ico n m) = l
@[simp]
theorem list.Ico.filter_lt (n m l : ) :
list.filter (λ (x : ), x < l) (list.Ico n m) = l)
theorem list.Ico.filter_le_of_le_bot {n m l : } (hln : l n) :
list.filter (λ (x : ), l x) (list.Ico n m) = m
theorem list.Ico.filter_le_of_top_le {n m l : } (hml : m l) :
list.filter (λ (x : ), l x) (list.Ico n m) = list.nil
theorem list.Ico.filter_le_of_le {n m l : } (hnl : n l) :
list.filter (λ (x : ), l x) (list.Ico n m) = m
@[simp]
theorem list.Ico.filter_le (n m l : ) :
list.filter (λ (x : ), l x) (list.Ico n m) = list.Ico l) m
theorem list.Ico.filter_lt_of_succ_bot {n m : } (hnm : n < m) :
list.filter (λ (x : ), x < n + 1) (list.Ico n m) = [n]
@[simp]
theorem list.Ico.filter_le_of_bot {n m : } (hnm : n < m) :
list.filter (λ (x : ), x n) (list.Ico n m) = [n]
theorem list.Ico.trichotomy (n a b : ) :
n < a b n n b

For any natural numbers n, a, and b, one of the following holds:

1. n < a
2. n ≥ b
3. n ∈ Ico a b