Theorems · Theorem · measure theory
MeasureTheory.Measure.nullSingletonClass_hausdorff
∀ (X : Type u_2) [inst : EMetricSpace X] [inst_1 : MeasurableSpace X] [inst_2 : BorelSpace X] {d : ℝ},
0 < d → MeasureTheory.NullSingletonClass (MeasureTheory.Measure.hausdorffMeasure d)- Defined in
- Mathlib.MeasureTheory.Measure.Hausdorff
- Cited by
- 5 results in Mathlib
- Foundations
- Depth 202 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites20
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement and proof · cited by 25,697
- MeasurableSpacestatement and proof · cited by 13,106
- ENNRealproof · cited by 9,879
- SummationFilter.unconditionalproof · cited by 2,068
- BorelSpacestatement and proof · cited by 1,602
- tsumproof · cited by 1,148
- iSup_congr_Propproof · cited by 247
- EMetricSpacestatement and proof · cited by 242
- MeasureTheory.NullSingletonClassstatement · cited by 125
- nonpos_iff_eq_zeroproof · cited by 100
- iSup₂_leproof · cited by 96
- Set.subset_iUnionproof · cited by 81
Cited by5
Results whose statement or proof uses this declaration.
- HolderOnWith.hausdorffMeasure_image_leproof · cited by 2
- AntilipschitzWith.hausdorffMeasure_preimage_leproof · cited by 2
- MeasureTheory.Measure.hausdorffMeasure_le_one_of_subsingletonproof · cited by 1
- MeasureTheory.hausdorffMeasure_smul_right_imageproof · cited by 1
- MeasureTheory.Measure.noAtoms_hausdorffproof · cited by 0