comp_iterate — Mathlib

English

If f and g commute, then the n-th iterate of their composition equals the composition of their n-th iterates: (f ∘ g)^{[n]} = f^{[n]} ∘ g^{[n]}.

Русский

Если f и g commute, то n-я итерация их композиции равна композиции их n-й итераций: (f ∘ g)^{[n]} = f^{[n]} ∘ g^{[n]}.

LaTeX

$$$$\forall f,g:\alpha\to\alpha,\ (f\circ g = g\circ f)\Rightarrow \forall n\in\mathbb{N},\ (f\circ g)^{[n]} = f^{[n]}\circ g^{[n]}. $$$$

Lean4

theorem comp_iterate (h : Commute f g) (n : ℕ) : (f ∘ g)^[n] = f^[n] ∘ g^[n] := by
  induction n with
  | zero => rfl
  | succ n ihn =>
    funext x
    simp only [ihn, (h.iterate_right n).eq, iterate_succ, comp_apply]

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