finset_sum_apply' — Mathlib

English

For I, κ, a, s, the equality from the previous lemma holds with a set argument s on the right.

Русский

Для I, κ, a, s равенство из предыдущей леммы сохраняется для аргумента 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 : α) (s : Set β) :
    (∑ i ∈ I, κ i) a s = ∑ i ∈ I, κ i a s := by rw [finset_sum_apply, Measure.finset_sum_apply]

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