Theorems · Definition · measure theory
MeasureTheory.OuterMeasure.trim
{α : Type u_1} → [MeasurableSpace α] → MeasureTheory.OuterMeasure α → MeasureTheory.OuterMeasure αGiven an outer measure m we can forget its value on non-measurable sets, and then consider
m.trim, the unique maximal outer measure less than that function.
- Cited by
- 40 results in Mathlib
- Foundations
- Depth 162 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- MeasurableSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Setproof · cited by 53,352
- MeasurableSpacestatement and proof · cited by 13,106
- MeasurableSetproof · cited by 3,075
- MeasureTheory.OuterMeasurestatement and proof · cited by 287
- MeasurableSet.emptyproof · cited by 58
- MeasureTheory.inducedOuterMeasureproof · cited by 22
- MeasureTheory.OuterMeasure.emptyproof · cited by 5
Cited by45
Results whose statement or proof uses this declaration.
- MeasureTheory.OuterMeasure.trim_eqstatement · cited by 8
- MeasureTheory.Measure.trimmedstatement · cited by 6
- MeasureTheory.OuterMeasure.trim_eq_iInfstatement and proof · cited by 6
- MeasureTheory.OuterMeasure.le_trimstatement · cited by 6
- MeasureTheory.OuterMeasure.exists_measurable_superset_eq_trimstatement · cited by 4
- MeasureTheory.OuterMeasure.le_trim_iffstatement · cited by 4
- MeasureTheory.OuterMeasure.exists_measurable_superset_forall_eq_trimstatement and proof · cited by 3
- MeasureTheory.OuterMeasure.trim_binopstatement and proof · cited by 3
- MeasureTheory.Measure.toOuterMeasure_injectiveproof · cited by 2
- MeasureTheory.measure_eq_trimstatement · cited by 2
- MeasureTheory.OuterMeasure.trim_eq_trim_iffstatement · cited by 2
- MeasureTheory.OuterMeasure.restrict_trimstatement and proof · cited by 1