coe_sum — Mathlib

English

The sum of finitely many compactly supported maps yields a function whose evaluation equals the sum of evaluations: for a finite index set s and f_i ∈ C_c(α,β), (∑ i∈s f_i)(x) = ∑ i∈s f_i(x).

Русский

Сумма конечного числа компактно поддерживаемых отображений даёт функцию, чьё значение в точки равно сумме значений: (∑_i f_i)(x) = ∑_i f_i(x).

LaTeX

$$$$ \forall s: Finset\, ι, \forall f: ι \to C_c(\alpha,\beta),\forall x\in\alpha,\ (\sum_{i\in s} f(i))(x) = \sum_{i\in s} (f(i))(x). $$$$

Lean4

@[simp]
theorem coe_sum [AddCommMonoid β] [ContinuousAdd β] {ι : Type*} (s : Finset ι) (f : ι → C_c(α, β)) :
    ⇑(∑ i ∈ s, f i) = ∑ i ∈ s, (f i : α → β) :=
  map_sum coeFnMonoidHom f s

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