isPeriodicPt_minimalPeriod — Mathlib

English

For any f and x, x is periodic with period equal to its minimal period; i.e., IsPeriodicPt f (minimalPeriod f x) x.

Русский

Для любых f и x точка x периодична с периодом, равным её минимальному периодy; то есть IsPeriodicPt f (minimalPeriod f x) x.

LaTeX

$$$$ \\text{IsPeriodicPt}(f, \\operatorname{minimalPeriod}(f,x), x). $$$$

Lean4

theorem isPeriodicPt_minimalPeriod (f : α → α) (x : α) : IsPeriodicPt f (minimalPeriod f x) x := by
  classical
  delta minimalPeriod
  split_ifs with hx
  · exact (Nat.find_spec hx).2
  · exact isPeriodicPt_zero f x

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