Theorems · Theorem · measure theory

MeasureTheory.SimpleFunc.setToSimpleFunc_eq_sum_filter

∀ {α : Type u_1} {F : Type u_3} {F' : Type u_4} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F]
  [inst_2 : NormedAddCommGroup F'] [inst_3 : NormedSpace ℝ F'] [inst_4 : DecidablePred fun x => x ≠ 0]
  {m : MeasurableSpace α} (T : Set α → F →L[ℝ] F') (f : MeasureTheory.SimpleFunc α F),
  MeasureTheory.SimpleFunc.setToSimpleFunc T f = ∑ x ∈ f.range with x ≠ 0, (T (⇑f ⁻¹' {x})) x

Defined in

Mathlib.MeasureTheory.Integral.FinMeasAdditive

Cited by

4 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpaceDecidablePred