iterate — Mathlib

English

For a function f : α → α and an initial element a, the list iterate f a n contains the first n iterates of f starting at a, i.e. [a, f(a), f(f(a)), ..., f^{n-1}(a)].

Русский

Для функции f : α → α и начала a, список iterate f a n содержит первые n итераций применения f к a: [a, f(a), f(f(a)), ..., f^{n-1}(a)].

LaTeX

$$$$\operatorname{iterate}(f,a,n) = [a, f(a), \ldots, f^{n-1}(a)].$$$$

Lean4

/-- `iterate f a n` is `[a, f a, ..., f^[n - 1] a]`. -/
@[simp]
def iterate (f : α → α) (a : α) : (n : ℕ) → List α
  | 0 => []
  | n + 1 => a :: iterate f (f a) n

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