TheoremstoSmoothPartitionOfUnity, coe_toSmoothPartitionOfUnity, contMDiff_toPartitionOfUnity, toSmoothPartitionOfUnity_toPartitionOfUnity, exists_contMDiffMap_forall_closedBall_subset, exists_smooth_forall_closedBall_subset, exists_contMDiff_support_eq, exists_contMDiff_support_eq_aux, exists_msmooth_support_eq, exists_msmooth_support_eq_aux, exists_contMDiffMap_forall_closedBall_subset, exists_contMDiffMap_forall_closedEBall_subset, exists_smooth_forall_closedBall_subset, support_subset, toBumpCovering, toSmoothPartitionOfUnity, apply_ind, c_mem', eventuallyEq_one, eventuallyEq_one', exists_finset_toSmoothPartitionOfUnity_eventuallyEq, exists_isSubordinate, isSubordinate_toBumpCovering, locallyFinite, locallyFinite', mem_chartAt_ind_source, mem_chartAt_source_of_eq_one, mem_extChartAt_ind_source, mem_extChartAt_source_of_eq_one, mem_support_ind, point_finite, sum_toSmoothPartitionOfUnity_eq, support_toSmoothPartitionOfUnity_subset, toSmoothPartitionOfUnity_apply, toSmoothPartitionOfUnity_eq_mul_prod, toSmoothPartitionOfUnity_zero_of_zero, contMDiff_finsum_smul, toPartitionOfUnity, coe_finsupport, contDiffAt_finsum, contMDiffAt_finsum, contMDiff_finsum_smul, contMDiff_smul, contMDiff_sum, eventually_finsupport_subset, eventually_fintsupport_subset, exists_isSubordinate, exists_isSubordinate_chartAt_source, exists_isSubordinate_chartAt_source_of_isClosed, exists_pos_of_mem, finite_tsupport, finsum_smul_mem_convex, finsupport_subset_fintsupport, isSubordinate_toPartitionOfUnity, le_one, locallyFinite, locallyFinite', mem_finsupport, mem_fintsupport_iff, nonneg, nonneg', sum_eq_one, sum_eq_one', sum_finsupport, sum_finsupport', sum_finsupport_smul_eq_finsum, sum_le_one, sum_le_one', sum_nonneg, toPartitionOfUnity_toFun, exists_contMDiffMap_forall_mem_convex_of_local, exists_contMDiffMap_forall_mem_convex_of_local_const, exists_contMDiffMap_one_nhds_of_subset_interior, exists_contMDiffMap_zero_one_nhds_of_isClosed, exists_contMDiffMap_zero_one_of_isClosed, exists_contMDiffOn_forall_mem_convex_of_local, exists_contMDiffOn_section_forall_mem_convex_of_local, exists_contMDiffSection_forall_mem_convex_of_local, exists_contMDiff_support_eq_eq_one_iff, exists_contMDiff_zero_iff_one_iff_of_isClosed, exists_msmooth_support_eq_eq_one_iff, exists_msmooth_zero_iff_one_iff_of_isClosed, exists_smooth_forall_mem_convex_of_local, exists_smooth_forall_mem_convex_of_local_const, exists_smooth_one_nhds_of_subset_interior, exists_smooth_section_forall_mem_convex_of_local, exists_smooth_zero_one_nhds_of_isClosed, exists_smooth_zero_one_of_isClosed | 88 |