English
For finite α, if x and y lie in the same f-cycle, there exists a finite power i (as a element of Fin(orderOf f)) such that (f^i) x = y.
Русский
Для конечного множества α, если x и y лежат в одном цикле f, существует конечная степень i (из Fin(orderOf f)) такая что (f^i) x = y.
LaTeX
$$$[Finite\\ \\alpha]\\;\\forall f:\\mathrm{Equiv.Perm}(\\alpha),\\; \\forall x,y:\\alpha,\\mathrm{SameCycle}(f,x,y) \\Rightarrow \\exists i: \\mathrm{Fin}(\\mathrm{orderOf}(f)), (f^{i}) x = y.$$$
Lean4
theorem exists_pow_eq'' [Finite α] (h : SameCycle f x y) : ∃ i : ℕ, 0 < i ∧ i ≤ orderOf f ∧ (f ^ i) x = y :=
by
obtain ⟨_ | i, hi, rfl⟩ := h.exists_pow_eq'
· refine ⟨orderOf f, orderOf_pos f, le_rfl, ?_⟩
rw [pow_orderOf_eq_one, pow_zero]
· exact ⟨i.succ, i.zero_lt_succ, hi.le, by rfl⟩
