Commit 2024-01-27 17:21 0bcd6be6
View on Github →feat: two lemmas about cut-off functions (#9873) From sphere-eversion; I'm just upstreaming this. The version in sphere-eversion uses an unbundled design; we provide a bundled version (for now) to match the remaining file.