hausdorffMeasure_prod_real — Mathlib

English

In ℝ×ℝ, the Hausdorff measure with exponent 2 equals the Lebesgue measure (volume).

Русский

В пространстве ℝ×ℝ мера Хаара с размерностью 2 совпадает с объёмом (ламбда-мерой).

LaTeX

$$$\\mu_H^{[2]}(\\mathbb{R} \\times \\mathbb{R}) = \\mathrm{volume}$$$

Lean4

/-- In the space `ℝ × ℝ`, the Hausdorff measure coincides exactly with the Lebesgue measure. -/
@[simp]
theorem hausdorffMeasure_prod_real : (μH[2] : Measure (ℝ × ℝ)) = volume := by
  rw [← (volume_preserving_piFinTwo fun _ => ℝ).map_eq, ←
    (hausdorffMeasure_measurePreserving_piFinTwo (fun _ => ℝ) _).map_eq, ← hausdorffMeasure_pi_real, Fintype.card_fin,
    Nat.cast_two]

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