mem_periodicPts_iff_isPeriodicPt_factorial_card

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)

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