noAtoms_hausdorff — Mathlib

English

For X metric spaces, μH[d] has no atoms for d > 0.

Русский

Для метрического пространства X, μH[d] имеет неатомарную структуру для d > 0.

LaTeX

$$$ \text{NoAtoms }(μH[d]) $$$

Lean4

theorem noAtoms_hausdorff {d : ℝ} (hd : 0 < d) : NoAtoms (hausdorffMeasure d : Measure X) :=
  by
  refine ⟨fun x => ?_⟩
  rw [← nonpos_iff_eq_zero, hausdorffMeasure_apply]
  refine iSup₂_le fun ε _ => iInf₂_le_of_le (fun _ => { x }) ?_ <| iInf_le_of_le (fun _ => ?_) ?_
  · exact subset_iUnion (fun _ => { x } : ℕ → Set X) 0
  · simp only [EMetric.diam_singleton, zero_le]
  · simp [hd]

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