length_sum_le — Mathlib

English

For f : ι → Interval α and finite s ⊆ ι, the length of the sum is bounded by the sum of lengths: (sum f i).length ≤ sum (f i).length.

Русский

Для f : ι → Interval α и конечного множества s ⊆ ι длина суммы ограничена суммой длин: (sum f i).length ≤ sum (f i).length.

LaTeX

$$$ (\sum i \in s, f(i)).length \le \sum i \in s, (f(i)).length $$$

Lean4

theorem length_sum_le (f : ι → Interval α) (s : Finset ι) : (∑ i ∈ s, f i).length ≤ ∑ i ∈ s, (f i).length :=
  Finset.le_sum_of_subadditive _ length_zero length_add_le _ _

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