English
Let f: α → ℝ≥0 be a nonnegative function. Then the real sum of f (via the embedding of ℝ≥0 into ℝ) equals the sum of the embedded values: the real value of the NNReal sum is the same as summing the real embeddings.
Русский
Пусть f: α → ℝ≥0. Тогда сумма f в ℝ≥0, приведённая к ℝ, равна сумме по α считываемых значений в ℝ: сумма значений f в ℝ≥0 после отображения в ℝ равна сумме f(a) в ℝ.
LaTeX
$$$ \\uparrow\\Big(\\sum\\!\\!_L a\\, f(a)\\Big) = \\sum\\!\\!_L a\\,(f(a)\\;:\\;\\mathbb{R}) $$$
Lean4
@[norm_cast]
theorem coe_tsum {f : α → ℝ≥0} : ↑(∑'[L] a, f a) = ∑'[L] a, (f a : ℝ) :=
Function.LeftInverse.map_tsum (g := NNReal.toRealHom) f NNReal.continuous_coe continuous_real_toNNReal
(fun x ↦ by simp)
