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 : ℕ) : Ico 0 n = range n

@[simp]

theorem List.Ico.length (n m : ℕ) : (Ico n m).length = m - n

theorem List.Ico.pairwise_lt (n m : ℕ) : Pairwise (fun (x1 x2 : ℕ) => x1 < x2) (Ico n m)

theorem List.Ico.nodup (n m : ℕ) : (Ico n m).Nodup

@[simp]

theorem List.Ico.mem {n m l : ℕ} : l ∈ Ico n m ↔ n ≤ l ∧ l < m

theorem List.Ico.eq_nil_of_le {n m : ℕ} (h : m ≤ n) : Ico n m = []

theorem List.Ico.map_add (n m k : ℕ) : map (fun (x : ℕ) => k + x) (Ico n m) = Ico (n + k) (m + k)

theorem List.Ico.map_sub (n m k : ℕ) (h₁ : k ≤ n) : map (fun (x : ℕ) => x - k) (Ico n m) = Ico (n - k) (m - k)

@[simp]

theorem List.Ico.self_empty {n : ℕ} : Ico n n = []

@[simp]

theorem List.Ico.eq_empty_iff {n m : ℕ} : Ico n m = [] ↔ m ≤ n

theorem List.Ico.append_consecutive {n m l : ℕ} (hnm : n ≤ m) (hml : m ≤ l) : Ico n m ++ Ico m l = Ico n l

@[simp]

theorem List.Ico.inter_consecutive (n m l : ℕ) : Ico n m ∩ Ico m l = []

@[simp]

theorem List.Ico.bagInter_consecutive (n m l : ℕ) : (Ico n m).bagInter (Ico m l) = []

@[simp]

theorem List.Ico.succ_singleton {n : ℕ} : Ico n (n + 1) = [n]

theorem List.Ico.succ_top {n m : ℕ} (h : n ≤ m) : Ico n (m + 1) = Ico n m ++ [m]

theorem List.Ico.eq_cons {n m : ℕ} (h : n < m) : Ico n m = n :: Ico (n + 1) m

@[simp]

theorem List.Ico.pred_singleton {m : ℕ} (h : 0 < m) : Ico (m - 1) m = [m - 1]

theorem List.Ico.chain'_succ (n m : ℕ) : Chain' (fun (a b : ℕ) => b = a.succ) (Ico n m)

theorem List.Ico.notMem_top {n m : ℕ} : ¬m ∈ Ico n m

@[deprecated List.Ico.notMem_top (since := "2025-05-23")]

theorem List.Ico.not_mem_top {n m : ℕ} : ¬m ∈ Ico n m

Alias of List.Ico.notMem_top.

theorem List.Ico.filter_lt_of_top_le {n m l : ℕ} (hml : m ≤ l) : filter (fun (x : ℕ) => decide (x < l)) (Ico n m) = Ico n m

theorem List.Ico.filter_lt_of_le_bot {n m l : ℕ} (hln : l ≤ n) : filter (fun (x : ℕ) => decide (x < l)) (Ico n m) = []

theorem List.Ico.filter_lt_of_ge {n m l : ℕ} (hlm : l ≤ m) : filter (fun (x : ℕ) => decide (x < l)) (Ico n m) = Ico n l

@[simp]

theorem List.Ico.filter_lt (n m l : ℕ) : filter (fun (x : ℕ) => decide (x < l)) (Ico n m) = Ico n (min m l)

theorem List.Ico.filter_le_of_le_bot {n m l : ℕ} (hln : l ≤ n) : filter (fun (x : ℕ) => decide (l ≤ x)) (Ico n m) = Ico n m

theorem List.Ico.filter_le_of_top_le {n m l : ℕ} (hml : m ≤ l) : filter (fun (x : ℕ) => decide (l ≤ x)) (Ico n m) = []

theorem List.Ico.filter_le_of_le {n m l : ℕ} (hnl : n ≤ l) : filter (fun (x : ℕ) => decide (l ≤ x)) (Ico n m) = Ico l m

@[simp]

theorem List.Ico.filter_le (n m l : ℕ) : filter (fun (x : ℕ) => decide (l ≤ x)) (Ico n m) = Ico (max n l) m

theorem List.Ico.filter_lt_of_succ_bot {n m : ℕ} (hnm : n < m) : filter (fun (x : ℕ) => decide (x < n + 1)) (Ico n m) = [n]

@[simp]

theorem List.Ico.filter_le_of_bot {n m : ℕ} (hnm : n < m) : filter (fun (x : ℕ) => decide (x ≤ n)) (Ico n m) = [n]

theorem List.Ico.trichotomy (n a b : ℕ) : n < a ∨ b ≤ n ∨ n ∈ 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