conj — Mathlib

English

If x and y lie on the same f-cycle, then their images under g lie on the same cycle of the conjugated permutation g f g⁻¹.

Русский

Если x и y лежат в одном цикле f, то g x и g y лежат в одном цикле у перестановки g f g⁻¹.

LaTeX

$$$\\forall f,g: \\mathrm{Perm}(\\alpha),\\; \\forall x,y:\\alpha,\\; \\mathrm{SameCycle}(f)\\ x\\ y \\Rightarrow \\mathrm{SameCycle}(g f g^{-1})\\ (g x)\\ (g y).$$$

Lean4

theorem conj : SameCycle f x y → SameCycle (g * f * g⁻¹) (g x) (g y) := by simp [sameCycle_conj]

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