mathlib

62abfe52 - refactor(measure_theory/measure/hausdorff): move `dimH` to a new file, redefine (#9391)

refactor(measure_theory/measure/hausdorff): move `dimH` to a new file, redefine (#9391) * move definition of the Hausdorff dimension to a new file `topology.metric_space.hausdorff_dimension`; * move `dimH` and related lemmas to the root namespace; * rewrite the definition so that it no longer requires `[measurable_space X] [borel_space X]`; use `rw dimH_def` to get a version using `[measurable_space X]` from the environment; * add `dimH_le`, `set.finite.dimH_zero` and `finset.dimH_zero`; * make `dimH` irreducible.