length_splitLengths_getElem_eq — Mathlib

English

For each i with i < (sz.splitLengths l).length, the i-th piece length equals sz[i].

Русский

Для каждого i с i < (sz.splitLengths l).length длина i-ой части равна sz[i].

LaTeX

$$$ \\forall i < (sz.splitLengths l).length, \\ (sz.splitLengths l)[i].length = sz[i] $$$

Lean4

theorem length_splitLengths_getElem_eq {i : ℕ} (hi : i < sz.length) (h : (sz.take (i + 1)).sum ≤ l.length) :
    ((sz.splitLengths l)[i]'(by simpa)).length = sz[i] :=
  by
  rw [List.getElem_take' (hj := i.lt_add_one)]
  simp only [take_splitLength]
  conv_rhs =>
    rw [List.getElem_take' (hj := i.lt_add_one)]
    simp +singlePass only [← map_splitLengths_length l _ h]
    rw [getElem_map]

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