PartitionOfUnity

📁 Source: Mathlib/Topology/PartitionOfUnity.lean

Statistics

Metric	Count
Definitions `BumpCovering`, `IsSubordinate`, `ind`, `instFunLikeContinuousMapReal`, `instInhabited`, `single`, `toFun`, `toPOUFun`, `toPartitionOfUnity`, `PartitionOfUnity`, `IsSubordinate`, `finsupport`, `fintsupport`, `instFunLikeContinuousMapReal`, `instInhabited`, `toFun`	16
Theorems `mono`, `toPartitionOfUnity`, `coe_single`, `continuous_toPOUFun`, `eventuallyEq_one`, `eventuallyEq_one'`, `exists_finset_toPOUFun_eventuallyEq`, `exists_finset_toPartitionOfUnity_eventuallyEq`, `exists_isSubordinate`, `exists_isSubordinate_hasCompactSupport_of_locallyFinite_t2space`, `exists_isSubordinate_of_locallyFinite`, `exists_isSubordinate_of_locallyFinite_of_prop`, `exists_isSubordinate_of_locallyFinite_of_prop_t2space`, `exists_isSubordinate_of_prop`, `ind_apply`, `le_one`, `le_one'`, `locallyFinite`, `locallyFinite'`, `locallyFinite_tsupport`, `nonneg`, `nonneg'`, `point_finite`, `sum_toPOUFun_eq`, `sum_toPartitionOfUnity_eq`, `support_toPOUFun_subset`, `support_toPartitionOfUnity_subset`, `toFun_eq_coe`, `toPOUFun_eq_mul_prod`, `toPOUFun_zero_of_zero`, `toPartitionOfUnity_apply`, `toPartitionOfUnity_eq_mul_prod`, `toPartitionOfUnity_zero_of_zero`, `continuous_finsum_smul`, `coe_finsupport`, `continuous_finsum_smul`, `continuous_smul`, `eventually_finsupport_subset`, `eventually_fintsupport_subset`, `exists_finset_nhds`, `exists_finset_nhds'`, `exists_finset_nhds_support_subset`, `exists_isSubordinate`, `exists_isSubordinate_of_locallyFinite`, `exists_isSubordinate_of_locallyFinite_t2space`, `exists_pos`, `finite_tsupport`, `finsupport_subset_fintsupport`, `le_one`, `locallyFinite`, `locallyFinite'`, `locallyFinite_tsupport`, `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`, `exists_continuous_sum_one_of_isOpen_isCompact`	65
Total	81

BumpCovering

Definitions

