English
If a smooth bump covering exists, then there is an immersion of the manifold into some Euclidean space.
Русский
Если существует гладкое бамп-покрытие, то существовaет погружение многообразия в некоторое евклидово пространство.
LaTeX
$$$\exists n\,\exists e: M \to \mathbb{R}^n \text{ such that } e \text{ is a ContMDiffMap and an immersion, with injectivity of mfderiv along } e$$$
Lean4
/-- Baby version of the Whitney weak embedding theorem: if `M` admits a finite covering by
supports of bump functions, then for some `n` it can be embedded into the `n`-dimensional
Euclidean space. -/
theorem exists_embedding_euclidean_of_compact [T2Space M] [CompactSpace M] :
∃ (n : ℕ) (e : M → EuclideanSpace ℝ (Fin n)),
ContMDiff I (𝓡 n) ∞ e ∧ IsClosedEmbedding e ∧ ∀ x : M, Injective (mfderiv I (𝓡 n) e x) :=
by
rcases SmoothBumpCovering.exists_isSubordinate I isClosed_univ fun (x : M) _ => univ_mem with ⟨ι, f, -⟩
haveI := f.fintype
rcases f.exists_immersion_euclidean with ⟨n, e, hsmooth, hinj, hinj_mfderiv⟩
exact ⟨n, e, hsmooth, hsmooth.continuous.isClosedEmbedding hinj, hinj_mfderiv⟩
