apply_eq_self_iff — Mathlib

English

If x and y lie in the same f-cycle, then f fixes x if and only if it fixes y.

Русский

Пусть x и y лежат в одном циклe f. Тогда f фиксирует x тогда и только тогда, когда фиксирует y.

LaTeX

$$$\\forall f:\\mathrm{Perm}(\\alpha),\\; \\forall x,y:\\alpha,\\; \\mathrm{SameCycle}(f\\ x\\ y) \\Rightarrow (f(x)=x \\iff f(y)=y).$$$$

Lean4

theorem apply_eq_self_iff : SameCycle f x y → (f x = x ↔ f y = y) := fun ⟨i, hi⟩ => by
  rw [← hi, ← mul_apply, ← zpow_one_add, add_comm, zpow_add_one, mul_apply, (f ^ i).injective.eq_iff]

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