mathlib documentation

geometry.manifold.whitney_embedding

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 #

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 smooth_bump_covering.embedding_pi_tangent {ι : Type uι} {E : Type uE} [normed_group E] [normed_space E] [finite_dimensional E] {H : Type uH} [topological_space H] {I : model_with_corners E H} {M : Type uM} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] [t2_space M] [fintype ι] {s : set M} (f : smooth_bump_covering ι I M s) :
C^I, M; 𝓘(, ι → E × ), ι → E ×

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

Equations
theorem smooth_bump_covering.embedding_pi_tangent_coe {ι : Type uι} {E : Type uE} [normed_group E] [normed_space E] [finite_dimensional E] {H : Type uH} [topological_space H] {I : model_with_corners E H} {M : Type uM} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] [t2_space M] [fintype ι] {s : set M} (f : smooth_bump_covering ι I M s) :
(f.embedding_pi_tangent) = λ (x : M) (i : ι), ((f i) x (ext_chart_at I (f.c i)) x, (f i) x)
theorem smooth_bump_covering.comp_embedding_pi_tangent_mfderiv {ι : Type uι} {E : Type uE} [normed_group E] [normed_space E] [finite_dimensional E] {H : Type uH} [topological_space H] {I : model_with_corners E H} {M : Type uM} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] [t2_space M] [fintype ι] {s : set M} (f : smooth_bump_covering ι I M s) (x : M) (hx : x s) :
theorem smooth_bump_covering.embedding_pi_tangent_ker_mfderiv {ι : Type uι} {E : Type uE} [normed_group E] [normed_space E] [finite_dimensional E] {H : Type uH} [topological_space H] {I : model_with_corners E H} {M : Type uM} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] [t2_space M] [fintype ι] {s : set M} (f : smooth_bump_covering ι I M s) (x : M) (hx : x s) :

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.

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.