Theorems · Theorem · measure theory

MeasureTheory.integral_indicator

∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {f : X → E} {s : Set X} {μ : MeasureTheory.Measure X},
  MeasurableSet s → ∫ (x : X), s.indicator f x ∂μ = ∫ (x : X) in s, f x ∂μ

For a function f and a measurable set s, the integral of indicator s f over the whole space is equal to ∫ x in s, f x ∂μ defined as ∫ x, f x ∂(μ.restrict s).

Defined in

Mathlib.MeasureTheory.Integral.Bochner.Set

Cited by

38 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpace