Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-07-17 16:20 8139d7eb

View on Github →

feat(measure_theory/hausdorff_measure): μH and dimH of a subsingleton (#8347)

Estimated changes

Modified src/measure_theory/hausdorff_measure.lean

added theorem measure_theory.dimH_empty

added theorem measure_theory.dimH_singleton

added theorem measure_theory.dimH_subsingleton

Modified src/measure_theory/measure_space.lean

added theorem measure_theory.measure_subsingleton