length_sum — Mathlib

English

The length distributes over finite sums: (sum f i).length = sum (f i).length over a finite index set.

Русский

Длина распределяется по конечной сумме: (sum f(i)).length = sum (f(i)).length.

LaTeX

$$$ \left( \sum_{i \in s} f(i) \right).length = \sum_{i \in s} (f(i)).length $$$

Lean4

@[simp]
theorem length_sum (f : ι → NonemptyInterval α) (s : Finset ι) : (∑ i ∈ s, f i).length = ∑ i ∈ s, (f i).length :=
  map_sum (⟨⟨length, length_zero⟩, length_add⟩ : NonemptyInterval α →+ α) _ _

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