ofReal_sum_of_nonneg — Mathlib

English

For a finite set s and nonnegative real-valued f, ofReal(sum f) equals sum of ofReal(f).

Русский

Для конечного множества s и неотрицательных действительных f: ofReal(∑ f) = ∑ ofReal(f).

LaTeX

$$$\operatorname{ofReal}\left(\sum_{i\in s} f(i)\right) = \sum_{i\in s} \operatorname{ofReal}\left(f(i)\right)$$$

Lean4

theorem ofReal_sum_of_nonneg {s : Finset α} {f : α → ℝ} (hf : ∀ i, i ∈ s → 0 ≤ f i) :
    ENNReal.ofReal (∑ i ∈ s, f i) = ∑ i ∈ s, ENNReal.ofReal (f i) :=
  by
  simp_rw [ENNReal.ofReal, ← coe_finset_sum, coe_inj]
  exact Real.toNNReal_sum_of_nonneg hf

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