Zulip Chat Archive

Stream: maths

Topic: Partition of unity


view this post on Zulip Yury G. Kudryashov (Feb 25 2021 at 07:01):

Hi, I'm trying to formalize smooth partition of unity. Is there anyone else interested in this? Current progress:

  • paracompact spaces : done, polishing for a PR, see #6395
  • shrinking lemma: WIP;
  • smooth bump function: done, needs refactoring;
  • general partition of unity: not started.

Last updated: May 19 2021 at 00:40 UTC