sum_hom — Mathlib

English

For a finite index set ι, a family of morphisms f: ι → X ⟶ Y, and a finite set s, the hom of the sum equals the sum of the homs: (s.sum f).hom = ∑_{i∈s} (f i).hom.

Русский

Для конечной индексной множества ι и семейства морфизмов f: ι → X ⟶ Y верно, что hom от суммы равен сумме hom-ов: (s.sum f).hom = ∑_{i∈s} (f i).hom.

LaTeX

$$$(s.\mathrm{sum}\ f).\mathrm{hom} = \sum_{i\in s} (f\,i).\mathrm{hom}$$$

Lean4

@[simp]
theorem sum_hom {ι : Type*} (f : ι → (X ⟶ Y)) (s : Finset ι) : (s.sum f).hom = s.sum fun i => (f i).hom :=
  (forget V G).map_sum f s

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