coe_sum — Mathlib

English

The Real embedding respects Finset sums: sum over s of f i, when coerced to Real, equals the Real sum of coerced values.

Русский

Преобразование Real сохраняет сумму по конечному множеству: сумма по s f i при приведении к Real равна сумме приведённых значений.

LaTeX

$$$\\\\sum i \\\\in s, f i)^{\\\\uparrow} = \\\\(\\\\sum i \\\\in s, (f i)^{\\\\uparrow}.$$$

Lean4

@[simp, norm_cast]
theorem coe_sum (s : Finset ι) (f : ι → ℝ≥0) : ∑ i ∈ s, f i = ∑ i ∈ s, (f i : ℝ) :=
  map_sum toRealHom _ _

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