length_splitWrtCompositionAux — Mathlib

English

For any list l and any ns, the number of sublists produced by splitting l along ns equals the length of ns.

Русский

Для любого списка l и ns количество полученных подсписков при разбиении l по ns равно длине ns.

LaTeX

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

Lean4

theorem length_splitWrtCompositionAux (l : List α) (ns) : length (l.splitWrtCompositionAux ns) = ns.length :=
  by
  induction ns generalizing l
  · simp [splitWrtCompositionAux, *]
  · simp [*]

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