mathlib3 documentation

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 #

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.

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

Equations
theorem smooth_bump_covering.embedding_pi_tangent_coe {ι : Type uι} {E : Type uE} [normed_add_comm_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] [hi : 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)

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.