dimH_sUnion — Mathlib

English

The Hausdorff dimension of the union of a countable family of sets equals the supremum of their dimensions.

Русский

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

LaTeX

$$dimH(⋃_{S∈S} S) = ⨆ s ∈ S, dimH(s)$$

Lean4

@[simp]
theorem dimH_sUnion {S : Set (Set X)} (hS : S.Countable) : dimH (⋃₀ S) = ⨆ s ∈ S, dimH s := by
  rw [sUnion_eq_biUnion, dimH_bUnion hS]

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