coe_sum — Mathlib

English

Sum of normed group homs corresponds to pointwise sum of their values.

Русский

Сумма NormedAddGroupHom соответствует по точечной сумме их значений.

LaTeX

$$$$ \displaystyle \forall s \ (f_i)_{i \in s}: \; \Big( \sum i \in s, f_i \Big) = \sum i \in s, f_i $$$$

Lean4

@[simp]
theorem coe_sum {ι : Type*} (s : Finset ι) (f : ι → NormedAddGroupHom V₁ V₂) :
    ⇑(∑ i ∈ s, f i) = ∑ i ∈ s, (f i : V₁ → V₂) :=
  map_sum coeAddHom f s

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