Theorems · Theorem · measure theory

MeasureTheory.SimpleFunc.map_setToSimpleFunc

∀ {α : Type u_1} {F : Type u_3} {F' : Type u_4} {G : Type u_5} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F]
  [inst_2 : NormedAddCommGroup F'] [inst_3 : NormedSpace ℝ F'] [inst_4 : NormedAddCommGroup G] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} (T : Set α → F →L[ℝ] F'),
  MeasureTheory.FinMeasAdditive μ T →
    ∀ {f : MeasureTheory.SimpleFunc α G},
      MeasureTheory.Integrable (⇑f) μ →
        ∀ {g : G → F},
          g 0 = 0 →
            MeasureTheory.SimpleFunc.setToSimpleFunc T (MeasureTheory.SimpleFunc.map g f) =
              ∑ x ∈ f.range, (T (⇑f ⁻¹' {x})) (g x)

Defined in

Mathlib.MeasureTheory.Integral.FinMeasAdditive

Cited by

6 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpaceNormedAddCommGroup