coe_sum — Mathlib

English

For any finite set, the coercion commutes with finite sums: the underlying function of the sum equals the sum of the underlying functions.

Русский

Для любого конечного множества сумма через коэрцию сохраняется: базовая функция суммы равна сумме базовых функций.

LaTeX

$$$\\text{coe\_sum }(s)(f)$$$

Lean4

@[simp]
theorem coe_sum {ι : Type*} (s : Finset ι) (f : ι → C(X, R)₀) : ⇑(s.sum f) = s.sum (fun i => ⇑(f i)) :=
  map_sum coeFnAddMonoidHom f s

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