mathlib

603a6066 - feat(measure_theory/hausdorff_measure): dimH and Hölder/Lipschitz maps (#8361)

feat(measure_theory/hausdorff_measure): dimH and Hölder/Lipschitz maps (#8361) * expand module docs; * prove that a Lipschitz continuous map does not increase Hausdorff measure and Hausdorff dimension of sets; * prove similar lemmas about Hölder continuous and antilipschitz maps; * add convenience lemmas for some bundled types and for `Cⁿ` smooth maps; * Hausdorff dimension of `ℝⁿ` equals `n`; * prove a baby version of Sard's theorem: if `f : E → F` is a `C¹` smooth map between normed vector spaces such that `finrank ℝ E < finrank ℝ F`, then `(range f)ᶜ` is dense.