hausdorffMeasure_of_lt_dimH — Mathlib

English

If the bound d is less than the Hausdorff dimension of s, then the d-dimensional Hausdorff measure is infinite.

Русский

Если граница d меньше размерности Хаусдорфа множества s, то μ_H^d(s) = ∞.

LaTeX

$$μ_H[d](s) = ∞ \quad \text{whenever} \quad d < dim_H(s)$$

Lean4

theorem hausdorffMeasure_of_lt_dimH {s : Set X} {d : ℝ≥0} (h : ↑d < dimH s) : μH[d] s = ∞ :=
  by
  simp only [dimH_def, lt_iSup_iff] at h
  rcases h with ⟨d', hsd', hdd'⟩
  rw [ENNReal.coe_lt_coe, ← NNReal.coe_lt_coe] at hdd'
  exact top_unique (hsd' ▸ hausdorffMeasure_mono hdd'.le _)

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