Commit 2021-08-31 15:40 603a6066

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.