setToFun_finset_sum — Mathlib

English

Variant form: equality holds for sum over a Finset with the same integrability hypothesis as above.

Русский

Вариант формы равенства для суммы по Finset с теми же условиями интегрируемости.

LaTeX

$$$\forall s: Finset I, \forall (f : I \to α \to E), (\forall i ∈ s, Integrable (f i) μ) \Rightarrow (setToFun μ T hT (\sum i ∈ s, f i) = \sum i ∈ s, setToFun μ T hT (f i))$$$

Lean4

theorem setToFun_finset_sum (hT : DominatedFinMeasAdditive μ T C) {ι} (s : Finset ι) {f : ι → α → E}
    (hf : ∀ i ∈ s, Integrable (f i) μ) : (setToFun μ T hT fun a => ∑ i ∈ s, f i a) = ∑ i ∈ s, setToFun μ T hT (f i) :=
  by convert setToFun_finset_sum' hT s hf with a; simp

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