dfinsuppSum_apply — Mathlib

English

Applying the sum of linear maps represented by a dependent finitely supported function to a vector b equals the sum over the indices of applying each map to b.

Русский

Применение суммы линейных отображений, заданной через dfinsupp, к вектору b эквивалентно сумме по индексам от применения каждого отображения к b.

LaTeX

$$$ (t.sum g)\, b = t.sum (\lambda i d, g\, i\, d\, b)$$$

Lean4

@[simp]
theorem dfinsuppSum_apply (t : Π₀ i, γ i) (g : ∀ i, γ i → M →ₛₗ[σ₁₂] M₂) (b : M) :
    (t.sum g) b = t.sum fun i d => g i d b :=
  sum_apply _ _ _

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