mathlib

571e13ca - feat(measure_theory/measure/hausdorff): the 1-measure of a segment is its length (#18981)

feat(measure_theory/measure/hausdorff): the 1-measure of a segment is its length (#18981) Or in other words, length along a line segment is the distance between its endpoints. This also proves that the `d`-dimensional Hausdorff measure scales by a factor of `‖r‖₊ ^ d` when the set is scaled by `r` (both linearly and affinely), and that it is translation-invariant.