map_splitLengths_length — Mathlib

English

Mapping length across sz.splitLengths l yields sz provided sz.sum ≤ l.length.

Русский

Преобразование длины по sz.splitLengths l даёт sz при условии sz.sum ≤ l.length.

LaTeX

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

Lean4

theorem map_splitLengths_length (h : sz.sum ≤ l.length) : (sz.splitLengths l).map length = sz :=
  by
  induction sz generalizing l
  · simp
  case cons head tail ih =>
    simp only [sum_cons] at h
    simp only [splitLengths_cons, map_cons, length_take, cons.injEq, min_eq_left_iff]
    rw [ih]
    · simp [Nat.le_of_add_right_le h]
    · simp [Nat.le_sub_of_add_le' h]

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