splitWrtCompositionAux_cons — Mathlib

English

Let l be a finite list of elements and ns a list of natural numbers. If we split l according to the composition n :: ns, the resulting list is the first block consisting of the first n elements, followed by the split of the remaining elements according to ns.

Русский

Пусть l — конечный список элементов, ns — список натуральных чисел. Если разложить l по композиции n :: ns, то полученный список состоит из первого блока из первых n элементов и разбиения оставшейся части по ns.

LaTeX

$$$l.splitWrtCompositionAux (n :: ns) = take n l :: (drop n l).splitWrtCompositionAux ns$$$

Lean4

@[local simp]
theorem splitWrtCompositionAux_cons (l : List α) (n ns) :
    l.splitWrtCompositionAux (n :: ns) = take n l :: (drop n l).splitWrtCompositionAux ns := by
  simp [splitWrtCompositionAux]

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