length_splitWrtComposition — Mathlib

English

If l is split according to a composition c, the total number of elements in the blocks is the length of c.

Русский

Если список l разбить по композиции c, то сумма длин блоков равна длине композиции.

LaTeX

$$$\operatorname{length}(l.splitWrtComposition(c)) = c.length$$$

Lean4

/-- When one splits a list along a composition `c`, the number of sublists thus created is
`c.length`. -/
@[simp]
theorem length_splitWrtComposition (l : List α) (c : Composition n) : length (l.splitWrtComposition c) = c.length :=
  length_splitWrtCompositionAux _ _

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