getElem_splitWrtCompositionAux — Mathlib

English

For the i-th block (i.e., index i in the partition), the i-th element is given by the slice of l from sizeUpTo i to sizeUpTo i+1.

Русский

Для i-го блока i-й элемент задаётся как срез списка от размераUpTo i до размераUpTo i+1.

LaTeX

$$$(l.splitWrtCompositionAux ns)[i] = (l.take (ns.take (i+1)).sum).drop (ns.take i).sum$$$

Lean4

theorem getElem_splitWrtCompositionAux (l : List α) (ns : List ℕ) {i : ℕ}
    (hi : i < (l.splitWrtCompositionAux ns).length) :
    (l.splitWrtCompositionAux ns)[i] = (l.take (ns.take (i + 1)).sum).drop (ns.take i).sum := by
  induction ns generalizing l i with
  | nil => cases hi
  | cons n ns IH =>
    rcases i with - | i
    · simp
    · simp only [splitWrtCompositionAux, getElem_cons_succ, IH, take, sum_cons, splitAt_eq, drop_take, drop_drop]
      rw [Nat.add_sub_add_left]

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