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 #

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 × ℝ) ^ ι.

Instances For

    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.