English
For a finite s and f a cycle-on s, for a,b ∈ s there exists n with f^n(a) = b and n < card(s).
Русский
Для конечного s и f цикла на s, для любых a,b ∈ s существует n < |s| такой, что f^n(a) = b.
LaTeX
$$$\mathrm{IsCycleOn}(f,s) \land a,b \in s \Rightarrow \exists n < |s|, (f^n)a = b$$$
Lean4
theorem isCycleOn_formPerm (h : l.Nodup) : l.formPerm.IsCycleOn {a | a ∈ l} :=
by
refine ⟨l.formPerm.bijOn fun _ => List.formPerm_mem_iff_mem, fun a ha b hb => ?_⟩
rw [Set.mem_setOf, ← List.idxOf_lt_length_iff] at ha hb
rw [← List.getElem_idxOf ha, ← List.getElem_idxOf hb]
refine ⟨l.idxOf b - l.idxOf a, ?_⟩
simp only [sub_eq_neg_add, zpow_add, zpow_neg, Equiv.Perm.inv_eq_iff_eq, zpow_natCast, Equiv.Perm.coe_mul,
List.formPerm_pow_apply_getElem _ h, Function.comp]
rw [add_comm]
