splitLengths_cons — Mathlib

English

Splitting with a cons head n: (n :: sz).splitLengths l = l.take n :: sz.splitLengths (l.drop n).

Русский

Разбиение с конструктором cons head n: (n :: sz).splitLengths l = l.take n :: sz.splitLengths (l.drop n).

LaTeX

$$$ (n :: sz).splitLengths\\ l = \\ l.take n \\;::\\; sz.splitLengths(\\ l.drop n) $$$

Lean4

@[simp]
theorem splitLengths_cons (n : ℕ) : (n :: sz).splitLengths l = l.take n :: sz.splitLengths (l.drop n) := by
  simp [splitLengths]

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