# mathlib3documentation

geometry.manifold.whitney_embedding

# Whitney embedding theorem #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

noncomputable def smooth_bump_covering.embedding_pi_tangent {ι : Type uι} {E : Type uE} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] [t2_space M] [hi : fintype ι] {s : set M} (f : M s) :
E × )) M E × )

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

Equations
theorem smooth_bump_covering.embedding_pi_tangent_coe {ι : Type uι} {E : Type uE} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] [t2_space M] [hi : fintype ι] {s : set M} (f : M s) :
(f.embedding_pi_tangent) = λ (x : M) (i : ι), ((f i) x (f.c i)) x, (f i) x)
theorem smooth_bump_covering.embedding_pi_tangent_inj_on {ι : Type uι} {E : Type uE} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] [t2_space M] [hi : fintype ι] {s : set M} (f : M s) :
theorem smooth_bump_covering.embedding_pi_tangent_injective {ι : Type uι} {E : Type uE} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] [t2_space M] [hi : fintype ι] (f : M)) :
theorem smooth_bump_covering.comp_embedding_pi_tangent_mfderiv {ι : Type uι} {E : Type uE} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] [t2_space M] [hi : fintype ι] {s : set M} (f : M s) (x : M) (hx : x s) :
.comp (continuous_linear_map.proj (f.ind x hx))).comp (mfderiv I E × )) (f.embedding_pi_tangent) x) = I (f.c (f.ind x hx))) x
theorem smooth_bump_covering.embedding_pi_tangent_ker_mfderiv {ι : Type uι} {E : Type uE} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] [t2_space M] [hi : fintype ι] {s : set M} (f : M s) (x : M) (hx : x s) :
theorem smooth_bump_covering.embedding_pi_tangent_injective_mfderiv {ι : Type uι} {E : Type uE} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] [t2_space M] [hi : fintype ι] {s : set M} (f : M s) (x : M) (hx : x s) :
theorem smooth_bump_covering.exists_immersion_euclidean {ι : Type uι} {E : Type uE} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] [t2_space M] [finite ι] (f : M)) :
(n : ) (e : M (fin n)), (fin n))) e (x : M), function.injective (mfderiv I (fin n))) 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} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] [t2_space M]  :
(n : ) (e : M (fin n)), (fin n))) e (x : M), function.injective (mfderiv I (fin n))) 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.