leftInvSeq_reverse — Mathlib

English

The left inversion sequence of a reversed word is the reverse of the right inversion sequence of the original word.

Русский

Левая последовательность инверсий перевернутого слова — это обратная последовательность правой инверсии исходного слова.

LaTeX

$$$cs.leftInvSeq\, \omega.reverse = (cs.rightInvSeq\, \omega).reverse$$$

Lean4

theorem leftInvSeq_reverse (ω : List B) : lis(ω.reverse) = (ris ω).reverse := by
  simp [leftInvSeq_eq_reverse_rightInvSeq_reverse]

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