dimH_univ_pi — Mathlib

English

For any index set ι, the Hausdorff dimension of the full product space ι → ℝ equals the cardinality of ι.

Русский

Для любого индекса ι размерность Хаусдорфа пространства ι → ℝ равна кардиналу ι.

LaTeX

$$$\\dim_H(\\mathrm{univ}_{\\,\\iota}) = |\\iota|$$$

Lean4

theorem dimH_univ_pi (ι : Type*) [Fintype ι] : dimH (univ : Set (ι → ℝ)) = Fintype.card ι := by
  simp only [← Metric.iUnion_ball_nat_succ (0 : ι → ℝ), dimH_iUnion, dimH_ball_pi _ (Nat.cast_add_one_pos _),
    iSup_const]

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