dense_compl_range_of_finrank_lt_finrank

English

The Hausdorff dimension of the image of a set under the orthogonal projection to a subspace is at most the dimension of the original set.

Русский

Размерность Хаусдорфа образа множества под проекцией на подпространство не превосходит размерности исходного множества.

LaTeX

$$dimH(K.orthogonalProjection '' s) ≤ dimH s$$

Lean4

/-- A particular case of Sard's Theorem. If `f` is a `C¹` smooth map from a real vector space to a
real vector space `F` of strictly larger dimension, then the complement of the range of `f` is dense
in `F`. -/
theorem dense_compl_range_of_finrank_lt_finrank [FiniteDimensional ℝ F] {f : E → F} (h : ContDiff ℝ 1 f)
    (hEF : finrank ℝ E < finrank ℝ F) : Dense (range f)ᶜ :=
  dense_compl_of_dimH_lt_finrank <| h.dimH_range_le.trans_lt <| Nat.cast_lt.2 hEF

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