getElem_splitWrtComposition — Mathlib

English

Similarly, the i-th element of the i-th block equals the slice from sizeUpTo i to sizeUpTo (i+1).

Русский

Аналогично, i-й элемент i-го блока равен срезу от sizeUpTo i до sizeUpTo (i+1).

LaTeX

$$$(l.splitWrtComposition c)[i] = (l.take (c.sizeUpTo i)).drop (c.sizeUpTo i).sum$$$

Lean4

theorem getElem_splitWrtComposition (l : List α) (c : Composition n) (i : Nat)
    (h : i < (l.splitWrtComposition c).length) :
    (l.splitWrtComposition c)[i] = (l.take (c.sizeUpTo (i + 1))).drop (c.sizeUpTo i) :=
  getElem_splitWrtComposition' _ _ h

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