Zulip Chat Archive

Stream: maths

Topic: Towards Whitney's embedding theorem


view this post on Zulip 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.

view this post on Zulip 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? ;-)

view this post on Zulip 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 CC^\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.

view this post on Zulip Yury G. Kudryashov (Mar 23 2021 at 19:39):

More than a week later: #6839


Last updated: May 12 2021 at 08:14 UTC