Towards Whitney's embedding theorem

Stream: maths

[Yury G. Kudryashov]

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]

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

[Yury G. Kudryashov]

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]

More than a week later: #6839