mathlib documentation

data.list.range

Ranges of naturals as lists #

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 = [1, ..., n] 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 : ) :
@[simp]
theorem list.range'_eq_nil {s n : } :
@[simp]
theorem list.mem_range' {m s n : } :
m list.range' s n s m m < s + n
theorem list.map_add_range' (a s n : ) :
theorem list.map_sub_range' (a s n : ) (h : a s) :
list.map (λ (x : ), x - a) (list.range' s 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.nodup_range' (s n : ) :
@[simp]
theorem list.range'_append (s m n : ) :
list.range' s m ++ list.range' (s + m) n = list.range' s (n + m)
theorem list.nth_range' (s : ) {m n : } :
m < n(list.range' s n).nth m = option.some (s + m)
@[simp]
theorem list.nth_le_range' {n m : } (i : ) (H : i < (list.range' n m).length) :
(list.range' n m).nth_le i H = n + i
theorem list.range'_concat (s n : ) :
list.range' s (n + 1) = list.range' s n ++ [s + n]
@[simp]
theorem list.length_range (n : ) :
@[simp]
theorem list.range_eq_nil {n : } :
theorem list.nodup_range (n : ) :
@[simp]
theorem list.mem_range {m n : } :
@[simp]
theorem list.not_mem_range_self {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 : ) :
@[simp]
theorem list.chain'_range_succ (r : → Prop) (n : ) :
list.chain' r (list.range n.succ) ∀ (m : ), m < nr m m.succ
theorem list.chain_range_succ (r : → Prop) (n a : ) :
list.chain r a (list.range n.succ) r a 0 ∀ (m : ), m < nr m m.succ
theorem list.range_add (a b : ) :
list.range (a + b) = list.range a ++ list.map (λ (x : ), a + x) (list.range b)
@[simp]
theorem list.length_iota (n : ) :
theorem list.nodup_iota (n : ) :
theorem list.mem_iota {m n : } :
m list.iota n 1 m m n
theorem list.reverse_range' (s n : ) :
(list.range' s 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.mem_fin_range {n : } (a : fin n) :
@[simp]
@[simp]
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 α) :
theorem list.enum_from_eq_zip_range' {α : Type u} (l : list α) {n : } :
@[simp]
theorem list.unzip_enum_from_eq_prod {α : Type u} (l : list α) {n : } :
@[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 < (list.fin_range n).length) :
(list.fin_range n).nth_le i h = i, _⟩
@[simp]
theorem list.map_nth_le {α : Type u} (l : list α) :
list.map (λ (n : fin l.length), l.nth_le n _) (list.fin_range l.length) = l
theorem list.of_fn_eq_pmap {α : Type u_1} {n : } {f : fin n → α} :
list.of_fn f = list.pmap (λ (i : ) (hi : i < n), f i, hi⟩) (list.range n) _
theorem list.of_fn_eq_map {α : Type u_1} {n : } {f : fin n → α} :
theorem list.nodup_of_fn {α : Type u_1} {n : } {f : fin n → α} (hf : function.injective f) :