Commit 2024-02-13 19:40 ff21e64f

View on Github →

feat: fintsupport of (smooth) partitions of unity (#10015) From sphere-eversion: the result is used there for smooth partitions of unity, but also holds in the continuous setting. In passing,

use Type* (not Type _) in sum_finsupport_smul_eq_finsum,
tag SmoothPartitionOfUnity.toPartitionOfUnity with @simps.

Estimated changes

Modified Mathlib/Geometry/Manifold/PartitionOfUnity.lean

added theorem SmoothPartitionOfUnity.coe_finsupport

added theorem SmoothPartitionOfUnity.eventually_finsupport_subset

added theorem SmoothPartitionOfUnity.eventually_fintsupport_subset

added theorem SmoothPartitionOfUnity.finite_tsupport

added def SmoothPartitionOfUnity.finsupport

added theorem SmoothPartitionOfUnity.finsupport_subset_fintsupport

added def SmoothPartitionOfUnity.fintsupport

added theorem SmoothPartitionOfUnity.mem_finsupport

added theorem SmoothPartitionOfUnity.mem_fintsupport_iff

added theorem SmoothPartitionOfUnity.sum_finsupport'

added theorem SmoothPartitionOfUnity.sum_finsupport

added theorem SmoothPartitionOfUnity.sum_finsupport_smul_eq_finsum

Modified Mathlib/Topology/PartitionOfUnity.lean

added theorem PartitionOfUnity.eventually_finsupport_subset

added theorem PartitionOfUnity.eventually_fintsupport_subset

added theorem PartitionOfUnity.finite_tsupport

added theorem PartitionOfUnity.finsupport_subset_fintsupport

added def PartitionOfUnity.fintsupport

added theorem PartitionOfUnity.mem_fintsupport_iff

modified theorem PartitionOfUnity.sum_finsupport_smul_eq_finsum