English
For a finite-dimensional real normed space E, the Hausdorff dimension of the universal set equals finrank E.
Русский
Для конечномерного вещественного нормированного пространства E размерность Хаусдорфа универсума равна finrank E.
LaTeX
$$$\\dim_H(\\mathrm{univ}) = \\mathrm{finrank}_{\\mathbb{R}}(E)$$$
Lean4
/-- A particular case of Sard's Theorem. Let `f : E → F` be a map between finite-dimensional real
vector spaces. Suppose that `f` is `C¹` smooth on a convex set `s` of Hausdorff dimension strictly
less than the dimension of `F`. Then the complement of the image `f '' s` is dense in `F`. -/
theorem dense_compl_image_of_dimH_lt_finrank [FiniteDimensional ℝ F] {f : E → F} {s t : Set E} (h : ContDiffOn ℝ 1 f s)
(hc : Convex ℝ s) (ht : t ⊆ s) (htF : dimH t < finrank ℝ F) : Dense (f '' t)ᶜ :=
dense_compl_of_dimH_lt_finrank <| (h.dimH_image_le hc ht).trans_lt htF