English
Let f be a permutation with f(f(x)) = x for a fixed x. Then for every integer i, f^i(x) is either x or f(x). Equivalently, the orbit of x under the cyclic group generated by f has at most two points.
Русский
Пусть f — перестановка such that f(f(x)) = x для фиксированного x. Тогда для любого целого i функция f^i(x) принимает значение либо x, либо f(x). Другими словами, орбита x под циклической подпгруппой, порождаемой f, состоит из не более чем двух элементов.
LaTeX
$$$$ f^2(x)=x \;\Rightarrow\; \forall i \in \mathbb{Z},\; f^i(x) \in \{x,\;f(x)\}. $$$$
Lean4
theorem zpow_apply_eq_of_apply_apply_eq_self {x : α} (hffx : f (f x) = x) : ∀ i : ℤ, (f ^ i) x = x ∨ (f ^ i) x = f x
| (n : ℕ) => pow_apply_eq_of_apply_apply_eq_self hffx n
| Int.negSucc n =>
by
rw [zpow_negSucc, inv_eq_iff_eq, ← f.injective.eq_iff, ← mul_apply, ← pow_succ', eq_comm, inv_eq_iff_eq, ←
mul_apply, ← pow_succ, @eq_comm _ x, or_comm]
exact pow_apply_eq_of_apply_apply_eq_self hffx _
