data.list.range

Ranges of naturals as lists #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file shows basic results about list.iota, list.range, list.range' (all defined in data.list.defs) and defines list.fin_range. fin_range 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.

@[simp]
theorem list.length_range' (s n : ) :
n).length = n
@[simp]
theorem list.range'_eq_nil {s n : } :
n = 0
@[simp]
theorem list.mem_range' {m s n : } :
m n s m m < s + n
theorem list.map_add_range' (a s n : ) :
n) = list.range' (a + s) n
theorem list.map_sub_range' (a s n : ) (h : a s) :
list.map (λ (x : ), x - a) n) = list.range' (s - a) n
theorem list.chain_succ_range' (s n : ) :
list.chain (λ (a b : ), b = a.succ) s (list.range' (s + 1) n)
theorem list.chain_lt_range' (s n : ) :
(list.range' (s + 1) n)
theorem list.pairwise_lt_range' (s n : ) :
theorem list.nodup_range' (s n : ) :
n).nodup
@[simp]
theorem list.range'_append (s m n : ) :
m ++ list.range' (s + m) n = (n + m)
theorem list.range'_sublist_right {s m n : } :
m <+ n m n
theorem list.range'_subset_right {s m n : } :
m n m n
theorem list.nth_range' (s : ) {m n : } :
m < n n).nth m = option.some (s + m)
@[simp]
theorem list.nth_le_range' {n m : } (i : ) (H : i < m).length) :
m).nth_le i H = n + i
theorem list.range'_concat (s n : ) :
(n + 1) = n ++ [s + n]
theorem list.range_core_range' (s n : ) :
n) = (n + s)
theorem list.range_eq_range' (n : ) :
= n
theorem list.range_succ_eq_map (n : ) :
list.range (n + 1) = 0 ::
theorem list.range'_eq_map_range (s n : ) :
n = (list.range n)
@[simp]
theorem list.length_range (n : ) :
@[simp]
theorem list.range_eq_nil {n : } :
n = 0
theorem list.pairwise_lt_range (n : ) :
theorem list.pairwise_le_range (n : ) :
theorem list.nodup_range (n : ) :
theorem list.range_sublist {m n : } :
m n
theorem list.range_subset {m n : } :
m n
@[simp]
theorem list.mem_range {m n : } :
m m < n
@[simp]
theorem list.not_mem_range_self {n : } :
n
@[simp]
theorem list.self_mem_range_succ (n : ) :
n list.range (n + 1)
theorem list.nth_range {m n : } (h : m < n) :
theorem list.range_succ (n : ) :
= ++ [n]
@[simp]
theorem list.range_zero  :
theorem list.chain'_range_succ (r : Prop) (n : ) :
(list.range n.succ) (m : ), m < n r m m.succ
theorem list.chain_range_succ (r : Prop) (n a : ) :
a (list.range n.succ) r a 0 (m : ), m < n r m m.succ
theorem list.range_add (a b : ) :
list.range (a + b) = ++ list.map (λ (x : ), a + x) (list.range b)
@[simp]
theorem list.length_iota (n : ) :
theorem list.pairwise_gt_iota (n : ) :
theorem list.nodup_iota (n : ) :
theorem list.mem_iota {m n : } :
m 1 m m n
theorem list.reverse_range' (s n : ) :
n).reverse = list.map (λ (i : ), s + n - 1 - i) (list.range n)
def list.fin_range (n : ) :
list (fin n)

All elements of fin n, from 0 to n-1. The corresponding finset is finset.univ.

Equations
• = _
@[simp]
theorem list.fin_range_zero  :
@[simp]
theorem list.mem_fin_range {n : } (a : fin n) :
theorem list.nodup_fin_range (n : ) :
@[simp]
theorem list.length_fin_range (n : ) :
@[simp]
theorem list.fin_range_eq_nil {n : } :
n = 0
theorem list.prod_range_succ {α : Type u} [monoid α] (f : α) (n : ) :
theorem list.sum_range_succ {α : Type u} [add_monoid α] (f : α) (n : ) :
theorem list.prod_range_succ' {α : Type u} [monoid α] (f : α) (n : ) :
(list.map f (list.range n.succ)).prod = f 0 * (list.map (λ (i : ), f i.succ) (list.range n)).prod

A variant of prod_range_succ which pulls off the first term in the product rather than the last.

theorem list.sum_range_succ' {α : Type u} [add_monoid α] (f : α) (n : ) :
(list.map f (list.range n.succ)).sum = f 0 + (list.map (λ (i : ), f i.succ) (list.range n)).sum

A variant of sum_range_succ which pulls off the first term in the sum rather than the last.

@[simp]
theorem list.enum_from_map_fst {α : Type u} (n : ) (l : list α) :
=
@[simp]
theorem list.enum_map_fst {α : Type u} (l : list α) :
theorem list.enum_eq_zip_range {α : Type u} (l : list α) :
@[simp]
theorem list.unzip_enum_eq_prod {α : Type u} (l : list α) :
l.enum.unzip = , l)
theorem list.enum_from_eq_zip_range' {α : Type u} (l : list α) {n : } :
= l.length).zip l
@[simp]
theorem list.unzip_enum_from_eq_prod {α : Type u} (l : list α) {n : } :
l).unzip = l.length, l)
@[simp]
theorem list.nth_le_range {n : } (i : ) (H : i < (list.range n).length) :
(list.range n).nth_le i H = i
@[simp]
theorem list.nth_le_fin_range {n i : } (h : i < .length) :
.nth_le i h = i, _⟩