Commit 2023-08-11 08:55 b44650d7

View on Github →

feat: construct a smooth function on a manifold equal to one on a given closed set and with given support (#6067)

Estimated changes

Modified Mathlib/Geometry/Manifold/PartitionOfUnity.lean

added theorem IsOpen.exists_msmooth_support_eq

added theorem IsOpen.exists_msmooth_support_eq_aux

added theorem SmoothPartitionOfUnity.exists_isSubordinate_chartAt_source

added theorem SmoothPartitionOfUnity.exists_isSubordinate_chartAt_source_of_isClosed

added theorem SmoothPartitionOfUnity.exists_pos_of_mem

added theorem exists_msmooth_support_eq_eq_one_iff

added theorem exists_msmooth_zero_iff_one_iff_of_closed