hausdorffMeasure_of_dimH_lt — Mathlib

English

If μH[d] s ≠ 0 and μH[d] s ≠ ∞, then dimH s = d.

Русский

Если μ_H^d(s) ≠ 0 и μ_H^d(s) ≠ ∞, то dim_H(s) = d.

LaTeX

$$μ_H[d](s) ≠ 0 \land μ_H[d](s) ≠ ∞ \Rightarrow dimH(s) = d$$

Lean4

theorem hausdorffMeasure_of_dimH_lt {s : Set X} {d : ℝ≥0} (h : dimH s < d) : μH[d] s = 0 :=
  by
  rw [dimH_def] at h
  rcases ENNReal.lt_iff_exists_nnreal_btwn.1 h with ⟨d', hsd', hd'd⟩
  rw [ENNReal.coe_lt_coe, ← NNReal.coe_lt_coe] at hd'd
  exact (hausdorffMeasure_zero_or_top hd'd s).resolve_right fun h₂ => hsd'.not_ge <| le_iSup₂ (α := ℝ≥0∞) d' h₂

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