11.1. Basic construction🔗

A metric space X carries a natural measurable space structure, the Borel σ-algebra, and for each non-negative real number d, a measure, the d-dimensional Hausdorff measure.

Mathlib contains a theory of Hausdorff measure. Here is how it looks:

variable (X : Type*)
  [MetricSpace X] [MeasurableSpace X] [BorelSpace X]
  (d : ℝ)

μH[d] : Measure X#check hausdorffMeasure (X := X) d

Note that d can be any real number but the definition should be regarded as junk when d < 0.

Mathlib also has special notation for the Hausdorff measure. It is available here because we opened the MeasureTheory namespace above:

μH[d] : Measure X#check (μH[d] : Measure X)