Restriction of a measure to a sub-σ-algebra #
Main definitions #
MeasureTheory.Measure.trim: restriction of a measure to a sub-sigma algebra.
Restriction of a measure to a sub-σ-algebra.
It is common to see a measure
μ on a measurable space structure
m0 as being also a measure on
m ≤ m0. Since measures in mathlib have to be trimmed to the measurable space,
cannot be a measure on
m, hence the definition of