Theorems · Theorem · measure theory

MeasureTheory.setToFun_finsetSum_measure

∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {f : α → E} {ι : Type u_7}
  {s : Finset ι} (hs : s.Nonempty) {μ : ι → MeasureTheory.Measure α} {T : ι → Set α → E →L[ℝ] F} {C : ι → ℝ}
  (hTs : ∀ (i : ι), MeasureTheory.DominatedFinMeasAdditive (μ i) (T i) (C i)),
  (∀ i ∈ s, MeasureTheory.Integrable f (μ i)) →
    MeasureTheory.setToFun (∑ i ∈ s, μ i) (∑ i ∈ s, T i) ⋯ f = ∑ i ∈ s, MeasureTheory.setToFun (μ i) (T i) ⋯ f

Defined in

Mathlib.MeasureTheory.Integral.SetToL1

Cited by

0 results in Mathlib

Foundations

Depth 248 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpace