Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Theorem
smooth_partition_of_unity.le_one
Modification history
2021-08-06 09:28
src/geometry/manifold/partition_of_unity.lean
feat(topology,geometry/manifold): continuous and smooth partition of unity (#8281) …
Added
smooth_partition_of_unity.le_one
View on Github →