Theorems · Theorem · measure theory

MeasureTheory.Measure.restrict_apply

∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  MeasurableSet t → (μ.restrict s) t = μ (t ∩ s)

If t is a measurable set, then the measure of t with respect to the restriction of the measure to s equals the outer measure of t ∩ s. An alternate version requiring that s be measurable instead of t exists as Measure.restrict_apply'.

Defined in

Mathlib.MeasureTheory.Measure.Restrict

Cited by

159 results in Mathlib

Foundations

Depth 195 from the axioms, rests on 4,764 definitions · uses propext, Classical.choice, Quot.sound