toReal_sum — Mathlib

English

If every f(a) ≠ ∞ for a ∈ s, then toReal(∑ f(a)) = ∑ toReal(f(a)).

Русский

Если для всех a ∈ s f(a) конечна, то toReal(∑ f(a)) = ∑ toReal(f(a)).

LaTeX

$$$\operatorname{toReal}\left(\sum_{a\in s} f(a)\right) = \sum_{a\in s} \operatorname{toReal}\left(f(a)\right)$$$

Lean4

/-- seeing `ℝ≥0∞` as `Real` does not change their sum, unless one of the `ℝ≥0∞` is infinity -/
theorem toReal_sum {s : Finset α} {f : α → ℝ≥0∞} (hf : ∀ a ∈ s, f a ≠ ∞) :
    ENNReal.toReal (∑ a ∈ s, f a) = ∑ a ∈ s, ENNReal.toReal (f a) :=
  by
  rw [ENNReal.toReal, toNNReal_sum hf, NNReal.coe_sum]
  rfl

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