Commit 2024-01-16 15:36 fce2e43c

feat: lemmas about partitions of unity (#9635)

• add finsupport: the support (the set of indices which functions are non-vanishing) at a point, as a Finset
• every point has a neighbourhood on which only finitely many functions are non-vanishing From sphere-eversion; I'm just upstreaming results.