English
The 1-dimensional Hausdorff measure of a segment equals its Euclidean distance: μ_H[1](affineSegment ℝ x y) = edist x y.
Русский
1-мерная Хаусдорфова мера отрезка равна евклидову расстоянию между его концами: μ_H^1(affineSegment ℝ x y) = edist x y.
LaTeX
$$$\mu\!\_{H}^{1}(affineSegment \\mathbb{R} \\; x \\; y) = \mathrm{edist}(x,y)$$$
Lean4
/-- The measure of a segment is the distance between its endpoints. -/
@[simp]
theorem hausdorffMeasure_segment {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E]
(x y : E) : μH[1] (segment ℝ x y) = edist x y := by rw [← affineSegment_eq_segment, hausdorffMeasure_affineSegment]