English
For any type α and permutation f of α, the relation x ~ y defined by x and y lying in the same cycle of f is an equivalence relation on α.
Русский
Пусть α — множество, f — перестановка α. Отношение x ~ y, означающее, что x и y лежат в одной и той же цикле перестановки f, является эквивалентностью на α.
LaTeX
$$$R_f(x,y) := (x \\text{ SameCycle } f y) \\\\ R_f \\text{ является эквивалентностью на } \\alpha,$\n $$\\forall x\\in\\alpha,\\; R_f(x,x)\\quad\\land\\quad \\forall x,y\\in\\alpha,\\; R_f(x,y)\\Rightarrow R_f(y,x)\\quad\\land\\quad \\forall x,y,z\\in\\alpha,\\; (R_f(x,y) \\land R_f(y,z))\\Rightarrow R_f(x,z).$$$$
Lean4
/-- The setoid defined by the `SameCycle` relation. -/
def setoid (f : Perm α) : Setoid α where
r := f.SameCycle
iseqv := SameCycle.equivalence f
