image_iterate_eq — Mathlib

English

For any f: α → α and n ∈ ℕ, the image of the n-th iterate equals the n-th iterate of the image operator: image (f^[n]) = (image f)^[n].

Русский

Для любой f: α → α и натурального n, образ n-ой итерации равен n-ой итерации образа: image (f^[n]) = (image f)^[n].

LaTeX

$$$ \\operatorname{image}(f^{[n]}) = (\\operatorname{image} f)^{[n]}. $$$

Lean4

theorem image_iterate_eq {f : α → α} {n : ℕ} : image (f^[n]) = (image f)^[n] := by
  induction n with
  | zero => simp
  | succ n ih => rw [iterate_succ', iterate_succ', ← ih, image_comp_eq]

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