iterate_eq_iterate_iff_of_lt_minimalPeriod

English

If m and n are both less than the minimal period, then f^m x = f^n x iff m = n.

Русский

Если m и n оба меньше минимального периода, то f^m(x) = f^n(x) тогда и только тогда, когда m = n.

LaTeX

$$$$ m < \\operatorname{minimalPeriod}(f,x) \\land n < \\operatorname{minimalPeriod}(f,x) \\Rightarrow (f^{[m]}x = f^{[n]}x \\iff m = n). $$$$

Lean4

theorem iterate_eq_iterate_iff_of_lt_minimalPeriod {m n : ℕ} (hm : m < minimalPeriod f x) (hn : n < minimalPeriod f x) :
    f^[m] x = f^[n] x ↔ m = n :=
  iterate_injOn_Iio_minimalPeriod.eq_iff hm hn

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