Theorems · Definition · measure theory

MeasureTheory.Measure.trim

{α : Type u_1} → {m m0 : MeasurableSpace α} → MeasureTheory.Measure α → m ≤ m0 → MeasureTheory.Measure α

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 any m ≤ m0. Since measures in mathlib have to be trimmed to the measurable space, μ itself cannot be a measure on m, hence the definition of μ.trim hm. This notion is related to OuterMeasure.trim, see the lemma toOuterMeasure_trim_eq_trim_toOuterMeasure.

Defined in

Mathlib.MeasureTheory.Measure.Trim

Cited by

286 results in Mathlib

Foundations

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