iterate_add — Mathlib

English

For any f, a, m, n, iterate f a (m+n) equals iterate f a m concatenated with iterate f (f^m a) n.

Русский

Для любых f, a, m, n выполняется: iterate f a (m+n) равно конкатенации iterate f a m и iterate f (f^m a) n.

LaTeX

$$$$ \\operatorname{iterate} f\\, a\\,(m+n) = \\operatorname{iterate} f\\, a\\, m \\;\\;++\\;\\; \\operatorname{iterate} f\\,(f^{[m]} a)\\, n. $$$$

Lean4

theorem iterate_add (f : α → α) (a : α) (m n : ℕ) : iterate f a (m + n) = iterate f a m ++ iterate f (f^[m] a) n := by
  induction m generalizing a with
  | zero => simp
  | succ n ih => rw [iterate, add_right_comm, iterate, ih, Nat.iterate, cons_append]

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