of_zpow — Mathlib

English

If (f^n).IsCycleOn s for some integer n and s, and f is bijective on s, then f.IsCycleOn s.

Русский

Если существует целочисленная степень n, такая что (f^n) образует цикл на s, и f — биекция на s, тогда f образует цикл на s.

LaTeX

$$$(f^n).IsCycleOn(s) \land f.BijOn(s,s) \Rightarrow f.IsCycleOn(s)$$$

Lean4

theorem of_zpow {n : ℤ} (hf : (f ^ n).IsCycleOn s) (h : Set.BijOn f s s) : f.IsCycleOn s :=
  ⟨h, fun _ hx _ hy => (hf.2 hx hy).of_zpow⟩

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