# Documentation

Mathlib.Geometry.Manifold.WhitneyEmbedding

# Whitney embedding theorem #

In this file we prove a version of the Whitney embedding theorem: for any compact real manifold M, for sufficiently large n there exists a smooth embedding M → ℝ^n.

## TODO #

• Prove the weak Whitney embedding theorem: any σ-compact smooth m-dimensional manifold can be embedded into ℝ^(2m+1). This requires a version of Sard's theorem: for a locally Lipschitz continuous map f : ℝ^m → ℝ^n, m < n, the range has Hausdorff dimension at most m, hence it has measure zero.

## Tags #

partition of unity, smooth bump function, whitney theorem

### Whitney embedding theorem #

In this section we prove a version of the Whitney embedding theorem: for any compact real manifold M, for sufficiently large n there exists a smooth embedding M → ℝ^n.

def SmoothBumpCovering.embeddingPiTangent {ι : Type uι} {E : Type uE} [] [] {H : Type uH} [] {I : } {M : Type uM} [] [] [] [hi : ] {s : Set M} (f : ) :
ContMDiffMap I (modelWithCornersSelf (ιE × )) M (ιE × )

Smooth embedding of M into (E × ℝ) ^ ι.

Instances For
theorem SmoothBumpCovering.embeddingPiTangent_coe {ι : Type uι} {E : Type uE} [] [] {H : Type uH} [] {I : } {M : Type uM} [] [] [] [hi : ] {s : Set M} (f : ) :
= fun x i => (↑() x ↑(extChartAt I ()) x, ↑() x)
theorem SmoothBumpCovering.embeddingPiTangent_injOn {ι : Type uι} {E : Type uE} [] [] {H : Type uH} [] {I : } {M : Type uM} [] [] [] [hi : ] {s : Set M} (f : ) :
theorem SmoothBumpCovering.embeddingPiTangent_injective {ι : Type uι} {E : Type uE} [] [] {H : Type uH} [] {I : } {M : Type uM} [] [] [] [hi : ] (f : SmoothBumpCovering ι I M Set.univ) :
theorem SmoothBumpCovering.comp_embeddingPiTangent_mfderiv {ι : Type uι} {E : Type uE} [] [] {H : Type uH} [] {I : } {M : Type uM} [] [] [] [hi : ] {s : Set M} (f : ) (x : M) (hx : x s) :
theorem SmoothBumpCovering.embeddingPiTangent_ker_mfderiv {ι : Type uι} {E : Type uE} [] [] {H : Type uH} [] {I : } {M : Type uM} [] [] [] [hi : ] {s : Set M} (f : ) (x : M) (hx : x s) :
theorem SmoothBumpCovering.embeddingPiTangent_injective_mfderiv {ι : Type uι} {E : Type uE} [] [] {H : Type uH} [] {I : } {M : Type uM} [] [] [] [hi : ] {s : Set M} (f : ) (x : M) (hx : x s) :
theorem SmoothBumpCovering.exists_immersion_euclidean {ι : Type uι} {E : Type uE} [] [] {H : Type uH} [] {I : } {M : Type uM} [] [] [] [] (f : SmoothBumpCovering ι I M Set.univ) :
n e, Smooth I () e ∀ (x : M), Function.Injective ↑(mfderiv I () e x)

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 immersed into the n-dimensional Euclidean space.

theorem exists_embedding_euclidean_of_compact {E : Type uE} [] [] {H : Type uH} [] {I : } {M : Type uM} [] [] [] [] :
n e, Smooth I () e ∀ (x : M), Function.Injective ↑(mfderiv I () e x)

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.