of_pow — Mathlib

English

If (f^n) is a cycle-on s and f is bijective on s, then f is a cycle-on s.

Русский

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

LaTeX

$$$(f^n).IsCycleOn(s) \land f \text{ bijection on } s \Rightarrow f.IsCycleOn(s)$$$

Lean4

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

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