English
For finite α, x belongs to periodicPts f if and only if x is periodic with period (|α|)! under f, i.e., x ∈ periodicPts f ⇔ IsPeriodicPt f (|α|)! x.
Русский
Для конечного множества α точка x принадлежит множеству периодических точек periodicPts f тогда и только тогда, когда x периодична при f с периодом (|α|)!, т.е. x ∈ periodicPts f ⇔ IsPeriodicPt f (|α|)! x.
LaTeX
$$$x \in \mathrm{periodicPts}(f) \iff \mathrm{IsPeriodicPt}(f, (|\alpha|)!, x)$$$
Lean4
theorem mem_periodicPts_iff_isPeriodicPt_factorial_card [Fintype α] : x ∈ periodicPts f ↔ IsPeriodicPt f (card α)! x
where
mp := isPeriodicPt_factorial_card_of_mem_periodicPts
mpr h := minimalPeriod_pos_iff_mem_periodicPts.mp (IsPeriodicPt.minimalPeriod_pos (Nat.factorial_pos _) h)