## Stream: maths

### Topic: Towards Whitney's embedding theorem

#### Yury G. Kudryashov (Mar 14 2021 at 11:13):

As a part of the "partition of unity" project I formalized a baby version of the Whitney embedding theorem: for a compact manifold there exists an embedding into some finite dimensional space.

#### Kevin Buzzard (Mar 14 2021 at 12:11):

I don't understand the definition at the other end of the link at all. Maybe add a docstring? ;-)

#### Yury G. Kudryashov (Mar 14 2021 at 14:27):

I'm going to make it PR-ready today. Adding docstrings is a part of this process. The definition is a smooth map from an abstract $C^\infty$-smooth manifold to a special finite dimensional space. The next lemmas say that this map is injective and its derivative is injective at every point.

#### Yury G. Kudryashov (Mar 23 2021 at 19:39):

More than a week later: #6839

Last updated: May 12 2021 at 08:14 UTC