dense_compl_image_of_dimH_lt_finrank

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

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