splitLengths_length_getElem — Mathlib

English

If the index i is within bounds, the i-th element of (sz.splitLengths l) has length sz[i].

Русский

Если индекс i в пределах, то длина i-ого элемента sz.splitLengths l равна sz[i].

LaTeX

$$$ (sz.splitLengths l)[i].length = sz[i] \\text{ for } i < (sz.splitLengths l).length $$$

Lean4

theorem splitLengths_length_getElem {α : Type*} (l : List α) (sz : List ℕ) (h : sz.sum ≤ l.length) (i : ℕ)
    (hi : i < (sz.splitLengths l).length) : (sz.splitLengths l)[i].length = sz[i]'(by simpa using hi) :=
  by
  have := map_splitLengths_length l sz h
  rw [← List.getElem_map List.length]
  · simp [this]
  · simpa using hi

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