coe_list_sum — Mathlib

English

The sum over a list commutes with taking Real values componentwise: (l.sum)^\uparrow = (l.map (\uparrow)).sum.

Русский

Сумма списка сохраняет переход к Real по компонентам: (l.sum)^\uparrow = (l.map (\uparrow)).sum.

LaTeX

$$$ (l.sum \\\\text{ : }\\\\mathbb{R}_{\\\\ge 0})^{\\\\uparrow} = (l.\\\\text{map} (\\\\uparrow)).\\\\text{sum}. $$$

Lean4

@[norm_cast]
theorem coe_list_sum (l : List ℝ≥0) : ((l.sum : ℝ≥0) : ℝ) = (l.map (↑)).sum :=
  map_list_sum toRealHom l

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