English
Let l be a finite list of natural numbers. The numbers that appear in any subrange of any member of l.ranges are exactly the numbers 0,1,..., sum(l)−1. Equivalently, for every n, there exists some s in l.ranges with n in s if and only if n < sum(l).
Русский
Пусть l — конечный список натуральных чисел. Числа, которые встречаются в любом диапазоне, входящем в любой элемент l.ranges, совпадают с числами 0,1,..., сумма(l)−1. Эквивалентно: для каждого n существует s в l.ranges с n в s тогда и только тогда n < сумма(l).
LaTeX
$$$$(\exists s \in l.ranges,\ n \in s) \iff n < l.sum.$$$$
Lean4
/-- Any entry of any member of `l.ranges` is strictly smaller than `l.sum`. -/
theorem mem_mem_ranges_iff_lt_sum (l : List ℕ) {n : ℕ} : (∃ s ∈ l.ranges, n ∈ s) ↔ n < l.sum := by
rw [← mem_range, ← ranges_flatten, mem_flatten]
