finset_sum_apply — Mathlib

English

Applying a Finset-sum of measures to a set s equals the Finset-sum of the evaluations: (I.sum i μ_i)(s) = ∑ i μ_i(s).

Русский

Применение суммы по Finset к множеству s равно сумме значений: (I.sum i μ_i)(s) = ∑ i μ_i(s).

LaTeX

$$$\bigl(\sum i\in I, μ_i\bigr)(s) = \sum i\in I, μ_i(s).$$$

Lean4

theorem finset_sum_apply {m : MeasurableSpace α} (I : Finset ι) (μ : ι → Measure α) (s : Set α) :
    (∑ i ∈ I, μ i) s = ∑ i ∈ I, μ i s := by rw [coe_finset_sum, Finset.sum_apply]

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