English
If two cycles are conjugate, their supports have the same cardinality, hence are of equal size.
Русский
Если два цикла коньюгированы, их поддержки имеют одинаковый кардинал, значит одинакового размера.
LaTeX
$$$\\forall \\sigma,\\tau : \\mathrm{Equiv.Perm}(\\alpha),\\; \\sigma.\\mathrm{IsCycle} \\land \\tau.\\mathrm{IsCycle} \\Rightarrow (\\sigma \\sim \\tau) \\Rightarrow |\\sigma.\\mathrm{support}| = |\\tau.\\mathrm{support}|.$$$
Lean4
theorem conj (h : f.IsCycleOn s) : (g * f * g⁻¹).IsCycleOn ((g : Perm α) '' s) :=
⟨(g.bijOn_image.comp h.1).comp g.bijOn_symm_image, fun x hx y hy =>
by
rw [← preimage_inv] at hx hy
convert Equiv.Perm.SameCycle.conj (h.2 hx hy) (g := g) <;> rw [apply_inv_self]⟩
