hausdorffMeasure_of_finrank_lt — Mathlib

English

If E is finite-dimensional and d exceeds finrank E, then the Hausdorff measure μ_H^d(E) is zero.

Русский

Если E конечномерно, и d больше чем размерность E, то мера Хаусдорфа μ_H^d(E) равна нулю.

LaTeX

$$(μ_H[d])(E) = 0$$

Lean4

theorem hausdorffMeasure_of_finrank_lt [MeasurableSpace E] [BorelSpace E] {d : ℝ} (hd : finrank ℝ E < d) :
    (μH[d] : Measure E) = 0 := by
  lift d to ℝ≥0 using (Nat.cast_nonneg _).trans hd.le
  rw [← measure_univ_eq_zero]
  apply hausdorffMeasure_of_dimH_lt
  rw [dimH_univ_eq_finrank]
  exact mod_cast hd

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