Theorems · Theorem · measure theory
MeasureTheory.hausdorffMeasure_real
MeasureTheory.Measure.hausdorffMeasure 1 = MeasureTheory.volume
In the space ℝ, the Hausdorff measure coincides exactly with the Lebesgue measure.
- Defined in
- Mathlib.MeasureTheory.Measure.Hausdorff
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 250 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites13
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Realstatement and proof · cited by 25,697
- MeasureTheory.Measurestatement and proof · cited by 10,939
- Nat.cast_oneproof · cited by 2,501
- MeasureTheory.MeasureSpace.volumestatement and proof · cited by 1,323
- MeasureTheory.Measure.mapproof · cited by 858
- MeasureTheory.MeasurePreserving.map_eqproof · cited by 72
- MeasureTheory.Measure.hausdorffMeasurestatement and proof · cited by 71
- MeasurableEquiv.funUniqueproof · cited by 10
- MeasureTheory.volume_preserving_funUniqueproof · cited by 4
- MeasureTheory.hausdorffMeasure_pi_realproof · cited by 3
- Fintype.card_unitproof · cited by 3
Cited by2
Results whose statement or proof uses this declaration.
- MeasureTheory.hausdorffMeasure_affineSegmentproof · cited by 1
- MeasureTheory.hausdorffMeasure_smul_right_imageproof · cited by 1