one_le_hausdorffMeasure_zero_of_nonempty

English

If a subset s of X is nonempty, then its 0-dimensional Hausdorff measure is at least 1.

Русский

Для непустого подмножества s пространства X выполняется: \mu_H^0(s) \ge 1.

LaTeX

$$$s \neq \varnothing \Rightarrow 1 \le \mu_H^{0}(s)$$$

Lean4

theorem one_le_hausdorffMeasure_zero_of_nonempty {s : Set X} (h : s.Nonempty) : 1 ≤ μH[0] s :=
  by
  rcases h with ⟨x, hx⟩
  calc
    (1 : ℝ≥0∞) = μH[0] ({ x } : Set X) := (hausdorffMeasure_zero_singleton x).symm
    _ ≤ μH[0] s := measure_mono (singleton_subset_iff.2 hx)

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