Documentation

Mathlib.Data.List.Iterate

iterate #

Proves various lemmas about List.iterate.

@[simp]
theorem List.length_iterate {α : Type u_1} (f : αα) (a : α) (n : ) :
(List.iterate f a n).length = n
@[simp]
theorem List.iterate_eq_nil {α : Type u_1} {f : αα} {a : α} {n : } :
List.iterate f a n = [] n = 0
theorem List.getElem?_iterate {α : Type u_1} (f : αα) (a : α) (n : ) (i : ) :
i < n(List.iterate f a n)[i]? = some (f^[i] a)
@[deprecated List.getElem?_iterate]
theorem List.get?_iterate {α : Type u_1} (f : αα) (a : α) (n : ) (i : ) (h : i < n) :
(List.iterate f a n).get? i = some (f^[i] a)
@[simp]
theorem List.getElem_iterate {α : Type u_1} (f : αα) (a : α) (n : ) (i : ) (h : i < (List.iterate f a n).length) :
(List.iterate f a n)[i] = f^[i] a
@[deprecated List.getElem_iterate]
theorem List.get_iterate {α : Type u_1} (f : αα) (a : α) (n : ) (i : Fin (List.iterate f a n).length) :
(List.iterate f a n).get i = f^[i] a
@[simp]
theorem List.mem_iterate {α : Type u_1} {f : αα} {a : α} {n : } {b : α} :
b List.iterate f a n m < n, b = f^[m] a
@[simp]
theorem List.range_map_iterate {α : Type u_1} (n : ) (f : αα) (a : α) :
List.map (fun (x : ) => f^[x] a) (List.range n) = List.iterate f a n
theorem List.iterate_add {α : Type u_1} (f : αα) (a : α) (m : ) (n : ) :
List.iterate f a (m + n) = List.iterate f a m ++ List.iterate f (f^[m] a) n
theorem List.take_iterate {α : Type u_1} (f : αα) (a : α) (m : ) (n : ) :