Theorems · Inductive type · measure theory
MeasureTheory.OuterMeasure
Type u_2 → Type u_2
An outer measure is a countably subadditive monotone function that sends ∅ to 0.
- Defined in
- Mathlib.MeasureTheory.OuterMeasure.Defs
- Cited by
- 287 results in Mathlib
- Foundations
- Depth 0 from the axioms, rests on 1 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites0
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Nothing in Mathlib beyond the foundations.
Cited by327
Results whose statement or proof uses this declaration.
- MeasureTheory.Measure.extproof · cited by 308
- MeasureTheory.Measure.toOuterMeasurestatement · cited by 75
- MeasureTheory.OuterMeasure.trimstatement and proof · cited by 40
- MeasureTheory.OuterMeasure.caratheodorystatement and proof · cited by 37
- MeasureTheory.OuterMeasure.monostatement and proof · cited by 36
- MeasureTheory.Measure.restrict_apply'proof · cited by 32
- MeasureTheory.OuterMeasure.mapstatement and proof · cited by 30
- PMF.toOuterMeasurestatement · cited by 26
- MeasureTheory.Content.outerMeasurestatement · cited by 24
- MeasureTheory.OuterMeasure.extstatement and proof · cited by 24
- MeasureTheory.inducedOuterMeasurestatement · cited by 22
- MeasureTheory.OuterMeasure.comapstatement and proof · cited by 22
Showing the 200 most cited of 327.