Commit 2021-09-26 22:22 62abfe52

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.