Theorems · Theorem · measure theory

MeasureTheory.SimpleFunc.lintegral_eq_of_subset

∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : MeasureTheory.SimpleFunc α ENNReal)
  {s : Finset ENNReal},
  (∀ (x : α), f x ≠ 0 → μ (⇑f ⁻¹' {f x}) ≠ 0 → f x ∈ s) → f.lintegral μ = ∑ x ∈ s, x * μ (⇑f ⁻¹' {x})

Defined in

Mathlib.MeasureTheory.Function.SimpleFunc

Cited by

3 results in Mathlib

Foundations

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