getElem_iterate — Mathlib

English

For all f, a, n, i, with i < length(iterate f a n), the i-th element equals f^[i] a.

Русский

Для всех f, a, n, i при i < length(iterate f a n) i-й элемент равен f^[i] a.

LaTeX

$$$$ \\forall f\\, a\\, n\\, i:\\ i < \\operatorname{length}(\\operatorname{iterate} f\\, a\\, n) \\Rightarrow (\\operatorname{iterate} f\\, a\\, n)[i] = f^{[i]} a. $$$$

Lean4

@[simp]
theorem getElem_iterate (f : α → α) (a : α) (n : ℕ) (i : Nat) (h : i < (iterate f a n).length) :
    (iterate f a n)[i] = f^[i] a :=
  (getElem_eq_iff _).2 <| getElem?_iterate _ _ _ _ <| by rwa [length_iterate] at h

Похожие утверждения