splitWrtCompositionAux — Mathlib

English

Auxiliary procedure that, given a list and a sequence of cut positions, splits the list into sublists according to those positions.

Русский

Вспомогательная процедура: дан список и последовательность позиций разреза, она разделяет список на подсписки по этим положениям.

LaTeX

$$$\\mathrm{splitWrtCompositionAux}:\\mathrm{List}\\,\\alpha \\to \\mathrm{List}\\,\\mathbb{N} \\to \\mathrm{List}(\\mathrm{List}\\,\\alpha)$ with recursive definition $\\dots$$$

Lean4

/-- Auxiliary for `List.splitWrtComposition`. -/
def splitWrtCompositionAux : List α → List ℕ → List (List α)
  | _, [] => []
  | l, n :: ns =>
    let (l₁, l₂) := l.splitAt n
    l₁ :: splitWrtCompositionAux l₂ ns

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