finset_sum_apply — Mathlib

English

For finite I, κ i, and a, the value of the sum kernel at a and s equals the sum over i of κ i a at s.

Русский

Для конечного множества I и κ i, и для a аналогично: значение суммы ядра на a и s равно сумме κ i a на s.

LaTeX

$$$$(\sum_{i\in I} \kappa_i) a \, s = \sum_{i\in I} (\kappa_i a) \, s$$$$

Lean4

theorem finset_sum_apply (I : Finset ι) (κ : ι → Kernel α β) (a : α) : (∑ i ∈ I, κ i) a = ∑ i ∈ I, κ i a := by
  rw [coe_finset_sum, Finset.sum_apply]

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