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	Set Set.instMembership finsum AddCommGroup.toAddCommMonoid Real SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring 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	ContinuousMap Set Set.instMembership DFunLike.coe 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	ContinuousMap Set Set.instMembership DFunLike.coe ContinuousMap.instFunLike	—	exists_continuous_forall_mem_convex_of_local continuousOn_const

---

← Back to Index