flatten_splitLengths — Mathlib

English

If l.length ≤ sz.sum, then flatten(sz.splitLengths l) = l.

Русский

Если длина l не превосходит суммы sz, то объединение частей sz.splitLengths l равно l.

LaTeX

$$$ (sz.splitLengths\\ l).flatten = l \\text{ if } l.length \\le sz.sum $$$

Lean4

theorem flatten_splitLengths (h : l.length ≤ sz.sum) : (sz.splitLengths l).flatten = l :=
  by
  induction sz generalizing l
  · simp_all
  case cons head tail ih =>
    simp only [splitLengths_cons, flatten_cons]
    rw [ih, take_append_drop]
    simpa [add_comm] using h

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