take_splitLength — Mathlib

English

Taking i elements from sz.splitLengths l equals splitting sz into i parts then taking i from l.

Русский

Взятие i элементов из sz.splitLengths l эквивалентно взятию i частей sz.splitLengths l от l.

LaTeX

$$$ (sz.splitLengths l).take i = (sz.take i).splitLengths l $$$

Lean4

theorem take_splitLength (i : ℕ) : (sz.splitLengths l).take i = (sz.take i).splitLengths l :=
  by
  induction i generalizing sz l
  case zero => simp
  case succ i hi =>
    cases sz
    · simp
    · simp only [splitLengths_cons, take_succ_cons, hi]

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