iterate_succ' — Mathlib

English

For any function f, the successor of n-th iterate equals f composed with the n-th iterate: f^{[n+1]} = f ∘ f^{[n]}.

Русский

Для любой функции f, следующая за n-й итерацией итерация равна композиции f с n-й итерацией: f^{[n+1]} = f ∘ f^{[n]}.

LaTeX

$$$$\forall f:\alpha\to\alpha,\forall n\in\mathbb{N},\ f^{[n+1]} = f\circ f^{[n]}. $$$$

Lean4

theorem iterate_succ' (n : ℕ) : f^[n.succ] = f ∘ f^[n] := by rw [iterate_succ, (Commute.self_iterate f n).comp_eq]

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