Theorems · Definition · convex and discrete geometry

Convexity.iConvexComb

{R : Type u_1} →
  {M : Type u_3} →
    {I : Type u_6} →
      [inst : PartialOrder R] →
        [inst_1 : Semiring R] →
          [inst_2 : IsStrictOrderedRing R] → [Convexity.ConvexSpace R M] → Convexity.StdSimplex R I → (I → M) → M

Take a convex combination with the given weight distribution of an indexed family of points.

Defined in

Mathlib.Geometry.Convex.ConvexSpace.Defs

Cited by

51 results in Mathlib

Foundations

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

Assumes

PartialOrderSemiringIsStrictOrderedRingConvexity.ConvexSpace