Theorems · Theorem · convex and discrete geometry

Convexity.iConvexComb_eq_sum

∀ {R : Type u_2} {M : Type u_3} {I : Type u_5} [inst : Semiring R] [inst_1 : PartialOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Convexity.ConvexSpace R M]
  [Convexity.IsModuleConvexSpace R M] (w : Convexity.StdSimplex R I) (f : I → M),
  Convexity.iConvexComb w f = w.weights.sum fun i r => r • f i

iConvexComb in a module can be expressed as a sum.

Defined in

Mathlib.Geometry.Convex.ConvexSpace.Module

Cited by

9 results in Mathlib

Foundations

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

Assumes

SemiringPartialOrderIsStrictOrderedRingAddCommMonoidModuleConvexity.ConvexSpaceConvexity.IsModuleConvexSpace