range_map_iterate — Mathlib

English

The map of the range: (range n).map (f^[·] a) equals the iterate f a n.

Русский

Отображение диапазона (range n) по функции (f^[·] a) даёт повторение iterate f a n.

LaTeX

$$$$ (\\operatorname{range} n).map (\\lambda x. f^{\\,[x]} a) = \\operatorname{iterate} f\\, a\\, n. $$$$

Lean4

@[simp]
theorem range_map_iterate (n : ℕ) (f : α → α) (a : α) : (List.range n).map (f^[·] a) = List.iterate f a n := by
  apply List.ext_getElem <;> simp

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