ranges_length — Mathlib

English

The lengths of the inner lists in l.ranges are exactly the elements of l.

Русский

Длины вложенных списков в l.ranges равны элементам списка l.

LaTeX

$$$ (l.ranges).map\;\mathrm{length} = l $$$

Lean4

/-- The lengths of the members of `l.ranges` are those given by `l` -/
theorem ranges_length (l : List ℕ) : l.ranges.map length = l := by
  induction l with
  | nil => simp only [ranges, map_nil]
  | cons a l hl => -- (a :: l)

    simp only [ranges, map_cons, length_range, map_map, cons.injEq, true_and]
    conv_rhs => rw [← hl]
    apply map_congr_left
    intro s _
    simp only [Function.comp_apply, length_map]

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