Zero-dimensional Hausdorff measure #
Zero-dimensional Hausdorff measure μH[0] is counting measure on every extended metric Borel
space: each singleton has measure 1, so finite sets are counted by finite additivity, and an
infinite set contains finite subsets of every cardinality, so its measure is ∞.
@[simp]
theorem
TauCeti.hausdorffMeasure_zero_eq_count
{X : Type u_1}
[EMetricSpace X]
[MeasurableSpace X]
[BorelSpace X]
:
Zero-dimensional Hausdorff measure is counting measure. Thus the normalized Euclidean
Hausdorff measure μHE[0] also counts points, by euclideanHausdorffMeasure_zero.