map_length_splitWrtCompositionAux

English

For any ns, if the length of l is at least the sum of the blocks, then the sequence of block lengths of l.splitWrtCompositionAux ns is exactly ns.

Русский

Для любого ns, если длина l не меньше суммы блоков, то последовательность длин блоков l.splitWrtCompositionAux ns равна ns.

LaTeX

$$$\operatorname{map}\,\operatorname{length}(l.splitWrtCompositionAux(ns)) = ns$$$

Lean4

theorem map_length_splitWrtCompositionAux {ns : List ℕ} :
    ∀ {l : List α}, ns.sum ≤ l.length → map length (l.splitWrtCompositionAux ns) = ns := by
  induction ns with
  | nil => simp [splitWrtCompositionAux]
  | cons n ns IH => grind [splitWrtCompositionAux_cons]

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