minimalPeriod_pos — Mathlib

English

If x is periodic for f, and f^n(x) is periodic with some period m, then x is periodic with period m.

Русский

Если x периодично относительно f, и f^n(x) имеет период m, то x периодично относительно f с периодом m.

LaTeX

$$$$ x \\in \\operatorname{periodicPts}(f) \\land \\operatorname{IsPeriodicPt}(f,m,f^{[n]}(x)) \\Rightarrow \\operatorname{IsPeriodicPt}(f,m,x). $$$$

Lean4

theorem minimalPeriod_pos (hn : 0 < n) (hx : IsPeriodicPt f n x) : 0 < minimalPeriod f x :=
  minimalPeriod_pos_of_mem_periodicPts <| mk_mem_periodicPts hn hx

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