α : Type u_1
β : Type ?u.204043
a b c d : ℝ≥0∞
r p q : ℝ≥0
s : Finset α
f : α → ℝ
hf : ∀ (i : α), i ∈ s → 0 ≤ f i
⊢ Real.toNNReal (∑ i in s, f i) = ∑ a in s, Real.toNNReal (f a)
α : Type u_1
β : Type ?u.204043
a b c d : ℝ≥0∞
r p q : ℝ≥0
s : Finset α
f : α → ℝ
hf : ∀ (i : α), i ∈ s → 0 ≤ f i
⊢ ENNReal.ofReal (∑ i in s, f i) = ∑ i in s, ENNReal.ofReal (f i)
simp_rw [ENNReal.ofReal, ← coe_finset_sum, coe_eq_coe]
no goals
α : Type u_1
β : Type ?u.204043
a b c d : ℝ≥0∞
r p q : ℝ≥0
s : Finset α
f : α → ℝ
hf : ∀ (i : α), i ∈ s → 0 ≤ f i
⊢ Real.toNNReal (∑ i in s, f i) = ∑ a in s, Real.toNNReal (f a)
exact Real.toNNReal_sum_of_nonneg hf