mathlib3
7f16dd20 - feat(topology/partition_of_unity): local to global (#15490)

Commit
3 years ago
feat(topology/partition_of_unity): local to global (#15490) Use partitions of unity to construct global maps. Motivated by discussions with @PatrickMassot . Useful for the sphere eversion project and probably duplicates some lemmas from that project.
Author
Parents
Loading