iterate_add_minimalPeriod_eq — Mathlib

English

For any n, f^[n + minimalPeriod f x] x = f^[n] x; i.e., adding one full period yields the same state after n iterations.

Русский

При любом n: f^[n + minimalPeriod f x] x = f^[n] x; то есть добавление полного периода приводит к тому же состоянию после n итераций.

LaTeX

$$$$ f^{n + \\operatorname{minimalPeriod}(f,x)}(x) = f^{n}(x). $$$$

Lean4

@[simp]
theorem iterate_add_minimalPeriod_eq : f^[n + minimalPeriod f x] x = f^[n] x :=
  by
  rw [iterate_add_apply]
  congr
  exact isPeriodicPt_minimalPeriod f x

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