dimH_univ_eq_finrank — Mathlib

English

In a finite-dimensional real normed space E, the Hausdorff dimension of the whole space equals finrank E.

Русский

В конечномерном вещественном нормированном пространстве E размерность Хаусдорфа пространства E равна finrank E.

LaTeX

$$$\\dim_H(\\mathrm{univ}) = \\mathrm{finrank}_{\\mathbb{R}}(E)$$$

Lean4

theorem dimH_univ_eq_finrank : dimH (univ : Set E) = finrank ℝ E :=
  dimH_of_mem_nhds (@univ_mem _ (𝓝 0))

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