sum_take_map_length_splitWrtComposition

English

The sum of the lengths of the first i blocks equals the i-th prefix size of the original list, i.e., the i-th partial size in the composition.

Русский

Сумма длин первых i блоков равна размеру префикса исходного списка, соответствующему i-му шагу композиции.

LaTeX

$$$\left(\mathrm{take}\ i\ (\mathrm{map}\ \mathrm{length}\ (l.splitWrtComposition c))\right).\mathrm{sum} = c.sizeUpTo i$$$

Lean4

theorem sum_take_map_length_splitWrtComposition (l : List α) (c : Composition l.length) (i : ℕ) :
    (((l.splitWrtComposition c).map length).take i).sum = c.sizeUpTo i :=
  by
  congr
  exact map_length_splitWrtComposition l c

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