Lemmas about List.range and List.enum

Most of the results are deferred to Data.Init.List.Nat.Range, where more results about natural arithmetic are available.

Ranges and enumeration

enumFrom

@[simp]

theorem List.enumFrom_eq_nil {α : Type u_1} {n : Nat} {l : List α} : List.enumFrom n l = [] ↔ l = []

@[simp]

theorem List.enumFrom_length {α : Type u_1} {n : Nat} {l : List α} : (List.enumFrom n l).length = l.length

@[simp]

theorem List.getElem?_enumFrom {α : Type u_1} (n : Nat) (l : List α) (m : Nat) : (List.enumFrom n l)[m]? = Option.map (fun (a : α) => (n + m, a)) l[m]?

@[simp]

theorem List.getElem_enumFrom {α : Type u_1} (l : List α) (n : Nat) (i : Nat) (h : i < (List.enumFrom n l).length) : (List.enumFrom n l)[i] = (n + i, l[i])

theorem List.map_fst_add_enumFrom_eq_enumFrom {α : Type u_1} (l : List α) (n : Nat) (k : Nat) : List.map (Prod.map (fun (x : Nat) => x + n) id) (List.enumFrom k l) = List.enumFrom (n + k) l

theorem List.map_fst_add_enum_eq_enumFrom {α : Type u_1} (l : List α) (n : Nat) : List.map (Prod.map (fun (x : Nat) => x + n) id) l.enum = List.enumFrom n l