PartitionOfUnity

📁 Source: Mathlib/Analysis/Convex/PartitionOfUnity.lean

Statistics

Metric	Count
Definitions	0
Theorems finsum_smul_mem_convex, exists_continuous_forall_mem_convex_of_local, exists_continuous_forall_mem_convex_of_local_const	3
Total	3

PartitionOfUnity

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finsum_smul_mem_convex 📖	mathematical	Set Set.instMembership Convex Real Real.semiring Real.partialOrder AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction	finsum DFunLike.coe ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.instFunLike PartitionOfUnity instFunLikeContinuousMapReal	—	Convex.finsum_mem Real.instIsStrictOrderedRing nonneg sum_eq_one

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_continuous_forall_mem_convex_of_local 📖	mathematical	Convex Real Real.semiring Real.partialOrder AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Set Filter Filter.instMembership nhds ContinuousOn Set.instMembership	DFunLike.coe ContinuousMap ContinuousMap.instFunLike	—	PartitionOfUnity.exists_isSubordinate isClosed_univ isOpen_interior Set.mem_iUnion mem_interior_iff_mem_nhds PartitionOfUnity.IsSubordinate.continuous_finsum_smul ContinuousOn.mono interior_subset PartitionOfUnity.finsum_smul_mem_convex Set.mem_univ subset_closure
exists_continuous_forall_mem_convex_of_local_const 📖	mathematical	Convex Real Real.semiring Real.partialOrder AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Filter.Eventually Set Set.instMembership nhds	DFunLike.coe ContinuousMap ContinuousMap.instFunLike	—	exists_continuous_forall_mem_convex_of_local continuousOn_const

---

← Back to Index