Commit 2026-08-12 18:02 b3eab835

feat(Topology/MetricSpace): differentiable maps do not increase Hausdorff dimension (#41799) Add the Luzin N property of differentiable maps and deduce that differentiable maps do not increase Hausdorff dimension, over any nontrivially normed field with no finite-dimensionality or separability assumptions:

• MeasureTheory.Measure.isSeparable_of_hausdorffMeasure_ne_top: a set with μH[d] s ≠ ∞ is separable
• DifferentiableOn.hausdorffMeasure_image_eq_zero: if f is differentiable on t and μH[d] t = 0 for some 0 ≤ d, then μH[d] (f '' t) = 0
• DifferentiableOn.dimH_image_le: dimH (f '' t) ≤ dimH t, as a corollary of the Luzin N property
• Differentiable.dimH_range_le, DifferentiableOn.dense_compl_image_of_dimH_lt_finrank, Differentiable.dense_compl_range_of_finrank_lt_finrank: differentiable versions of the Sard-type corollaries; dense_compl_of_dimH_lt_finrank and these corollaries also drop FiniteDimensional instance assumptions that already follow from their hypotheses This resolves the TODO on ContDiffOn.dimH_image_le: the Convex ℝ s hypothesis is not needed. The four ContDiff/ContDiffOn lemmas (ContDiffOn.dimH_image_le, ContDiff.dimH_range_le, ContDiffOn.dense_compl_image_of_dimH_lt_finrank, ContDiff.dense_compl_range_of_finrank_lt_finrank) are deprecated in favour of the Differentiable versions.