hausdorffMeasure_affineSegment — Mathlib

English

In the same setting, the 1-dimensional Hausdorff measure of the image of s under the lineMap equals the line distance times the measure of s: μ_H[1](AffineMap.lineMap x y '' s) = d(x,y) · μ_H[1] s.

Русский

В той же постановке 1-мерная Хаусдорфова мера образа множества s по отображению lineMap равна расстоянию между концами x,y, умноженному на меру s.

LaTeX

$$$\mu\!\_{H}^{1}(AffineMap.lineMap x y '' s) = d(x,y) \cdot \mu\!\_{H}^{1}(s)$$$

Lean4

/-- The measure of a segment is the distance between its endpoints. -/
@[simp]
theorem hausdorffMeasure_affineSegment (x y : P) : μH[1] (affineSegment ℝ x y) = edist x y :=
  by
  rw [affineSegment, hausdorffMeasure_lineMap_image, hausdorffMeasure_real, Real.volume_Icc, sub_zero,
    ENNReal.ofReal_one, ← Algebra.algebraMap_eq_smul_one]
  exact (edist_nndist _ _).symm

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