dimH_univ_pi_fin

Mathlib.Topology.MetricSpace.HausdorffDimension

URI: https://scilib.ai/kg/mathlib#Real.dimH_univ_pi_fin

English

For Finite n, the Hausdorff dimension of the space (ℝ)^{Fin n} is n.

Русский

Для Fin n размерность Хаусдорфа пространства (ℝ)^{Fin n} равна n.

LaTeX

$$$\\dim_H(\\mathrm{univ}) = n$$$

Lean4

theorem dimH_univ_pi_fin (n : ℕ) : dimH (univ : Set (Fin n → ℝ)) = n := by rw [dimH_univ_pi, Fintype.card_fin]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru