English
The i-th element of the list produced by splitting l with c is the slice from sizeUpTo i to sizeUpTo i+1, i.e., the i-th block’s element range.
Русский
i-й элемент списка, полученного разбиением l по c, является срезом от sizeUpTo i до sizeUpTo (i+1).
LaTeX
$$$(l.splitWrtComposition c)[i] = (l.take (c.sizeUpTo (i + 1))).drop (c.sizeUpTo i)$$$
Lean4
/-- The `i`-th sublist in the splitting of a list `l` along a composition `c`, is the slice of `l`
between the indices `c.sizeUpTo i` and `c.sizeUpTo (i+1)`, i.e., the indices in the `i`-th
block of the composition. -/
theorem getElem_splitWrtComposition' (l : List α) (c : Composition n) {i : ℕ}
(hi : i < (l.splitWrtComposition c).length) :
(l.splitWrtComposition c)[i] = (l.take (c.sizeUpTo (i + 1))).drop (c.sizeUpTo i) :=
getElem_splitWrtCompositionAux _ _ hi
