minimalPeriod_apply — Mathlib

English

If x is periodic, then minimalPeriod f (f x) = minimalPeriod f x.

Русский

Если x периодична, то минимальный период f( f(x) ) равен минимальному периоду f(x).

LaTeX

$$$$ x \\in \\operatorname{periodicPts}(f) \\Rightarrow \\operatorname{minimalPeriod}(f, f(x)) = \\operatorname{minimalPeriod}(f,x). $$$$

Lean4

theorem minimalPeriod_apply (hx : x ∈ periodicPts f) : minimalPeriod f (f x) = minimalPeriod f x :=
  minimalPeriod_apply_iterate hx 1

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