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.

theorem List.getElem_range'_1 {n m : ℕ} (i : ℕ) (H : i < (range' n m).length) : (range' n m)[i] = n + i

theorem List.chain'_range_succ (r : ℕ → ℕ → Prop) (n : ℕ) : Chain' r (range n.succ) ↔ ∀ (m : ℕ), m < n → r m m.succ

theorem List.chain_range_succ (r : ℕ → ℕ → Prop) (n a : ℕ) : Chain r a (range n.succ) ↔ r a 0 ∧ ∀ (m : ℕ), m < n → r m m.succ

@[deprecated List.get_range' (since := "2024-08-19")]

theorem List.nthLe_range' {n m step : ℕ} (i : ℕ) (H : i < (range' n m step).length) : (range' n m step).get ⟨i, H⟩ = n + step * i

Alias of List.get_range'.

@[deprecated List.getElem_range'_1 (since := "2024-08-19")]

theorem List.nthLe_range'_1 {n m : ℕ} (i : ℕ) (H : i < (range' n m).length) : (range' n m)[i] = n + i

Alias of List.getElem_range'_1.

@[deprecated List.get_range (since := "2024-08-19")]

theorem List.nthLe_range {n : ℕ} (i : ℕ) (H : i < (range n).length) : (range n).get ⟨i, H⟩ = i

Alias of List.get_range.

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

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

The members of l.ranges are pairwise disjoint

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

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

@[deprecated "Use `List.ranges_flatten`." (since := "2024-10-17")]

theorem List.ranges_flatten' (l : List ℕ) : l.ranges.flatten = range (Nat.sum l)

See List.ranges_flatten for the version about List.sum.

@[deprecated List.ranges_flatten' (since := "2024-10-15")]

theorem List.ranges_join' (l : List ℕ) : l.ranges.flatten = range (Nat.sum l)

Alias of List.ranges_flatten'.

---

See List.ranges_flatten for the version about List.sum.

@[deprecated "Use `List.mem_mem_ranges_iff_lt_sum`." (since := "2024-11-18")]

theorem List.mem_mem_ranges_iff_lt_natSum (l : List ℕ) {n : ℕ} : (∃ (s : List ℕ), s ∈ l.ranges ∧ n ∈ s) ↔ n < Nat.sum l

Any entry of any member of l.ranges is strictly smaller than Nat.sum l. See List.mem_mem_ranges_iff_lt_sum for the version about List.sum.