dfinsuppSumAddHom_apply — Mathlib

English

For every r in R, applying the big sumAddHom to f and g and then evaluating at r equals the sumAddHom evaluated at the composition with eval r: (sumAddHom g f) r = sumAddHom (i ↦ (eval r) ∘ (g i)) f.

Русский

Для каждого элемента r из R применение большой суммы sumAddHom к f и g и последующая подстановочная оценка в r равны сумме по i от (eval r) ∘ (g i) к f.

LaTeX

$$$ (\mathrm{sumAddHom}\, g\, f)\, r = \mathrm{sumAddHom}\bigl(\lambda i. (\mathrm{eval}\, r) \circ (g i)\bigr)\, f $$$

Lean4

theorem dfinsuppSumAddHom_apply [AddZeroClass R] [AddCommMonoid S] [∀ i, AddZeroClass (β i)] (f : Π₀ i, β i)
    (g : ∀ i, β i →+ R →+ S) (r : R) : (sumAddHom g f) r = sumAddHom (fun i => (eval r).comp (g i)) f :=
  map_dfinsuppSumAddHom (eval r) f g

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