injective_iff_iterate_factorial_card_eq_id

English

For finite α, f is injective iff the iterated map f^[(|α|)!] equals the identity, i.e., f^[(|α|)!] = id.

Русский

Для конечного множества α отображение f инъективно тогда и только тогда, когда повторная итерация f на степени (|α|)! равна тождественному отображению.

LaTeX

$$$\operatorname{Injective}(f) \iff f^{((|\alpha|)!) } = \mathrm{id}$$$

Lean4

theorem injective_iff_iterate_factorial_card_eq_id [Fintype α] : Injective f ↔ f^[(card α)!] = id := by
  simp only [injective_iff_periodicPts_eq_univ, mem_periodicPts_iff_isPeriodicPt_factorial_card, funext_iff,
    eq_univ_iff_forall, IsPeriodicPt, id, IsFixedPt]

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