# Ranges of naturals as lists #

This file shows basic results about `List.iota`, `List.range`, `List.range'` and defines `List.finRange`. `finRange n` is the list of elements of `Fin n`. `iota n = [n, n - 1, ..., 1]` and `range n = [0, ..., n - 1]` are basic list constructions used for tactics. `range' a b = [a, ..., a + b - 1]` is there to help prove properties about them. Actual maths should use `List.Ico` instead.

source
theorem List.getElem_range'_1 {n m : ℕ} (i : ℕ) (H : i < (range' n m).length) :
(range' n m)[i] = n + i
source
theorem List.isChain_range (r : ℕ → ℕ → Prop) (n : ℕ) :
IsChain r (range n) ↔ ∀ (m : ℕ), m < n - 1 → r m m.succ
source
theorem List.isChain_range_succ (r : ℕ → ℕ → Prop) (n : ℕ) :
IsChain r (range n.succ) ↔ ∀ (m : ℕ), m < n → r m m.succ
source
theorem List.isChain_cons_range_succ (r : ℕ → ℕ → Prop) (n a : ℕ) :
IsChain r (a :: range n.succ) ↔ r a 0 ∧ ∀ (m : ℕ), m < n → r m m.succ
source
@[deprecated List.isChain_cons_range_succ (since := "2025-09-21")]
theorem List.chain_range_succ (r : ℕ → ℕ → Prop) (n a : ℕ) :
IsChain r (a :: range n.succ) ↔ r a 0 ∧ ∀ (m : ℕ), m < n → r m m.succ

Alias of `List.isChain_cons_range_succ`.

source
@[deprecated List.isChain_range_succ (since := "2025-09-24")]
theorem List.chain'_range_succ (r : ℕ → ℕ → Prop) (n : ℕ) :
IsChain r (range n.succ) ↔ ∀ (m : ℕ), m < n → r m m.succ

Alias of `List.isChain_range_succ`.

source
def List.ranges :
List ℕ → List (List ℕ)

From `l : List ℕ`, construct `l.ranges : List (List ℕ)` such that `l.ranges.map List.length = l` and `l.ranges.join = range l.sum`

- Example: `[1,2,3].ranges = [[0],[1,2],[3,4,5]]`

Equations

- [].ranges = []
- (a :: l).ranges = List.range a :: List.map (List.map fun (x : ℕ) => a + x) l.ranges

Instances For

source
theorem List.ranges_disjoint (l : List ℕ) :
Pairwise Disjoint l.ranges

The members of `l.ranges` are pairwise disjoint

source
theorem List.ranges_length (l : List ℕ) :
map length l.ranges = l

The lengths of the members of `l.ranges` are those given by `l`