dimH_bUnion — Mathlib

English

For a countable set of sets, the dimH of the big union equals the supremum over the dimH of the members.

Русский

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

LaTeX

$$dimH(⋃ i ∈ s, t i) = ⨆ i ∈ s, dimH(t i)$$

Lean4

@[simp]
theorem dimH_bUnion {s : Set ι} (hs : s.Countable) (t : ι → Set X) : dimH (⋃ i ∈ s, t i) = ⨆ i ∈ s, dimH (t i) :=
  by
  haveI := hs.toEncodable
  rw [biUnion_eq_iUnion, dimH_iUnion, ← iSup_subtype'']

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