minimalPeriod_le_card — Mathlib

English

For any x in α, the minimal period of f at x is at most the size of α, i.e., minimalPeriod f x ≤ |α| when α is finite.

Русский

Для любых x в α минимальный период f при x не превосходит мощности множества α: minimalPeriod f x ≤ |α|, когда α конечно.

LaTeX

$$$\min( \text{minimalPeriod}(f, x)) \leq |\alpha|$$$

Lean4

theorem minimalPeriod_le_card [Fintype α] : minimalPeriod f x ≤ card α :=
  by
  rw [← periodicOrbit_length]
  exact List.Nodup.length_le_card nodup_periodicOrbit

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