Commit 2023-06-27 21:22 178dc4da

View on Github →

feat: port Geometry.Manifold.PartitionOfUnity (#5460)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Geometry/Manifold/PartitionOfUnity.lean

added theorem BumpCovering.IsSubordinate.toSmoothPartitionOfUnity

added theorem BumpCovering.coe_toSmoothPartitionOfUnity

added theorem BumpCovering.smooth_toPartitionOfUnity

added def BumpCovering.toSmoothPartitionOfUnity

added theorem BumpCovering.toSmoothPartitionOfUnity_toPartitionOfUnity

added theorem Emetric.exists_smooth_forall_closedBall_subset

added theorem Metric.exists_smooth_forall_closedBall_subset

added theorem SmoothBumpCovering.IsSubordinate.support_subset

added theorem SmoothBumpCovering.IsSubordinate.toSmoothPartitionOfUnity

added def SmoothBumpCovering.IsSubordinate

added theorem SmoothBumpCovering.apply_ind

added theorem SmoothBumpCovering.eventuallyEq_one

added theorem SmoothBumpCovering.exists_finset_toSmoothPartitionOfUnity_eventuallyEq

added theorem SmoothBumpCovering.exists_isSubordinate

added def SmoothBumpCovering.ind

added theorem SmoothBumpCovering.isSubordinate_toBumpCovering

added theorem SmoothBumpCovering.mem_chartAt_ind_source

added theorem SmoothBumpCovering.mem_chartAt_source_of_eq_one

added theorem SmoothBumpCovering.mem_extChartAt_ind_source

added theorem SmoothBumpCovering.mem_extChartAt_source_of_eq_one

added theorem SmoothBumpCovering.mem_support_ind

added theorem SmoothBumpCovering.sum_toSmoothPartitionOfUnity_eq

added theorem SmoothBumpCovering.support_toSmoothPartitionOfUnity_subset

added def SmoothBumpCovering.toBumpCovering

added def SmoothBumpCovering.toSmoothPartitionOfUnity

added theorem SmoothBumpCovering.toSmoothPartitionOfUnity_apply

added theorem SmoothBumpCovering.toSmoothPartitionOfUnity_eq_mul_prod

added theorem SmoothBumpCovering.toSmoothPartitionOfUnity_zero_of_zero

added structure SmoothBumpCovering

added theorem SmoothPartitionOfUnity.IsSubordinate.contMDiff_finsum_smul

added theorem SmoothPartitionOfUnity.IsSubordinate.smooth_finsum_smul

added def SmoothPartitionOfUnity.IsSubordinate

added theorem SmoothPartitionOfUnity.contMDiff_finsum_smul

added theorem SmoothPartitionOfUnity.contMDiff_smul

added theorem SmoothPartitionOfUnity.exists_isSubordinate

added theorem SmoothPartitionOfUnity.finsum_smul_mem_convex

added theorem SmoothPartitionOfUnity.isSubordinate_toPartitionOfUnity

added theorem SmoothPartitionOfUnity.le_one

added theorem SmoothPartitionOfUnity.nonneg

added def SmoothPartitionOfUnity.single

added theorem SmoothPartitionOfUnity.smooth_finsum_smul

added theorem SmoothPartitionOfUnity.smooth_smul

added theorem SmoothPartitionOfUnity.smooth_sum

added theorem SmoothPartitionOfUnity.sum_eq_one

added theorem SmoothPartitionOfUnity.sum_le_one

added theorem SmoothPartitionOfUnity.sum_nonneg

added def SmoothPartitionOfUnity.toPartitionOfUnity

added structure SmoothPartitionOfUnity

added theorem exists_cont_mdiff_forall_mem_convex_of_local

added theorem exists_smooth_forall_mem_convex_of_local

added theorem exists_smooth_forall_mem_convex_of_local_const

added theorem exists_smooth_zero_one_of_closed