length_rightInvSeq — Mathlib

English

The length of the right inversion sequence equals the length of the original word: |ris ω| = |ω|.

Русский

Длина правой последовательности инверсий равна длине исходного слова: |ris ω| = |ω|.

LaTeX

$$$|cs.rightInvSeq\, \omega| = |\omega|$$$

Lean4

@[simp]
theorem length_rightInvSeq (ω : List B) : (ris ω).length = ω.length := by
  induction ω with
  | nil => simp
  | cons i ω ih => simpa [rightInvSeq]

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