iterate_eq_of_map_eq_add_int — Mathlib

English

If f x = x + m, then f^{[n]} x = x + n m for all n.

Русский

Если f(x) = x + m, тогда f^{[n]}(x) = x + n m для всех n.

LaTeX

$$$\forall x\in \mathbb{R}, \forall m\in \mathbb{Z},\; f(x) = x + m \Rightarrow \forall n\in \mathbb{N},\; f^{[n]}(x) = x + n m$$$

Lean4

theorem iterate_eq_of_map_eq_add_int {x : ℝ} {m : ℤ} (h : f x = x + m) (n : ℕ) : f^[n] x = x + n * m := by
  simpa only [nsmul_eq_mul, add_right_iterate] using (f.commute_add_int m).iterate_eq_of_map_eq n h

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