dimH_iUnion — Mathlib

English

The Hausdorff dimension of a countable union equals the supremum of Hausdorff dimensions of the pieces.

Русский

Размерность Хаусдорфа счетного объединения равна наибольшему размерностей составных частей.

LaTeX

$$dimH(⋃_{i} s_i) = ⨆_{i} dimH(s_i)$$

Lean4

@[simp]
theorem dimH_iUnion {ι : Sort*} [Countable ι] (s : ι → Set X) : dimH (⋃ i, s i) = ⨆ i, dimH (s i) :=
  by
  borelize X
  refine le_antisymm (dimH_le fun d hd => ?_) (iSup_le fun i => dimH_mono <| subset_iUnion _ _)
  contrapose! hd
  have : ∀ i, μH[d] (s i) = 0 := fun i => hausdorffMeasure_of_dimH_lt ((le_iSup (fun i => dimH (s i)) i).trans_lt hd)
  rw [measure_iUnion_null this]
  exact ENNReal.zero_ne_top

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