dimH_univ — Mathlib

English

Let e be a continuous linear bijection between normed spaces E and F over a nontrivial normed field 𝕜. Then the Hausdorff dimension of the whole space is preserved by e, i.e. dim_H(univ_E) = dim_H(univ_F).

Русский

Пусть e: E ≃L[𝕜] F — линейное взаимодополнение между нормированными пространствами E и F над непустым нормированным полем 𝕜. Тогда размерность Хаусдорфа пространства сохраняется: dim_H(универсум_E) = dim_H(универсум_F).

LaTeX

$$$\\dim_H(\\mathrm{univ}_E) = \\dim_H(\\mathrm{univ}_F)$$$

Lean4

theorem dimH_univ (e : E ≃L[𝕜] F) : dimH (univ : Set E) = dimH (univ : Set F) := by
  rw [← e.dimH_preimage, preimage_univ]

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