length_leftInvSeq — Mathlib

English

For every finite sequence ω, the left inverse sequence lis ω has the same length as ω; i.e., the operation lis preserves length.

Русский

Для любой конечной последовательности ω левая инверсионная последовательность lis ω имеет ту же длину, что и ω; то есть lis сохраняет длину.

LaTeX

$$$|\mathrm{lis}(\omega)| = |\omega|$$$

Lean4

@[simp]
theorem length_leftInvSeq (ω : List B) : (lis ω).length = ω.length := by
  simp [leftInvSeq_eq_reverse_rightInvSeq_reverse]

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