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 Int.range (and maybe List.range'?).

def List.Ico (n m : ℕ) : List ℕ

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

See also Mathlib/Order/Interval/Basic.lean for modelling intervals in general preorders, as well as sibling definitions alongside it such as Set.Ico, Multiset.Ico and Finset.Ico for sets, multisets and finite sets respectively.

Equations

• List.Ico n m = List.range' n (m - n)

theorem List.Ico.zero_bot (n : ℕ) : List.Ico 0 n = List.range n

@[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) : List.Ico n m ++ List.Ico m l = List.Ico n 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 : ℕ} : ¬m ∈ List.Ico 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 (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 (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