iterate_minimalPeriod — Mathlib

English

Applying the map f to x for an amount equal to the minimal period returns x again: f^[minimalPeriod f x] x = x.

Русский

Применение отображения f к x на количество, равное минимальному периоду, возвращает x: f^[minimalPeriod f x] x = x.

LaTeX

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

Lean4

@[simp]
theorem iterate_minimalPeriod : f^[minimalPeriod f x] x = x :=
  isPeriodicPt_minimalPeriod f x

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