English
If none of the terms are ∞, then the sum after applying the NNReal map equals the NNReal-sum of the NNReal values: toNNReal(∑ f(a)) = ∑ toNNReal(f(a)).
Русский
Если ни один из членов не равен ∞, то отображение в NNReal preserves сумму: toNNReal(∑ f(a)) = ∑ toNNReal(f(a)).
LaTeX
$$$\operatorname{toNNReal}\left(\sum_{a\in s} f(a)\right) = \sum_{a\in s} \operatorname{toNNReal}\left(f(a)\right)$$$
Lean4
/-- Seeing `ℝ≥0∞` as `ℝ≥0` does not change their sum, unless one of the `ℝ≥0∞` is
infinity -/
theorem toNNReal_sum {s : Finset α} {f : α → ℝ≥0∞} (hf : ∀ a ∈ s, f a ≠ ∞) :
ENNReal.toNNReal (∑ a ∈ s, f a) = ∑ a ∈ s, ENNReal.toNNReal (f a) :=
by
rw [← coe_inj, coe_toNNReal, coe_finset_sum, sum_congr rfl]
· intro x hx
exact (coe_toNNReal (hf x hx)).symm
· exact sum_ne_top.2 hf
