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