Commit 2025-08-20 17:51 c5657193

View on Github →

feat(Manifold/PartitionOfUnity): existence of global C^n smooth section for nontrivial bundles (#26875) Add existence of global C^n smooth section for nontrivial bundles

Estimated changes

Modified Mathlib/Geometry/Manifold/PartitionOfUnity.lean

added theorem SmoothPartitionOfUnity.contMDiff_totalSpace_weighted_sum_of_local_sections

added theorem exists_contMDiffOn_section_forall_mem_convex_of_local

added theorem exists_smooth_section_forall_mem_convex_of_local