Name	Category	Theorems
`IsSubordinate` 📖	MathDef	8 math math: `exists_isSubordinate_of_prop`, `SmoothBumpCovering.IsSubordinate.toBumpCovering`, `exists_isSubordinate_of_locallyFinite_of_prop_t2space`, `exists_isSubordinate_of_locallyFinite_of_prop`, `exists_isSubordinate_of_locallyFinite`, `SmoothBumpCovering.isSubordinate_toBumpCovering`, `exists_isSubordinate`, `exists_isSubordinate_hasCompactSupport_of_locallyFinite_t2space`
`ind` 📖	CompOp	2 math math: `eventuallyEq_one`, `ind_apply`
`instFunLikeContinuousMapReal` 📖	CompOp	22 math math: `eventuallyEq_one`, `toPartitionOfUnity_apply`, `point_finite`, `support_toPOUFun_subset`, `le_one`, `exists_isSubordinate_of_prop`, `toPartitionOfUnity_eq_mul_prod`, `locallyFinite`, `exists_finset_toPartitionOfUnity_eventuallyEq`, `locallyFinite_tsupport`, `toFun_eq_coe`, `exists_isSubordinate_of_locallyFinite_of_prop_t2space`, `ind_apply`, `sum_toPartitionOfUnity_eq`, `exists_isSubordinate_of_locallyFinite_of_prop`, `nonneg`, `exists_finset_toPOUFun_eventuallyEq`, `toPOUFun_eq_mul_prod`, `exists_isSubordinate_hasCompactSupport_of_locallyFinite_t2space`, `sum_toPOUFun_eq`, `coe_single`, `support_toPartitionOfUnity_subset`
`instInhabited` 📖	CompOp	—
`single` 📖	CompOp	1 math math: `coe_single`
`toFun` 📖	CompOp	5 math math: `nonneg'`, `toFun_eq_coe`, `eventuallyEq_one'`, `locallyFinite'`, `le_one'`
`toPOUFun` 📖	CompOp	6 math math: `support_toPOUFun_subset`, `continuous_toPOUFun`, `toPOUFun_zero_of_zero`, `exists_finset_toPOUFun_eventuallyEq`, `toPOUFun_eq_mul_prod`, `sum_toPOUFun_eq`
`toPartitionOfUnity` 📖	CompOp	10 math math: `toPartitionOfUnity_apply`, `toPartitionOfUnity_zero_of_zero`, `contMDiff_toPartitionOfUnity`, `toPartitionOfUnity_eq_mul_prod`, `toSmoothPartitionOfUnity_toPartitionOfUnity`, `exists_finset_toPartitionOfUnity_eventuallyEq`, `sum_toPartitionOfUnity_eq`, `IsSubordinate.toPartitionOfUnity`, `coe_toSmoothPartitionOfUnity`, `support_toPartitionOfUnity_subset`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_single` 📖	mathematical	—	`DFunLike.coe` `BumpCovering` `ContinuousMap` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `instFunLikeContinuousMapReal` `single` `Pi.single` `ContinuousMap.instZero` `Real.instZero` `ContinuousMap.instOne` `Real.instOne`	—	—
`continuous_toPOUFun` 📖	mathematical	—	`Continuous` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `toPOUFun`	—	`Continuous.mul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `ContinuousMapClass.map_continuous` `ContinuousMap.instContinuousMapClass` `continuous_finprod_cond` `Continuous.sub` `IsTopologicalAddGroup.to_continuousSub` `instIsTopologicalAddGroupReal` `continuous_const` `Function.mulSupport_one_sub` `locallyFinite`
`eventuallyEq_one` 📖	mathematical	`Set` `Set.instMembership`	`Filter.EventuallyEq` `Real` `nhds` `DFunLike.coe` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `ContinuousMap.instFunLike` `BumpCovering` `instFunLikeContinuousMapReal` `ind` `Pi.instOne` `Real.instOne`	—	`eventuallyEq_one'`
`eventuallyEq_one'` 📖	mathematical	`Set` `Set.univ` `Set.instMembership`	`Filter.EventuallyEq` `Real` `nhds` `DFunLike.coe` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `ContinuousMap.instFunLike` `toFun` `Pi.instOne` `Real.instOne`	—	—
`exists_finset_toPOUFun_eventuallyEq` 📖	mathematical	—	`Filter.EventuallyEq` `Real` `nhds` `toPOUFun` `Pi.instMul` `Real.instMul` `DFunLike.coe` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `ContinuousMap.instFunLike` `BumpCovering` `instFunLikeContinuousMapReal` `Finset.prod` `ContinuousMap.instCommMonoidOfContinuousMul` `Real.instCommMonoid` `IsTopologicalSemiring.toContinuousMul` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `CommRing.toRing` `Real.commRing` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `Real.normedCommRing` `instIsTopologicalRingReal` `Finset.filter` `WellOrderingRel` `ContinuousMap.instSubOfContinuousSub` `Real.instSub` `IsTopologicalAddGroup.to_continuousSub` `Real.instAddGroup` `instIsTopologicalAddGroupReal` `ContinuousMap.instOne` `Real.instOne`	—	`IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `IsTopologicalAddGroup.to_continuousSub` `instIsTopologicalAddGroupReal` `locallyFinite` `Filter.mp_mem` `Filter.univ_mem'` `ContinuousMap.coe_prod` `Finset.prod_apply` `toPOUFun_eq_mul_prod` `Set.Finite.mem_toFinset`
`exists_finset_toPartitionOfUnity_eventuallyEq` 📖	mathematical	—	`Filter.EventuallyEq` `Real` `nhds` `DFunLike.coe` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `ContinuousMap.instFunLike` `PartitionOfUnity` `PartitionOfUnity.instFunLikeContinuousMapReal` `toPartitionOfUnity` `Pi.instMul` `Real.instMul` `BumpCovering` `instFunLikeContinuousMapReal` `Finset.prod` `ContinuousMap.instCommMonoidOfContinuousMul` `Real.instCommMonoid` `IsTopologicalSemiring.toContinuousMul` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `CommRing.toRing` `Real.commRing` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `Real.normedCommRing` `instIsTopologicalRingReal` `Finset.filter` `WellOrderingRel` `ContinuousMap.instSubOfContinuousSub` `Real.instSub` `IsTopologicalAddGroup.to_continuousSub` `Real.instAddGroup` `instIsTopologicalAddGroupReal` `ContinuousMap.instOne` `Real.instOne`	—	`exists_finset_toPOUFun_eventuallyEq`
`exists_isSubordinate` 📖	mathematical	`IsOpen` `Set` `Set.instHasSubset` `Set.iUnion`	`IsSubordinate`	—	`precise_refinement_set` `exists_isSubordinate_of_locallyFinite` `IsSubordinate.mono`
`exists_isSubordinate_hasCompactSupport_of_locallyFinite_t2space` 📖	mathematical	`IsCompact` `IsOpen` `LocallyFinite` `Set` `Set.instHasSubset` `Set.iUnion`	`IsSubordinate` `HasCompactSupport` `Real` `Real.instZero` `DFunLike.coe` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `ContinuousMap.instFunLike` `BumpCovering` `instFunLikeContinuousMapReal`	—	`exists_isSubordinate_of_locallyFinite_of_prop_t2space` `exists_continuous_zero_one_of_isCompact'` `instRegularSpaceOfWeaklyLocallyCompactSpaceOfR1Space` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace` `T2Space.r1Space` `Disjoint.symm`
`exists_isSubordinate_of_locallyFinite` 📖	mathematical	`IsOpen` `LocallyFinite` `Set` `Set.instHasSubset` `Set.iUnion`	`IsSubordinate`	—	`exists_isSubordinate_of_locallyFinite_of_prop` `exists_continuous_zero_one_of_isClosed`
`exists_isSubordinate_of_locallyFinite_of_prop` 📖	mathematical	`DFunLike.coe` `ContinuousMap` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `ContinuousMap.instFunLike` `Set.EqOn` `Pi.instZero` `Real.instZero` `Pi.instOne` `Real.instOne` `Set` `Set.instMembership` `Set.Icc` `Real.instPreorder` `IsOpen` `LocallyFinite` `Set.instHasSubset` `Set.iUnion`	`BumpCovering` `instFunLikeContinuousMapReal` `IsSubordinate`	—	`exists_subset_iUnion_closure_subset` `LocallyFinite.point_finite` `Set.Subset.trans` `subset_closure` `LocallyFinite.subset` `Function.support_subset_iff'` `Set.mem_iUnion` `Set.EqOn.eventuallyEq_of_mem` `Set.EqOn.mono` `IsOpen.mem_nhds` `closure_mono` `isClosed_compl_iff` `isClosed_closure` `Set.disjoint_right`
`exists_isSubordinate_of_locallyFinite_of_prop_t2space` 📖	mathematical	`DFunLike.coe` `ContinuousMap` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `ContinuousMap.instFunLike` `Set.EqOn` `Pi.instZero` `Real.instZero` `Pi.instOne` `Real.instOne` `Set` `Set.instMembership` `Set.Icc` `Real.instPreorder` `IsCompact` `IsOpen` `LocallyFinite` `Set.instHasSubset` `Set.iUnion`	`BumpCovering` `instFunLikeContinuousMapReal` `IsSubordinate` `HasCompactSupport`	—	`exists_subset_iUnion_closure_subset_t2space` `LocallyFinite.point_finite` `HasSubset.Subset.trans` `Set.instIsTransSubset` `subset_closure` `LocallyFinite.subset` `Function.support_subset_iff'` `Set.Subset.trans` `Set.mem_iUnion` `Set.EqOn.eventuallyEq_of_mem` `Set.EqOn.mono` `IsOpen.mem_nhds` `closure_mono` `IsCompact.of_isClosed_subset` `isClosed_closure` `isClosed_compl_iff` `Set.disjoint_right`
`exists_isSubordinate_of_prop` 📖	mathematical	`DFunLike.coe` `ContinuousMap` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `ContinuousMap.instFunLike` `Set.EqOn` `Pi.instZero` `Real.instZero` `Pi.instOne` `Real.instOne` `Set` `Set.instMembership` `Set.Icc` `Real.instPreorder` `IsOpen` `Set.instHasSubset` `Set.iUnion`	`BumpCovering` `instFunLikeContinuousMapReal` `IsSubordinate`	—	`precise_refinement_set` `exists_isSubordinate_of_locallyFinite_of_prop` `IsSubordinate.mono`
`ind_apply` 📖	mathematical	`Set` `Set.instMembership`	`DFunLike.coe` `ContinuousMap` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `ContinuousMap.instFunLike` `BumpCovering` `instFunLikeContinuousMapReal` `ind` `Real.instOne`	—	`Filter.EventuallyEq.eq_of_nhds` `eventuallyEq_one`
`le_one` 📖	mathematical	—	`Real` `Real.instLE` `DFunLike.coe` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `ContinuousMap.instFunLike` `BumpCovering` `instFunLikeContinuousMapReal` `Real.instOne`	—	`le_one'`
`le_one'` 📖	mathematical	—	`Pi.hasLe` `ContinuousMap` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Preorder.toLE` `PartialOrder.toPreorder` `ContinuousMap.partialOrder` `Real.partialOrder` `toFun` `Pi.instOne` `ContinuousMap.instOne` `Real.instOne`	—	—
`locallyFinite` 📖	mathematical	—	`LocallyFinite` `Function.support` `Real` `Real.instZero` `DFunLike.coe` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `ContinuousMap.instFunLike` `BumpCovering` `instFunLikeContinuousMapReal`	—	`locallyFinite'`
`locallyFinite'` 📖	mathematical	—	`LocallyFinite` `Function.support` `Real` `Real.instZero` `DFunLike.coe` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `ContinuousMap.instFunLike` `toFun`	—	—
`locallyFinite_tsupport` 📖	mathematical	—	`LocallyFinite` `tsupport` `Real` `Real.instZero` `DFunLike.coe` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `ContinuousMap.instFunLike` `BumpCovering` `instFunLikeContinuousMapReal`	—	`LocallyFinite.closure` `locallyFinite`
`nonneg` 📖	mathematical	—	`Real` `Real.instLE` `Real.instZero` `DFunLike.coe` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `ContinuousMap.instFunLike` `BumpCovering` `instFunLikeContinuousMapReal`	—	`nonneg'`
`nonneg'` 📖	mathematical	—	`Pi.hasLe` `ContinuousMap` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Preorder.toLE` `PartialOrder.toPreorder` `ContinuousMap.partialOrder` `Real.partialOrder` `Pi.instZero` `ContinuousMap.instZero` `Real.instZero` `toFun`	—	—
`point_finite` 📖	mathematical	—	`Set.Finite` `setOf` `Real` `DFunLike.coe` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `ContinuousMap.instFunLike` `BumpCovering` `instFunLikeContinuousMapReal` `Real.instZero`	—	`LocallyFinite.point_finite` `locallyFinite`
`sum_toPOUFun_eq` 📖	mathematical	—	`finsum` `Real` `Real.instAddCommMonoid` `toPOUFun` `Real.instSub` `Real.instOne` `finprod` `Real.instCommMonoid` `DFunLike.coe` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `ContinuousMap.instFunLike` `BumpCovering` `instFunLikeContinuousMapReal`	—	`point_finite` `Set.Finite.coe_toFinset` `support_toPOUFun_subset` `Function.mulSupport_one_sub` `finsum_eq_sum_of_support_subset` `finprod_eq_prod_of_mulSupport_subset` `instIsStrictTotalOrderOfIsWellOrder` `WellOrderingRel.isWellOrder` `Finset.prod_one_sub_ordered` `sub_sub_cancel` `Finset.sum_congr` `Finset.prod_congr` `Lean.Meta.FastSubsingleton.elim` `Lean.Meta.instFastSubsingletonForall` `Lean.Meta.instFastSubsingletonDecidable` `toPOUFun_eq_mul_prod` `Set.Finite.mem_toFinset`
`sum_toPartitionOfUnity_eq` 📖	mathematical	—	`finsum` `Real` `Real.instAddCommMonoid` `DFunLike.coe` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `ContinuousMap.instFunLike` `PartitionOfUnity` `PartitionOfUnity.instFunLikeContinuousMapReal` `toPartitionOfUnity` `Real.instSub` `Real.instOne` `finprod` `Real.instCommMonoid` `BumpCovering` `instFunLikeContinuousMapReal`	—	`sum_toPOUFun_eq`
`support_toPOUFun_subset` 📖	mathematical	—	`Set` `Set.instHasSubset` `Function.support` `Real` `Real.instZero` `toPOUFun` `DFunLike.coe` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `ContinuousMap.instFunLike` `BumpCovering` `instFunLikeContinuousMapReal`	—	`toPOUFun_zero_of_zero`
`support_toPartitionOfUnity_subset` 📖	mathematical	—	`Set` `Set.instHasSubset` `Function.support` `Real` `Real.instZero` `DFunLike.coe` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `ContinuousMap.instFunLike` `PartitionOfUnity` `PartitionOfUnity.instFunLikeContinuousMapReal` `toPartitionOfUnity` `BumpCovering` `instFunLikeContinuousMapReal`	—	`support_toPOUFun_subset`
`toFun_eq_coe` 📖	mathematical	—	`toFun` `DFunLike.coe` `BumpCovering` `ContinuousMap` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `instFunLikeContinuousMapReal`	—	—
`toPOUFun_eq_mul_prod` 📖	mathematical	`Finset` `Finset.instMembership`	`toPOUFun` `Real` `Real.instMul` `DFunLike.coe` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `ContinuousMap.instFunLike` `BumpCovering` `instFunLikeContinuousMapReal` `Finset.prod` `Real.instCommMonoid` `Finset.filter` `WellOrderingRel` `Real.instSub` `Real.instOne`	—	`finprod_cond_eq_prod_of_cond_iff` `Finset.mem_filter` `sub_eq_self`
`toPOUFun_zero_of_zero` 📖	mathematical	`DFunLike.coe` `ContinuousMap` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `ContinuousMap.instFunLike` `BumpCovering` `instFunLikeContinuousMapReal` `Real.instZero`	`toPOUFun`	—	`toPOUFun.eq_1` `MulZeroClass.zero_mul`
`toPartitionOfUnity_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `ContinuousMap.instFunLike` `PartitionOfUnity` `PartitionOfUnity.instFunLikeContinuousMapReal` `toPartitionOfUnity` `Real.instMul` `BumpCovering` `instFunLikeContinuousMapReal` `finprod` `Real.instCommMonoid` `WellOrderingRel` `Real.instSub` `Real.instOne`	—	—
`toPartitionOfUnity_eq_mul_prod` 📖	mathematical	`Finset` `Finset.instMembership`	`DFunLike.coe` `ContinuousMap` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `ContinuousMap.instFunLike` `PartitionOfUnity` `PartitionOfUnity.instFunLikeContinuousMapReal` `toPartitionOfUnity` `Real.instMul` `BumpCovering` `instFunLikeContinuousMapReal` `Finset.prod` `Real.instCommMonoid` `Finset.filter` `WellOrderingRel` `Real.instSub` `Real.instOne`	—	`toPOUFun_eq_mul_prod`
`toPartitionOfUnity_zero_of_zero` 📖	mathematical	`DFunLike.coe` `ContinuousMap` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `ContinuousMap.instFunLike` `BumpCovering` `instFunLikeContinuousMapReal` `Real.instZero`	`PartitionOfUnity` `PartitionOfUnity.instFunLikeContinuousMapReal` `toPartitionOfUnity`	—	`toPOUFun_zero_of_zero`

