hausdorffMeasure_real — Mathlib

English

On the real line, the Hausdorff measure of dimension 1 equals the Lebesgue volume.

Русский

На вещественной прямой мера Хаусдорфа размерности 1 равна Lebesgue-объему.

LaTeX

$$$\mu_H^{1} = \mathrm{volume}$ on $\mathbb{R}$$$

Lean4

/-- In the space `ℝ`, the Hausdorff measure coincides exactly with the Lebesgue measure. -/
@[simp]
theorem hausdorffMeasure_real : (μH[1] : Measure ℝ) = volume := by
  rw [← (volume_preserving_funUnique Unit ℝ).map_eq, ← (hausdorffMeasure_measurePreserving_funUnique Unit ℝ 1).map_eq, ←
    hausdorffMeasure_pi_real, Fintype.card_unit, Nat.cast_one]

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