iterate

Proves various lemmas about List.iterate.

@[simp]

theorem List.length_iterate {α : Type u_1} (f : α → α) (a : α) (n : ℕ) : (iterate f a n).length = n

@[simp]

theorem List.iterate_eq_nil {α : Type u_1} {f : α → α} {a : α} {n : ℕ} : iterate f a n = [] ↔ n = 0

theorem List.getElem?_iterate {α : Type u_1} (f : α → α) (a : α) (n i : ℕ) : i < n → (iterate f a n)[i]? = some (f^[i] a)

@[deprecated List.getElem?_iterate (since := "2024-08-23")]

theorem List.get?_iterate {α : Type u_1} (f : α → α) (a : α) (n i : ℕ) (h : i < n) : (iterate f a n).get? i = some (f^[i] a)

@[simp]

theorem List.getElem_iterate {α : Type u_1} (f : α → α) (a : α) (n i : ℕ) (h : i < (iterate f a n).length) : (iterate f a n)[i] = f^[i] a

@[deprecated List.getElem_iterate (since := "2024-08-23")]

theorem List.get_iterate {α : Type u_1} (f : α → α) (a : α) (n : ℕ) (i : Fin (iterate f a n).length) : (iterate f a n).get i = f^[↑i] a

@[simp]

theorem List.mem_iterate {α : Type u_1} {f : α → α} {a : α} {n : ℕ} {b : α} : b ∈ iterate f a n ↔ ∃ m < n, b = f^[m] a

@[simp]

theorem List.range_map_iterate {α : Type u_1} (n : ℕ) (f : α → α) (a : α) : map (fun (x : ℕ) => f^[x] a) (range n) = iterate f a n

theorem List.iterate_add {α : Type u_1} (f : α → α) (a : α) (m n : ℕ) : iterate f a (m + n) = iterate f a m ++ iterate f (f^[m] a) n

theorem List.take_iterate {α : Type u_1} (f : α → α) (a : α) (m n : ℕ) : take m (iterate f a n) = iterate f a (m ⊓ n)