ranges_flatten — Mathlib

English

For any list l of natural numbers, the concatenation of ranges of each element flattens to the single range from 0 to sum(l) − 1: l.ranges.flatten = range(l.sum).

Русский

Для списка натуральных чисел l последовательности диапазонов элементов сводятся к единому диапазону от 0 до sum(l) − 1: l.ranges.flatten = range(l.sum).

LaTeX

$$$\text{l.ranges.flatten} = \text{range}(\text{l.sum})$$$

Lean4

theorem ranges_flatten : ∀ (l : List ℕ), l.ranges.flatten = range l.sum
  | [] => rfl
  | a :: l => by simp [ranges, ← map_flatten, ranges_flatten, range_add]

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