Theorems · Definition · convex and discrete geometry

Convexity.StdSimplex.map

{R : Type u} →
  [inst : PartialOrder R] →
    [inst_1 : Semiring R] →
      [IsStrictOrderedRing R] →
        {M : Type v} → {N : Type w} → (M → N) → Convexity.StdSimplex R M → Convexity.StdSimplex R N

Map a function over the support of a standard simplex. For each n : N, the weight is the sum of weights of all m : M with g m = n.

Defined in

Mathlib.Geometry.Convex.ConvexSpace.Defs

Cited by

43 results in Mathlib

Foundations

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

Assumes

PartialOrderSemiringIsStrictOrderedRing