Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-21 16:19 7f16dd20

View on Github →

feat(topology/partition_of_unity): local to global (#15490) Use partitions of unity to construct global maps. Motivated by discussions with @PatrickMassot . Useful for the sphere eversion project and probably duplicates some lemmas from that project.

Estimated changes

Modified src/analysis/convex/combination.lean

added theorem convex.finsum_mem

Created src/analysis/convex/partition_of_unity.lean

added theorem exists_continuous_forall_mem_convex_of_local

added theorem exists_continuous_forall_mem_convex_of_local_const

added theorem partition_of_unity.finsum_smul_mem_convex

Modified src/geometry/manifold/partition_of_unity.lean

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 smooth_partition_of_unity.cont_mdiff_finsum_smul

added theorem smooth_partition_of_unity.cont_mdiff_smul

added theorem smooth_partition_of_unity.finsum_smul_mem_convex

added theorem smooth_partition_of_unity.is_subordinate.cont_mdiff_finsum_smul

added theorem smooth_partition_of_unity.is_subordinate.smooth_finsum_smul

modified theorem smooth_partition_of_unity.is_subordinate_to_partition_of_unity

added theorem smooth_partition_of_unity.smooth_finsum_smul

added theorem smooth_partition_of_unity.smooth_smul

Modified src/topology/partition_of_unity.lean

added theorem bump_covering.locally_finite_tsupport

added theorem partition_of_unity.continuous_finsum_smul

added theorem partition_of_unity.continuous_smul

added theorem partition_of_unity.exists_pos

added theorem partition_of_unity.is_subordinate.continuous_finsum_smul

added theorem partition_of_unity.locally_finite_tsupport