English
If a smooth map f: E→F on finite-dimensional spaces has target dimension strictly larger than the domain, the complement of its range is dense in F.
Русский
Если размерность целевого пространства превышает размерность пространства домена, образ f(E) не охватывает всю F и дополнение к образу плотно в F.
LaTeX
$$Dense( F \\mathrm{range}(f) )$$
Lean4
/-- The Hausdorff dimension of the range of a `C¹`-smooth function defined on a finite-dimensional
real normed space is at most the dimension of its domain as a vector space over `ℝ`. -/
theorem dimH_range_le {f : E → F} (h : ContDiff ℝ 1 f) : dimH (range f) ≤ finrank ℝ E :=
calc
dimH (range f) = dimH (f '' univ) := by rw [image_univ]
_ ≤ dimH (univ : Set E) := (h.contDiffOn.dimH_image_le convex_univ Subset.rfl)
_ = finrank ℝ E := Real.dimH_univ_eq_finrank E
