sum_apply — Mathlib

English

Applying a finite sum of normed group homs to a vector equals the finite sum of applications.

Русский

Применение конечной суммы NormedAddGroupHom к вектору равняется конченой сумме применений.

LaTeX

$$$$ \left( \sum i \in s, f_i \right) v = \sum i \in s, f_i(v) $$$$

Lean4

theorem sum_apply {ι : Type*} (s : Finset ι) (f : ι → NormedAddGroupHom V₁ V₂) (v : V₁) :
    (∑ i ∈ s, f i) v = ∑ i ∈ s, f i v := by simp only [coe_sum, Finset.sum_apply]

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