hausdorffMeasure_segment — Mathlib

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]

Похожие утверждения