iterate_pos_eq_iff — Mathlib

English

For all f,x,m,n>0, f^{[n]}(x) = x + n m iff f(x) = x + m.

Русский

Для любых f, x, m и n>0: f^{[n]}(x) = x + n m тогда и только тогда, когда f(x) = x + m.

LaTeX

$$$\forall f, x, m, n:\; 0 < n \Rightarrow f^{[n]}(x) = x + n m \;\Leftrightarrow\; f(x) = x + m$$$

Lean4

theorem iterate_pos_eq_iff {x : ℝ} {m : ℤ} {n : ℕ} (hn : 0 < n) : f^[n] x = x + n * m ↔ f x = x + m := by
  simpa only [nsmul_eq_mul, add_right_iterate] using
    (f.commute_add_int m).iterate_pos_eq_iff_map_eq f.monotone (strictMono_id.add_const (m : ℝ)) hn

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