Mathlib Changelog
v3
Changelog
About
Github
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