Topic: Partition of unity
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