map_length_splitWrtComposition — Mathlib

English

When splitting a list along a composition, the lengths of the produced sublists correspond to the block sizes of the composition.

Русский

При разбиении списка по композиции длины полученных подсписков соответствуют размерам блоков композиции.

LaTeX

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

Lean4

/-- When one splits a list along a composition `c`, the lengths of the sublists thus created are
given by the block sizes in `c`. -/
theorem map_length_splitWrtComposition (l : List α) (c : Composition l.length) :
    map length (l.splitWrtComposition c) = c.blocks :=
  map_length_splitWrtCompositionAux (le_of_eq c.blocks_sum)

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