# 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
Instances For
@[simp]
theorem List.Ico.length (n : ) (m : ) :
(List.Ico n m).length = m - n
theorem List.Ico.pairwise_lt (n : ) (m : ) :
List.Pairwise (fun (x1 x2 : ) => x1 < x2) (List.Ico n m)
theorem List.Ico.nodup (n : ) (m : ) :
(List.Ico n m).Nodup
@[simp]
theorem List.Ico.mem {n : } {m : } {l : } :
l List.Ico n m n l l < m
theorem List.Ico.eq_nil_of_le {n : } {m : } (h : m n) :
List.Ico n m = []
theorem List.Ico.map_add (n : ) (m : ) (k : ) :
List.map (fun (x : ) => k + x) (List.Ico n m) = List.Ico (n + k) (m + k)
theorem List.Ico.map_sub (n : ) (m : ) (k : ) (h₁ : k n) :
List.map (fun (x : ) => x - k) (List.Ico n m) = List.Ico (n - k) (m - k)
@[simp]
theorem List.Ico.self_empty {n : } :
List.Ico n n = []
@[simp]
theorem List.Ico.eq_empty_iff {n : } {m : } :
List.Ico n m = [] m n
theorem List.Ico.append_consecutive {n : } {m : } {l : } (hnm : n m) (hml : m l) :
@[simp]
theorem List.Ico.inter_consecutive (n : ) (m : ) (l : ) :
List.Ico n m List.Ico m l = []
@[simp]
theorem List.Ico.bagInter_consecutive (n : ) (m : ) (l : ) :
(List.Ico n m).bagInter (List.Ico m l) = []
@[simp]
theorem List.Ico.succ_singleton {n : } :
List.Ico n (n + 1) = [n]
theorem List.Ico.succ_top {n : } {m : } (h : n m) :
List.Ico n (m + 1) = List.Ico n m ++ [m]
theorem List.Ico.eq_cons {n : } {m : } (h : n < m) :
List.Ico n 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' (fun (a b : ) => b = a.succ) (List.Ico n m)
theorem List.Ico.not_mem_top {n : } {m : } :
theorem List.Ico.filter_lt_of_top_le {n : } {m : } {l : } (hml : m l) :
List.filter (fun (x : ) => decide (x < l)) (List.Ico n m) = List.Ico n m
theorem List.Ico.filter_lt_of_le_bot {n : } {m : } {l : } (hln : l n) :
List.filter (fun (x : ) => decide (x < l)) (List.Ico n m) = []
theorem List.Ico.filter_lt_of_ge {n : } {m : } {l : } (hlm : l m) :
List.filter (fun (x : ) => decide (x < l)) (List.Ico n m) = List.Ico n l
@[simp]
theorem List.Ico.filter_lt (n : ) (m : ) (l : ) :
List.filter (fun (x : ) => decide (x < l)) (List.Ico n m) = List.Ico n (min m l)
theorem List.Ico.filter_le_of_le_bot {n : } {m : } {l : } (hln : l n) :
List.filter (fun (x : ) => decide (l x)) (List.Ico n m) = List.Ico n m
theorem List.Ico.filter_le_of_top_le {n : } {m : } {l : } (hml : m l) :
List.filter (fun (x : ) => decide (l x)) (List.Ico n m) = []
theorem List.Ico.filter_le_of_le {n : } {m : } {l : } (hnl : n l) :
List.filter (fun (x : ) => decide (l x)) (List.Ico n m) = List.Ico l m
@[simp]
theorem List.Ico.filter_le (n : ) (m : ) (l : ) :
List.filter (fun (x : ) => decide (l x)) (List.Ico n m) = List.Ico (max n l) m
theorem List.Ico.filter_lt_of_succ_bot {n : } {m : } (hnm : n < m) :
List.filter (fun (x : ) => decide (x < n + 1)) (List.Ico n m) = [n]
@[simp]
theorem List.Ico.filter_le_of_bot {n : } {m : } (hnm : n < m) :
List.filter (fun (x : ) => decide (x n)) (List.Ico n m) = [n]
theorem List.Ico.trichotomy (n : ) (a : ) (b : ) :
n < a b n n List.Ico a 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