Theorems · Theorem · convex and discrete geometry

Convexity.StdSimplex.mk_single

∀ {R : Type u} [inst : PartialOrder R] [inst_1 : Semiring R] {M : Type u_9} [inst_2 : IsStrictOrderedRing R] (x : M)
  {nonneg : 0 ≤ fun₀ | x => 1} {total : ((fun₀ | x => 1).sum fun x r => r) = 1},
  { weights := fun₀ | x => 1, nonneg := nonneg, total := total } = Convexity.StdSimplex.single x

Defined in

Mathlib.Geometry.Convex.ConvexSpace.Defs

Cited by

0 results in Mathlib

Foundations

Depth 72 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

PartialOrderSemiringIsStrictOrderedRing