isPeriodicPt_factorial_card_of_mem_periodicPts

English

If x is a periodic point of f and α is finite, then x is periodic with period (|α|)!, i.e., IsPeriodicPt f (|α|)! x.

Русский

Если x — периодическая точка отображения f на конечном множестве α, то период x делится на факториал размера α: IsPeriodicPt f (|α|)! x.

LaTeX

$$$\text{IsPeriodicPt}(f, (|\alpha|)!, x)$$$

Lean4

theorem isPeriodicPt_factorial_card_of_mem_periodicPts [Fintype α] (h : x ∈ periodicPts f) :
    IsPeriodicPt f (card α)! x :=
  isPeriodicPt_iff_minimalPeriod_dvd.mpr
    (Nat.dvd_factorial (minimalPeriod_pos_of_mem_periodicPts h) minimalPeriod_le_card)

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