# Documentation

Mathlib.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.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.

@[simp]
theorem List.length_range' (s : ) (n : ) :
@[simp]
theorem List.range'_eq_nil {s : } {n : } :
= [] n = 0
@[simp]
theorem List.mem_range' {m : } {s : } {n : } :
m s m m < s + n
theorem List.map_add_range' (a : ) (s : ) (n : ) :
List.map ((fun x x_1 => x + x_1) a) () = List.range' (a + s) n
theorem List.map_sub_range' (a : ) (s : ) (n : ) :
a sList.map (fun x => x - a) () = List.range' (s - a) n
theorem List.chain_succ_range' (s : ) (n : ) :
List.Chain (fun a b => b = ) s (List.range' (s + 1) n)
theorem List.chain_lt_range' (s : ) (n : ) :
List.Chain (fun x x_1 => x < x_1) s (List.range' (s + 1) n)
theorem List.pairwise_lt_range' (s : ) (n : ) :
List.Pairwise (fun x x_1 => x < x_1) ()
@[simp]
theorem List.range'_append (s : ) (m : ) (n : ) :
++ List.range' (s + m) n = List.range' s (n + m)
theorem List.range'_sublist_right {s : } {m : } {n : } :
List.Sublist () () m n
theorem List.range'_subset_right {s : } {m : } {n : } :
m n
theorem List.get?_range' (s : ) {m : } {n : } :
m < nList.get? () m = some (s + m)
@[simp]
theorem List.get_range' {n : } {m : } (i : ) (H : i < List.length ()) :
List.get () { val := i, isLt := H } = n + i
@[simp]
theorem List.nthLe_range' {n : } {m : } (i : ) (H : i < List.length ()) :
List.nthLe () i H = n + i
theorem List.range'_concat (s : ) (n : ) :
List.range' s (n + 1) = ++ [s + n]
theorem List.range'_eq_map_range (s : ) (n : ) :
= List.map (fun x => s + x) ()
@[simp]
theorem List.length_range (n : ) :
= n
@[simp]
theorem List.range_eq_nil {n : } :
= [] n = 0
theorem List.pairwise_lt_range (n : ) :
List.Pairwise (fun x x_1 => x < x_1) ()
theorem List.pairwise_le_range (n : ) :
List.Pairwise (fun x x_1 => x x_1) ()
theorem List.range_sublist {m : } {n : } :
List.Sublist () () m n
theorem List.range_subset {m : } {n : } :
m n
@[simp]
theorem List.mem_range {m : } {n : } :
m m < n
theorem List.get?_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.Chain' r () (m : ) → m < nr m ()
theorem List.chain_range_succ (r : Prop) (n : ) (a : ) :
List.Chain r a () r a 0 ((m : ) → m < nr m ())
theorem List.range_add (a : ) (b : ) :
List.range (a + b) = ++ List.map (fun x => a + x) ()
@[simp]
theorem List.length_iota (n : ) :
= n
theorem List.pairwise_gt_iota (n : ) :
List.Pairwise (fun x x_1 => x > x_1) ()
theorem List.mem_iota {m : } {n : } :
m 1 m m n
theorem List.reverse_range' (s : ) (n : ) :
List.reverse () = List.map (fun i => s + n - 1 - i) ()
def List.finRange (n : ) :
List (Fin n)

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

Equations
@[simp]
theorem List.finRange_zero :
= []
@[simp]
theorem List.mem_finRange {n : } (a : Fin n) :
@[simp]
theorem List.length_finRange (n : ) :
@[simp]
theorem List.finRange_eq_nil {n : } :
= [] n = 0
theorem List.sum_range_succ {α : Type u} [inst : ] (f : α) (n : ) :
List.sum (List.map f ()) = List.sum (List.map f ()) + f n
theorem List.prod_range_succ {α : Type u} [inst : ] (f : α) (n : ) :
theorem List.sum_range_succ' {α : Type u} [inst : ] (f : α) (n : ) :
List.sum (List.map f ()) = f 0 + List.sum (List.map (fun i => f ()) ())

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

theorem List.prod_range_succ' {α : Type u} [inst : ] (f : α) (n : ) :
List.prod (List.map f ()) = f 0 * List.prod (List.map (fun i => f ()) ())

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

@[simp]
theorem List.enum_from_map_fst {α : Type u} (n : ) (l : List α) :
List.map Prod.fst () =
@[simp]
theorem List.enum_map_fst {α : Type u} (l : List α) :
List.map Prod.fst () =
theorem List.enum_eq_zip_range {α : Type u} (l : List α) :
= List.zip () l
@[simp]
theorem List.unzip_enum_eq_prod {α : Type u} (l : List α) :
= (, l)
theorem List.enum_from_eq_zip_range' {α : Type u} (l : List α) {n : } :
= List.zip () l
@[simp]
theorem List.unzip_enum_from_eq_prod {α : Type u} (l : List α) {n : } :
List.unzip () = (, l)
@[simp]
theorem List.get_range {n : } (i : ) (H : i < ) :
List.get () { val := i, isLt := H } = i
@[simp]
theorem List.nthLe_range {n : } (i : ) (H : i < ) :
List.nthLe () i H = i
@[simp]
theorem List.get_finRange {n : } {i : } (h : ) :
List.get () { val := i, isLt := h } = { val := i, isLt := (_ : i < n) }
@[simp]
theorem List.finRange_map_get {α : Type u} (l : List α) :
List.map () () = l
@[simp]
theorem List.nthLe_finRange {n : } {i : } (h : ) :
List.nthLe () i h = { val := i, isLt := (_ : i < n) }