dimH_subsingleton — Mathlib

English

If s is a subsingleton, then its Hausdorff dimension is zero.

Русский

Если множество является одиночным или пустым, его размерность Хаусдорфа равна нулю.

LaTeX

$$dimH(s) = 0 \quad \text{if} \quad s \text{ is subsingleton}$$

Lean4

theorem dimH_subsingleton {s : Set X} (h : s.Subsingleton) : dimH s = 0 :=
  by
  borelize X
  apply le_antisymm _ (zero_le _)
  refine dimH_le_of_hausdorffMeasure_ne_top ?_
  exact ((hausdorffMeasure_le_one_of_subsingleton h le_rfl).trans_lt ENNReal.one_lt_top).ne

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