Commit 2023-05-09 06:12 47189ba3

View on Github →

feat: port Topology.PartitionOfUnity (#3863)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/PartitionOfUnity.lean

added theorem BumpCovering.IsSubordinate.mono

added theorem BumpCovering.IsSubordinate.toPartitionOfUnity

added def BumpCovering.IsSubordinate

added theorem BumpCovering.coe_single

added theorem BumpCovering.continuous_toPouFun

added theorem BumpCovering.eventuallyEq_one

added theorem BumpCovering.exists_finset_toPartitionOfUnity_eventuallyEq

added theorem BumpCovering.exists_finset_toPouFun_eventuallyEq

added theorem BumpCovering.exists_isSubordinate

added theorem BumpCovering.exists_isSubordinate_of_locallyFinite

added theorem BumpCovering.exists_isSubordinate_of_locallyFinite_of_prop

added theorem BumpCovering.exists_isSubordinate_of_prop

added def BumpCovering.ind

added theorem BumpCovering.ind_apply

added theorem BumpCovering.le_one

added theorem BumpCovering.locallyFinite_tsupport

added theorem BumpCovering.nonneg

added theorem BumpCovering.sum_toPartitionOfUnity_eq

added theorem BumpCovering.sum_toPouFun_eq

added theorem BumpCovering.support_toPartitionOfUnity_subset

added theorem BumpCovering.support_toPouFun_subset

added def BumpCovering.toPartitionOfUnity

added theorem BumpCovering.toPartitionOfUnity_apply

added theorem BumpCovering.toPartitionOfUnity_eq_mul_prod

added theorem BumpCovering.toPartitionOfUnity_zero_of_zero

added def BumpCovering.toPouFun

added theorem BumpCovering.toPouFun_eq_mul_prod

added theorem BumpCovering.toPouFun_zero_of_zero

added structure BumpCovering

added theorem PartitionOfUnity.IsSubordinate.continuous_finsum_smul

added def PartitionOfUnity.IsSubordinate

added theorem PartitionOfUnity.continuous_finsum_smul

added theorem PartitionOfUnity.continuous_smul

added theorem PartitionOfUnity.exists_finset_nhd_support_subset

added theorem PartitionOfUnity.exists_isSubordinate

added theorem PartitionOfUnity.exists_isSubordinate_of_locallyFinite

added theorem PartitionOfUnity.exists_pos

added theorem PartitionOfUnity.le_one

added theorem PartitionOfUnity.locallyFinite_tsupport

added theorem PartitionOfUnity.nonneg

added theorem PartitionOfUnity.sum_eq_one

added theorem PartitionOfUnity.sum_le_one

added theorem PartitionOfUnity.sum_nonneg

added structure PartitionOfUnity