Theorems · Theorem · convex and discrete geometry
Convexity.StdSimplex.total
∀ {R : Type u} [inst : LE R] [inst_1 : AddCommMonoid R] [inst_2 : One R] {M : Type v} (self : Convexity.StdSimplex R M),
(self.weights.sum fun x r => r) = 1The weights sum to 1.
- Defined in
- Mathlib.Geometry.Convex.ConvexSpace.Defs
- Cited by
- 5 results in Mathlib
- Foundations
- Depth 60 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- LEAddCommMonoidOne
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- AddCommMonoidstatement and proof · cited by 12,281
- Finsupp.sumstatement · cited by 481
- Convexity.StdSimplexstatement and proof · cited by 123
- Convexity.StdSimplex.weightsstatement · cited by 63
Cited by5
Results whose statement or proof uses this declaration.
- Convexity.StdSimplex.map_constproof · cited by 4
- Convexity.IsConvexSet.imageproof · cited by 1
- AddTorsor.iConvexComb_eq_affineCombinationproof · cited by 0
- Convexity.StdSimplex.support_weights_eq_singletonproof · cited by 0
- AddTorsor.convexCombination_assocproof · cited by 0