getElem?_iterate — Mathlib

English

For all n and i with i < n, the i-th element of iterate f a n is f^[i] a.

Русский

Для любых n и i, при i < n, i-й элемент iterate f a n равен f^[i] a.

LaTeX

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

Lean4

theorem getElem?_iterate (f : α → α) (a : α) : ∀ (n i : ℕ), i < n → (iterate f a n)[i]? = f^[i] a
  | n + 1, 0, _ => by simp
  | n + 1, i + 1, h => by simp [getElem?_iterate f (f a) n i (by simpa using h)]

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