English
Two formPerms on cycles are either equal or differ by subsingleton structure; equality corresponds to either equal cycles or same-subset structure.
Русский
Две формы formPerm совпадают либо если циклы совпадают, либо если циклы состоят из сопряжённых подпоследовательностей.
LaTeX
$$$\\text{formPerm\_eq\_formPerm\_iff}(s,s') \\iff s = s' \\lor (s.Subsingleton \\land s'.Subsingleton)$$$
Lean4
theorem cycleOf_formPerm (hl : Nodup l) (hn : 2 ≤ l.length) (x) : cycleOf l.attach.formPerm x = l.attach.formPerm :=
have hn : 2 ≤ l.attach.length := by rwa [← length_attach] at hn
have hl : l.attach.Nodup := by rwa [← nodup_attach] at hl
(isCycle_formPerm hl hn).cycleOf_eq ((formPerm_apply_mem_ne_self_iff _ hl _ (mem_attach _ _)).mpr hn)
