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 : ℕ) : List.take m (List.iterate f a n) = List.iterate f a (min m n)