rightInvSeq_reverse — Mathlib

English

The right inversion sequence reverses in a way consistent with word reversal: ris(ω.reverse) equals (lis ω).reverse.

Русский

Правая последовательность инверсий обращается так, чтобы соответствовать развороту слова: ris(ω.reverse) = (lis ω).reverse.

LaTeX

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

Lean4

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

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