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.pairwise_lt_range'
(s : ℕ)
(n : ℕ)
(step : optParam ℕ 1)
:
autoParam (0 < step) _auto✝ → List.Pairwise (fun (x x_1 : ℕ) => x < x_1) (List.range' s n step)
theorem
List.nodup_range'
(s : ℕ)
(n : ℕ)
(step : optParam ℕ 1)
(h : autoParam (0 < step) _auto✝)
:
(List.range' s n step).Nodup
@[simp]
theorem
List.nthLe_range'
{n : ℕ}
{m : ℕ}
{step : ℕ}
(i : ℕ)
(H : i < (List.range' n m step).length)
:
(List.range' n m step).nthLe i H = n + step * i
theorem
List.nthLe_range'_1
{n : ℕ}
{m : ℕ}
(i : ℕ)
(H : i < (List.range' n m).length)
:
(List.range' n m).nthLe i H = n + i
theorem
List.chain'_range_succ
(r : ℕ → ℕ → Prop)
(n : ℕ)
:
List.Chain' r (List.range n.succ) ↔ ∀ m < n, r m m.succ
theorem
List.chain_range_succ
(r : ℕ → ℕ → Prop)
(n : ℕ)
(a : ℕ)
:
List.Chain r a (List.range n.succ) ↔ r a 0 ∧ ∀ m < n, r m m.succ
All elements of Fin n
, from 0
to n-1
. The corresponding finset is Finset.univ
.
Equations
- List.finRange n = List.pmap Fin.mk (List.range n) ⋯
Instances For
theorem
List.pairwise_lt_finRange
(n : ℕ)
:
List.Pairwise (fun (x x_1 : Fin n) => x < x_1) (List.finRange n)
theorem
List.pairwise_le_finRange
(n : ℕ)
:
List.Pairwise (fun (x x_1 : Fin n) => x ≤ x_1) (List.finRange n)
@[simp]
theorem
List.enumFrom_eq_zip_range'
{α : Type u}
(l : List α)
{n : ℕ}
:
List.enumFrom n l = (List.range' n l.length).zip l
@[simp]
theorem
List.unzip_enumFrom_eq_prod
{α : Type u}
(l : List α)
{n : ℕ}
:
(List.enumFrom n l).unzip = (List.range' n l.length, l)
@[simp]
theorem
List.nthLe_range
{n : ℕ}
(i : ℕ)
(H : i < (List.range n).length)
:
(List.range n).nthLe i H = i
@[simp]
theorem
List.getElem_finRange
{n : ℕ}
{i : ℕ}
(h : i < (List.finRange n).length)
:
(List.finRange n)[i] = ⟨i, ⋯⟩
theorem
List.get_finRange
{n : ℕ}
{i : ℕ}
(h : i < (List.finRange n).length)
:
(List.finRange n).get ⟨i, h⟩ = ⟨i, ⋯⟩
@[simp]
theorem
List.finRange_map_get
{α : Type u}
(l : List α)
:
List.map l.get (List.finRange l.length) = l
@[simp]
theorem
List.nthLe_finRange
{n : ℕ}
{i : ℕ}
(h : i < (List.finRange n).length)
:
(List.finRange n).nthLe i h = ⟨i, ⋯⟩
@[simp]
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
Instances For
The members of l.ranges
are pairwise disjoint
See List.ranges_join
for the version about List.sum
.