BumpCovering.IsSubordinate

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mono` 📖	—	`BumpCovering.IsSubordinate` `Set` `Set.instHasSubset`	—	—	`Set.Subset.trans`
`toPartitionOfUnity` 📖	mathematical	`BumpCovering.IsSubordinate`	`PartitionOfUnity.IsSubordinate` `BumpCovering.toPartitionOfUnity`	—	`Set.Subset.trans` `closure_mono` `BumpCovering.support_toPartitionOfUnity_subset`

PartitionOfUnity

Definitions

Name	Category	Theorems
`IsSubordinate` 📖	MathDef	6 math math: `exists_isSubordinate_of_locallyFinite_t2space`, `exists_isSubordinate`, `SmoothPartitionOfUnity.IsSubordinate.toPartitionOfUnity`, `exists_isSubordinate_of_locallyFinite`, `BumpCovering.IsSubordinate.toPartitionOfUnity`, `SmoothPartitionOfUnity.isSubordinate_toPartitionOfUnity`
`finsupport` 📖	CompOp	6 math math: `coe_finsupport`, `eventually_finsupport_subset`, `sum_finsupport_smul_eq_finsum`, `finsupport_subset_fintsupport`, `sum_finsupport`, `mem_finsupport`
`fintsupport` 📖	CompOp	4 math math: `eventually_fintsupport_subset`, `eventually_finsupport_subset`, `finsupport_subset_fintsupport`, `mem_fintsupport_iff`
`instFunLikeContinuousMapReal` 📖	CompOp	32 math math: `BumpCovering.toPartitionOfUnity_apply`, `BumpCovering.toPartitionOfUnity_zero_of_zero`, `locallyFinite`, `exists_finset_nhds`, `IsSubordinate.continuous_finsum_smul`, `BumpCovering.contMDiff_toPartitionOfUnity`, `coe_finsupport`, `exists_finset_nhds_support_subset`, `sum_eq_one`, `BumpCovering.toPartitionOfUnity_eq_mul_prod`, `exists_isSubordinate_of_locallyFinite_t2space`, `finsum_smul_mem_convex`, `nonneg`, `sum_finsupport_smul_eq_finsum`, `BumpCovering.exists_finset_toPartitionOfUnity_eventuallyEq`, `locallyFinite_tsupport`, `continuous_finsum_smul`, `BumpCovering.sum_toPartitionOfUnity_eq`, `sum_le_one`, `le_one`, `sum_nonneg`, `BumpCovering.coe_toSmoothPartitionOfUnity`, `finite_tsupport`, `mem_fintsupport_iff`, `SmoothPartitionOfUnity.toPartitionOfUnity_toFun`, `exists_finset_nhds'`, `exists_pos`, `continuous_smul`, `sum_finsupport'`, `sum_finsupport`, `BumpCovering.support_toPartitionOfUnity_subset`, `mem_finsupport`
`instInhabited` 📖	CompOp	—
`toFun` 📖	CompOp	4 math math: `nonneg'`, `sum_eq_one'`, `sum_le_one'`, `locallyFinite'`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_finsupport` 📖	mathematical	—	`SetLike.coe` `Finset` `Finset.instSetLike` `finsupport` `Function.support` `Real` `Real.instZero` `DFunLike.coe` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `ContinuousMap.instFunLike` `PartitionOfUnity` `instFunLikeContinuousMapReal`	—	`Set.ext` `Finset.mem_coe` `mem_finsupport`
`continuous_finsum_smul` 📖	mathematical	`ContinuousAt`	`Continuous` `finsum` `Real` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `SMulWithZero.toSMulZeroClass` `Real.instZero` `DFunLike.coe` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `ContinuousMap.instFunLike` `PartitionOfUnity` `instFunLikeContinuousMapReal`	—	`continuous_finsum` `continuous_smul` `LocallyFinite.subset` `locallyFinite` `Function.support_smul_subset_left`
`continuous_smul` 📖	mathematical	`ContinuousAt`	`Continuous` `Real` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `SMulWithZero.toSMulZeroClass` `Real.instZero` `DFunLike.coe` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `ContinuousMap.instFunLike` `PartitionOfUnity` `instFunLikeContinuousMapReal`	—	`continuous_of_tsupport` `ContinuousAt.smul` `ContinuousMap.continuousAt` `tsupport_smul_subset_left`
`eventually_finsupport_subset` 📖	mathematical	—	`Filter.Eventually` `Finset` `Finset.instHasSubset` `finsupport` `fintsupport` `nhds`	—	`Filter.Eventually.mono` `eventually_fintsupport_subset` `HasSubset.Subset.trans` `Finset.instIsTransSubset` `finsupport_subset_fintsupport`
`eventually_fintsupport_subset` 📖	mathematical	—	`Filter.Eventually` `Finset` `Finset.instHasSubset` `fintsupport` `nhds`	—	`Filter.Eventually.mono` `LocallyFinite.eventually_subset` `LocallyFinite.closure` `locallyFinite` `isClosed_closure` `mem_fintsupport_iff`
`exists_finset_nhds` 📖	mathematical	—	`Filter.Eventually` `Real` `Finset.sum` `Real.instAddCommMonoid` `DFunLike.coe` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `ContinuousMap.instFunLike` `PartitionOfUnity` `Set.univ` `instFunLikeContinuousMapReal` `Real.instOne` `Set` `Set.instHasSubset` `Function.support` `Real.instZero` `SetLike.coe` `Finset` `Finset.instSetLike` `nhds`	—	`exists_finset_nhds'` `Filter.eventually_and` `nhdsWithin_univ`
`exists_finset_nhds'` 📖	mathematical	—	`Filter.Eventually` `Real` `Finset.sum` `Real.instAddCommMonoid` `DFunLike.coe` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `ContinuousMap.instFunLike` `PartitionOfUnity` `instFunLikeContinuousMapReal` `Real.instOne` `nhdsWithin` `Set` `Set.instHasSubset` `Function.support` `Real.instZero` `SetLike.coe` `Finset` `Finset.instSetLike` `nhds`	—	`LocallyFinite.exists_finset_support` `locallyFinite` `eventually_nhdsWithin_iff` `Filter.Eventually.mono` `finsum_eq_sum_of_support_subset` `sum_eq_one`
`exists_finset_nhds_support_subset` 📖	mathematical	`IsSubordinate` `IsOpen`	`Set` `Filter` `Filter.instMembership` `nhds` `Set.instHasSubset` `Set.iInter` `Finset` `Finset.instMembership` `Function.support` `Real` `Real.instZero` `DFunLike.coe` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `ContinuousMap.instFunLike` `PartitionOfUnity` `instFunLikeContinuousMapReal` `SetLike.coe` `Finset.instSetLike`	—	`LocallyFinite.exists_finset_nhds_support_subset` `locallyFinite`
`exists_isSubordinate` 📖	mathematical	`IsOpen` `Set` `Set.instHasSubset` `Set.iUnion`	`IsSubordinate`	—	`BumpCovering.exists_isSubordinate` `BumpCovering.IsSubordinate.toPartitionOfUnity`
`exists_isSubordinate_of_locallyFinite` 📖	mathematical	`IsOpen` `LocallyFinite` `Set` `Set.instHasSubset` `Set.iUnion`	`IsSubordinate`	—	`BumpCovering.exists_isSubordinate_of_locallyFinite` `BumpCovering.IsSubordinate.toPartitionOfUnity`
`exists_isSubordinate_of_locallyFinite_t2space` 📖	mathematical	`IsCompact` `IsOpen` `LocallyFinite` `Set` `Set.instHasSubset` `Set.iUnion`	`IsSubordinate` `HasCompactSupport` `Real` `Real.instZero` `DFunLike.coe` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `ContinuousMap.instFunLike` `PartitionOfUnity` `instFunLikeContinuousMapReal`	—	`BumpCovering.exists_isSubordinate_hasCompactSupport_of_locallyFinite_t2space` `BumpCovering.IsSubordinate.toPartitionOfUnity` `IsCompact.of_isClosed_subset` `isClosed_closure` `closure_mono` `BumpCovering.support_toPartitionOfUnity_subset`
`exists_pos` 📖	mathematical	`Set` `Set.instMembership`	`Real` `Real.instLT` `Real.instZero` `DFunLike.coe` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `ContinuousMap.instFunLike` `PartitionOfUnity` `instFunLikeContinuousMapReal`	—	`sum_eq_one` `Mathlib.Tactic.Contrapose.contrapose₁` `LE.le.antisymm` `nonneg` `finsum_zero` `zero_ne_one` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing`
`finite_tsupport` 📖	mathematical	—	`Set.Finite` `setOf` `Set` `Set.instMembership` `tsupport` `Real` `Real.instZero` `DFunLike.coe` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `ContinuousMap.instFunLike` `PartitionOfUnity` `instFunLikeContinuousMapReal`	—	`locallyFinite` `Set.Finite.subset` `Set.inter_comm` `mem_closure_iff_nhds`
`finsupport_subset_fintsupport` 📖	mathematical	—	`Finset` `Finset.instHasSubset` `finsupport` `fintsupport`	—	`mem_fintsupport_iff` `subset_closure` `mem_finsupport`
`le_one` 📖	mathematical	—	`Real` `Real.instLE` `DFunLike.coe` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `ContinuousMap.instFunLike` `PartitionOfUnity` `instFunLikeContinuousMapReal` `Real.instOne`	—	`LE.le.trans` `single_le_finsum` `Real.instIsOrderedAddMonoid` `LocallyFinite.point_finite` `locallyFinite` `nonneg` `sum_le_one`
`locallyFinite` 📖	mathematical	—	`LocallyFinite` `Function.support` `Real` `Real.instZero` `DFunLike.coe` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `ContinuousMap.instFunLike` `PartitionOfUnity` `instFunLikeContinuousMapReal`	—	`locallyFinite'`
`locallyFinite'` 📖	mathematical	—	`LocallyFinite` `Function.support` `Real` `Real.instZero` `DFunLike.coe` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `ContinuousMap.instFunLike` `toFun`	—	—
`locallyFinite_tsupport` 📖	mathematical	—	`LocallyFinite` `tsupport` `Real` `Real.instZero` `DFunLike.coe` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `ContinuousMap.instFunLike` `PartitionOfUnity` `instFunLikeContinuousMapReal`	—	`LocallyFinite.closure` `locallyFinite`
`mem_finsupport` 📖	mathematical	—	`Finset` `Finset.instMembership` `finsupport` `Set` `Set.instMembership` `Function.support` `Real` `Real.instZero` `DFunLike.coe` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `ContinuousMap.instFunLike` `PartitionOfUnity` `instFunLikeContinuousMapReal`	—	`Set.Finite.toFinset.congr_simp`
`mem_fintsupport_iff` 📖	mathematical	—	`Finset` `Finset.instMembership` `fintsupport` `Set` `Set.instMembership` `tsupport` `Real` `Real.instZero` `DFunLike.coe` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `ContinuousMap.instFunLike` `PartitionOfUnity` `instFunLikeContinuousMapReal`	—	`Set.Finite.mem_toFinset` `finite_tsupport`
`nonneg` 📖	mathematical	—	`Real` `Real.instLE` `Real.instZero` `DFunLike.coe` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `ContinuousMap.instFunLike` `PartitionOfUnity` `instFunLikeContinuousMapReal`	—	`nonneg'`
`nonneg'` 📖	mathematical	—	`Pi.hasLe` `ContinuousMap` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Preorder.toLE` `PartialOrder.toPreorder` `ContinuousMap.partialOrder` `Real.partialOrder` `Pi.instZero` `ContinuousMap.instZero` `Real.instZero` `toFun`	—	—
`sum_eq_one` 📖	mathematical	`Set` `Set.instMembership`	`finsum` `Real` `Real.instAddCommMonoid` `DFunLike.coe` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `ContinuousMap.instFunLike` `PartitionOfUnity` `instFunLikeContinuousMapReal` `Real.instOne`	—	`sum_eq_one'`
`sum_eq_one'` 📖	mathematical	`Set` `Set.univ` `Set.instMembership`	`finsum` `Real` `Real.instAddCommMonoid` `DFunLike.coe` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `ContinuousMap.instFunLike` `toFun` `Real.instOne`	—	—
`sum_finsupport` 📖	mathematical	`Set` `Set.instMembership`	`Finset.sum` `Real` `Real.instAddCommMonoid` `finsupport` `DFunLike.coe` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `ContinuousMap.instFunLike` `PartitionOfUnity` `instFunLikeContinuousMapReal` `Real.instOne`	—	`sum_eq_one` `finsum_eq_sum_of_support_subset` `Eq.superset` `Set.instReflSubset` `coe_finsupport`
`sum_finsupport'` 📖	mathematical	`Set` `Set.instMembership` `Finset` `Finset.instHasSubset` `finsupport`	`Finset.sum` `Real` `Real.instAddCommMonoid` `DFunLike.coe` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `ContinuousMap.instFunLike` `PartitionOfUnity` `instFunLikeContinuousMapReal` `Real.instOne`	—	`Finset.sum_sdiff` `sum_finsupport` `Finset.sum_congr` `mem_finsupport` `add_eq_right` `AddRightCancelSemigroup.toIsRightCancelAdd` `Finset.sum_const_zero`
`sum_finsupport_smul_eq_finsum` 📖	mathematical	—	`Finset.sum` `finsupport` `Real` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `DFunLike.coe` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `ContinuousMap.instFunLike` `PartitionOfUnity` `instFunLikeContinuousMapReal` `finsum`	—	`finsum_eq_sum_of_support_subset` `Pi.smul_apply'` `coe_finsupport` `Function.support_smul` `Real.instIsDomain` `DivisionSemiring.to_moduleIsTorsionFree` `Set.inter_subset_left`
`sum_le_one` 📖	mathematical	—	`Real` `Real.instLE` `finsum` `Real.instAddCommMonoid` `DFunLike.coe` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `ContinuousMap.instFunLike` `PartitionOfUnity` `instFunLikeContinuousMapReal` `Real.instOne`	—	`sum_le_one'`
`sum_le_one'` 📖	mathematical	—	`Real` `Real.instLE` `finsum` `Real.instAddCommMonoid` `DFunLike.coe` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `ContinuousMap.instFunLike` `toFun` `Real.instOne`	—	—
`sum_nonneg` 📖	mathematical	—	`Real` `Real.instLE` `Real.instZero` `finsum` `Real.instAddCommMonoid` `DFunLike.coe` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `ContinuousMap.instFunLike` `PartitionOfUnity` `instFunLikeContinuousMapReal`	—	`finsum_nonneg` `Real.instIsOrderedAddMonoid` `nonneg`

