coe_multiset_sum — Mathlib

English

The Real embedding preserves the sum of a multiset: (s.sum f)^\uparrow = (s.map (\uparrow)).sum.

Русский

Преобразование Real сохраняет сумму второго типа над мультимножество: (s.sum f)^\uparrow = (s.map (\uparrow)).sum.

LaTeX

$$$ (s.sum f \\\\text{ : }\\\\mathbb{R}_{\\\\ge 0})^{\\\\uparrow} = (s.map (\\\\uparrow)).\\\\text{sum}. $$$

Lean4

@[norm_cast]
theorem coe_multiset_sum (s : Multiset ℝ≥0) : ((s.sum : ℝ≥0) : ℝ) = (s.map (↑)).sum :=
  map_multiset_sum toRealHom s

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