length_splitLengths_getElem_le — Mathlib

English

The length of the i-th piece sz.splitLengths l equals sz[i].

Русский

Длина i-ой части sz.splitLengths l равна sz[i].

LaTeX

$$$ ((sz.splitLengths l)[i]).length = sz[i] $$$

Lean4

theorem length_splitLengths_getElem_le {i : ℕ} {hi : i < (sz.splitLengths l).length} :
    (sz.splitLengths l)[i].length ≤ sz[i]'(by simpa using hi) :=
  by
  induction sz generalizing l i
  · simp at hi
  case cons head tail tail_ih =>
    simp only [splitLengths_cons]
    cases i
    · simp
    · simp only [getElem_cons_succ, tail_ih]

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