dimH_union — Mathlib

English

Let s and t be subsets of a metric space X. Then the Hausdorff dimension of their union equals the maximum of the Hausdorff dimensions of s and t.

Русский

Пусть s и t — подмножества метрического пространства X. Тогда размерность Хаусдорфа объединения s и t равна максимуму размерностей Хаусдорфа s и Хаусдорфа t.

LaTeX

$$$$\\dimH(s \\cup t) = \\max(\\dimH s, \\dimH t).$$$$

Lean4

@[simp]
theorem dimH_union (s t : Set X) : dimH (s ∪ t) = max (dimH s) (dimH t) := by
  rw [union_eq_iUnion, dimH_iUnion, iSup_bool_eq, cond, cond]

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