exists_nat_pow_eq — Mathlib

English

For finite α, if x and y are in the same f-cycle, there exists a finite i with (f^i) x = y.

Русский

Для конечного α существует конечная степень i такая что (f^i) x = y, если x,y в одном цикле f.

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_nat_pow_eq [Finite α] (h : SameCycle f x y) : ∃ i : ℕ, (f ^ i) x = y :=
  by
  obtain ⟨i, _, hi⟩ := h.exists_pow_eq'
  exact ⟨i, hi⟩

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