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 -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