Theorems · Theorem · measure theory

MeasureTheory.IntegrableOn.restrict_toMeasurable

∀ {α : Type u_1} {ε' : Type u_4} {mα : MeasurableSpace α} {s : Set α} {μ : MeasureTheory.Measure α}
  [inst : TopologicalSpace ε'] [inst_1 : ESeminormedAddMonoid ε'] {f : α → ε'},
  MeasureTheory.IntegrableOn f s μ → (∀ x ∈ s, ‖f x‖ₑ ≠ 0) → μ.restrict (MeasureTheory.toMeasurable μ s) = μ.restrict s

If a function is integrable on a set s and nonzero there, then the measurable hull of s is well behaved: the restriction of the measure to toMeasurable μ s coincides with its restriction to s.

Defined in

Mathlib.MeasureTheory.Integral.IntegrableOn

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceESeminormedAddMonoid