coe_finset_sum — Mathlib

English

For a finite set s and f: α → ℝ≥0, the ENNReal image of the NNReal sum equals the sum of ENNReal images: ↑(∑_{a∈s} f(a)) = ∑_{a∈s} (f(a)↑).

Русский

Для конечного множества s и функции f: α → ℝ≥0, ENNReal отображает сумму NNReal так же, как сумма ENNReal отображений: ↑(∑ f(a)) = ∑ ↑(f(a)).

LaTeX

$$$$\\uparrow\\left(\\sum_{a\\in s} f(a)\\right) = \\sum_{a\\in s} (f(a) : \\mathbb{R}_{\\ge 0}^{\\infty})$$$$

Lean4

@[simp, norm_cast]
theorem coe_finset_sum {s : Finset α} {f : α → ℝ≥0} : ↑(∑ a ∈ s, f a) = ∑ a ∈ s, (f a : ℝ≥0∞) :=
  map_sum ofNNRealHom f s

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