formPerm_eq_formPerm_iff — Mathlib

English

Two formPerms are equal iff the underlying cycles are equal or both are subsingletons.

Русский

Два formPerm равны тогда и только тогда, когда соответствующие циклы равны или оба являются подпоследовательностями.

LaTeX

$$$s.formPerm hs = s'.formPerm hs' \\iff s = s' \\lor (s.Subsingleton \\land s'.Subsingleton)$$$

Lean4

nonrec theorem formPerm_eq_formPerm_iff {α : Type*} [DecidableEq α] {s s' : Cycle α} {hs : s.Nodup} {hs' : s'.Nodup} :
    s.formPerm hs = s'.formPerm hs' ↔ s = s' ∨ s.Subsingleton ∧ s'.Subsingleton :=
  by
  rw [Cycle.length_subsingleton_iff, Cycle.length_subsingleton_iff]
  revert s s'
  intro s s'
  apply @Quotient.inductionOn₂' _ _ _ _ _ s s'
  intro l l' hl hl'
  simpa using formPerm_eq_formPerm_iff hl hl'

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