hausdorffMeasure_le_one_of_subsingleton

English

If s is subsingleton and d ≥ 0, then the d-dimensional Hausdorff measure of s is at most 1.

Русский

Если s subsingleton и d ≥ 0, то μ_H^d(s) ≤ 1.

LaTeX

$$$s \text{ subsingleton} \Rightarrow \mu_H^{d}(s) \le 1 \quad (d \ge 0)$$$

Lean4

theorem hausdorffMeasure_le_one_of_subsingleton {s : Set X} (hs : s.Subsingleton) {d : ℝ} (hd : 0 ≤ d) : μH[d] s ≤ 1 :=
  by
  rcases eq_empty_or_nonempty s with (rfl | ⟨x, hx⟩)
  · simp only [measure_empty, zero_le]
  · rw [(subsingleton_iff_singleton hx).1 hs]
    rcases eq_or_lt_of_le hd with (rfl | dpos)
    · simp only [le_refl, hausdorffMeasure_zero_singleton]
    · haveI := noAtoms_hausdorff X dpos
      simp only [zero_le, measure_singleton]

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