PartitionOfUnity.IsSubordinate

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuous_finsum_smul` 📖	mathematical	`IsOpen` `PartitionOfUnity.IsSubordinate` `ContinuousOn`	`Continuous` `finsum` `Real` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `SMulWithZero.toSMulZeroClass` `Real.instZero` `DFunLike.coe` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `ContinuousMap.instFunLike` `PartitionOfUnity` `PartitionOfUnity.instFunLikeContinuousMapReal`	—	`PartitionOfUnity.continuous_finsum_smul` `ContinuousOn.continuousAt` `IsOpen.mem_nhds`

(root)

Definitions

Name	Category	Theorems
`BumpCovering` 📖	CompData	22 math math: `BumpCovering.eventuallyEq_one`, `BumpCovering.toPartitionOfUnity_apply`, `BumpCovering.point_finite`, `BumpCovering.support_toPOUFun_subset`, `BumpCovering.le_one`, `BumpCovering.exists_isSubordinate_of_prop`, `BumpCovering.toPartitionOfUnity_eq_mul_prod`, `BumpCovering.locallyFinite`, `BumpCovering.exists_finset_toPartitionOfUnity_eventuallyEq`, `BumpCovering.locallyFinite_tsupport`, `BumpCovering.toFun_eq_coe`, `BumpCovering.exists_isSubordinate_of_locallyFinite_of_prop_t2space`, `BumpCovering.ind_apply`, `BumpCovering.sum_toPartitionOfUnity_eq`, `BumpCovering.exists_isSubordinate_of_locallyFinite_of_prop`, `BumpCovering.nonneg`, `BumpCovering.exists_finset_toPOUFun_eventuallyEq`, `BumpCovering.toPOUFun_eq_mul_prod`, `BumpCovering.exists_isSubordinate_hasCompactSupport_of_locallyFinite_t2space`, `BumpCovering.sum_toPOUFun_eq`, `BumpCovering.coe_single`, `BumpCovering.support_toPartitionOfUnity_subset`
`PartitionOfUnity` 📖	CompData	32 math math: `BumpCovering.toPartitionOfUnity_apply`, `BumpCovering.toPartitionOfUnity_zero_of_zero`, `PartitionOfUnity.locallyFinite`, `PartitionOfUnity.exists_finset_nhds`, `PartitionOfUnity.IsSubordinate.continuous_finsum_smul`, `BumpCovering.contMDiff_toPartitionOfUnity`, `PartitionOfUnity.coe_finsupport`, `PartitionOfUnity.exists_finset_nhds_support_subset`, `PartitionOfUnity.sum_eq_one`, `BumpCovering.toPartitionOfUnity_eq_mul_prod`, `PartitionOfUnity.exists_isSubordinate_of_locallyFinite_t2space`, `PartitionOfUnity.finsum_smul_mem_convex`, `PartitionOfUnity.nonneg`, `PartitionOfUnity.sum_finsupport_smul_eq_finsum`, `BumpCovering.exists_finset_toPartitionOfUnity_eventuallyEq`, `PartitionOfUnity.locallyFinite_tsupport`, `PartitionOfUnity.continuous_finsum_smul`, `BumpCovering.sum_toPartitionOfUnity_eq`, `PartitionOfUnity.sum_le_one`, `PartitionOfUnity.le_one`, `PartitionOfUnity.sum_nonneg`, `BumpCovering.coe_toSmoothPartitionOfUnity`, `PartitionOfUnity.finite_tsupport`, `PartitionOfUnity.mem_fintsupport_iff`, `SmoothPartitionOfUnity.toPartitionOfUnity_toFun`, `PartitionOfUnity.exists_finset_nhds'`, `PartitionOfUnity.exists_pos`, `PartitionOfUnity.continuous_smul`, `PartitionOfUnity.sum_finsupport'`, `PartitionOfUnity.sum_finsupport`, `BumpCovering.support_toPartitionOfUnity_subset`, `PartitionOfUnity.mem_finsupport`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_continuous_sum_one_of_isOpen_isCompact` 📖	mathematical	`IsOpen` `IsCompact` `Set` `Set.instHasSubset` `Set.iUnion`	`tsupport` `Real` `Real.instZero` `DFunLike.coe` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `ContinuousMap.instFunLike` `Set.EqOn` `Finset.sum` `Pi.addCommMonoid` `Real.instAddCommMonoid` `Finset.univ` `Fin.fintype` `Pi.instOne` `Real.instOne` `Set.instMembership` `Set.Icc` `Real.instPreorder` `HasCompactSupport`	—	`PartitionOfUnity.exists_isSubordinate_of_locallyFinite_t2space` `locallyFinite_of_finite` `Finite.of_fintype` `Finset.sum_apply` `PartitionOfUnity.sum_eq_one'` `Set.Finite.subset` `Set.finite_univ` `Set.subset_univ` `Fintype.sum_subset` `Set.Finite.toFinset_setOf` `finsum_eq_sum` `PartitionOfUnity.nonneg` `PartitionOfUnity.le_one`

---

← Back to Index