instDecidableRelSameCycleOfNatOfDecidableEq

English

For a type α with decidable equality, the relation SameCycle(1) on α is decidable, and it is equivalent to equality: two elements lie in the same cycle of the identity permutation if and only if they are equal.

Русский

Для типа α с разрешимой эквивалентностью отношение SameCycle(1) на α разрешимо и эквивалентно равенству: два элемента лежат в одном цикле тождественной перестановки тогда и только если они равны.

LaTeX

$$$\mathrm{SameCycle}(\mathrm{id}_\alpha, x, y) \iff x = y$$$

Lean4

instance (priority := 100) [DecidableEq α] : DecidableRel (SameCycle (1 : Perm α)) := fun x y =>
  decidable_of_iff (x = y) sameCycle_one.symm

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