Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-06 09:28 f471b899

View on Github →

feat(topology,geometry/manifold): continuous and smooth partition of unity (#8281) Fixes #6392

Estimated changes

Modified src/geometry/manifold/bump_function.lean

Modified src/geometry/manifold/partition_of_unity.lean

added theorem bump_covering.coe_to_smooth_partition_of_unity

added theorem bump_covering.is_subordinate.to_smooth_partition_of_unity

added theorem bump_covering.smooth_to_partition_of_unity

added def bump_covering.to_smooth_partition_of_unity

added theorem bump_covering.to_smooth_partition_of_unity_to_partition_of_unity

added theorem exists_smooth_zero_one_of_closed

deleted def smooth_bump_covering.choice

deleted def smooth_bump_covering.choice_set

modified theorem smooth_bump_covering.coe_mk

added theorem smooth_bump_covering.exists_finset_to_smooth_partition_of_unity_eventually_eq

modified def smooth_bump_covering.ind

added theorem smooth_bump_covering.is_subordinate.support_subset

added theorem smooth_bump_covering.is_subordinate.to_smooth_partition_of_unity

modified def smooth_bump_covering.is_subordinate

added theorem smooth_bump_covering.is_subordinate_to_bump_covering

modified theorem smooth_bump_covering.mem_chart_at_source_of_eq_one

modified theorem smooth_bump_covering.mem_ext_chart_at_source_of_eq_one

added theorem smooth_bump_covering.sum_to_smooth_partition_of_unity_eq

added theorem smooth_bump_covering.support_to_smooth_partition_of_unity_subset

added def smooth_bump_covering.to_bump_covering

added def smooth_bump_covering.to_smooth_partition_of_unity

added theorem smooth_bump_covering.to_smooth_partition_of_unity_apply

added theorem smooth_bump_covering.to_smooth_partition_of_unity_eq_mul_prod

added theorem smooth_bump_covering.to_smooth_partition_of_unity_zero_of_zero

modified structure smooth_bump_covering

added theorem smooth_partition_of_unity.exists_is_subordinate

added def smooth_partition_of_unity.is_subordinate

added theorem smooth_partition_of_unity.is_subordinate_to_partition_of_unity

added theorem smooth_partition_of_unity.le_one

added theorem smooth_partition_of_unity.nonneg

added def smooth_partition_of_unity.single

added theorem smooth_partition_of_unity.smooth_sum

added theorem smooth_partition_of_unity.sum_eq_one

added theorem smooth_partition_of_unity.sum_le_one

added theorem smooth_partition_of_unity.sum_nonneg

added def smooth_partition_of_unity.to_partition_of_unity

added structure smooth_partition_of_unity

Modified src/geometry/manifold/times_cont_mdiff.lean

added theorem smooth_at_one

added theorem smooth_on_one

added theorem smooth_one

added theorem smooth_within_at_one

added theorem times_cont_mdiff_at_one

added theorem times_cont_mdiff_on_one

added theorem times_cont_mdiff_one

added theorem times_cont_mdiff_within_at_one

Modified src/geometry/manifold/times_cont_mdiff_map.lean

added theorem times_cont_mdiff_map.coe_fn_mk

Modified src/geometry/manifold/whitney_embedding.lean

added theorem exists_embedding_euclidean_of_compact

deleted theorem exists_embedding_finrank_of_compact

modified def smooth_bump_covering.embedding_pi_tangent

modified theorem smooth_bump_covering.embedding_pi_tangent_inj_on

modified theorem smooth_bump_covering.embedding_pi_tangent_injective

added theorem smooth_bump_covering.exists_immersion_euclidean

deleted theorem smooth_bump_covering.exists_immersion_finrank

Modified src/topology/paracompact.lean

Created src/topology/partition_of_unity.lean

added theorem bump_covering.coe_single

added theorem bump_covering.continuous_to_pou_fun

added theorem bump_covering.eventually_eq_one

added theorem bump_covering.exists_finset_to_partition_of_unity_eventually_eq

added theorem bump_covering.exists_finset_to_pou_fun_eventually_eq

added theorem bump_covering.exists_is_subordinate

added theorem bump_covering.exists_is_subordinate_of_locally_finite

added theorem bump_covering.exists_is_subordinate_of_locally_finite_of_prop

added theorem bump_covering.exists_is_subordinate_of_prop

added def bump_covering.ind

added theorem bump_covering.ind_apply

added theorem bump_covering.is_subordinate.mono

added theorem bump_covering.is_subordinate.to_partition_of_unity

added def bump_covering.is_subordinate

added theorem bump_covering.le_one

added theorem bump_covering.nonneg

added theorem bump_covering.sum_to_partition_of_unity_eq

added theorem bump_covering.sum_to_pou_fun_eq

added theorem bump_covering.support_to_partition_of_unity_subset

added theorem bump_covering.support_to_pou_fun_subset

added def bump_covering.to_partition_of_unity

added theorem bump_covering.to_partition_of_unity_apply

added theorem bump_covering.to_partition_of_unity_eq_mul_prod

added theorem bump_covering.to_partition_of_unity_zero_of_zero

added def bump_covering.to_pou_fun

added theorem bump_covering.to_pou_fun_eq_mul_prod

added theorem bump_covering.to_pou_fun_zero_of_zero

added structure bump_covering

added theorem partition_of_unity.exists_is_subordinate

added theorem partition_of_unity.exists_is_subordinate_of_locally_finite

added def partition_of_unity.is_subordinate

added theorem partition_of_unity.le_one

added theorem partition_of_unity.nonneg

added theorem partition_of_unity.sum_eq_one

added theorem partition_of_unity.sum_le_one

added theorem partition_of_unity.sum_nonneg

added structure partition_of_unity