Theorems · Definition · measure theory
MeasureTheory.OuterMeasure.toMeasure
{α : Type u_1} →
[ms : MeasurableSpace α] → (m : MeasureTheory.OuterMeasure α) → ms ≤ m.caratheodory → MeasureTheory.Measure αObtain a measure by giving an outer measure where all sets in the σ-algebra are Carathéodory measurable.
- Cited by
- 11 results in Mathlib
- Foundations
- Depth 169 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.
Cites9
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
- MeasureTheory.Measurestatement · cited by 10,939
- MeasurableSetproof · cited by 3,075
- MeasureTheory.OuterMeasurestatement and proof · cited by 287
- MeasureTheory.OuterMeasure.caratheodorystatement and proof · cited by 37
- MeasureTheory.OuterMeasure.emptyproof · cited by 5
- MeasureTheory.Measure.ofMeasurableproof · cited by 4
Cited by20
Results whose statement or proof uses this declaration.
- MeasureTheory.Measure.trimproof · cited by 286
- MeasureTheory.Measure.diracproof · cited by 210
- MeasureTheory.Measure.sumproof · cited by 121
- MeasureTheory.Measure.comapproof · cited by 96
- PMF.toMeasureproof · cited by 34
- MeasureTheory.Content.measureproof · cited by 10
- MeasureTheory.Measure.mkMetricproof · cited by 10
- MeasureTheory.toMeasure_applystatement · cited by 10
- MeasureTheory.le_toMeasure_applystatement · cited by 8
- MeasureTheory.Measure.liftLinearproof · cited by 5
- MeasureTheory.OuterMeasure.toMeasure_zerostatement · cited by 3
- MeasureTheory.toOuterMeasure_toMeasurestatement · cited by 3