Theorems · Definition · convex and discrete geometry

Convexity.StdSimplex.join

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

Join operation for standard simplices (monadic join). Given a distribution over distributions, flattens it to a single distribution. Use ConvexSpace.sConvexComb instead.

Defined in

Mathlib.Geometry.Convex.ConvexSpace.Defs

Cited by

4 results in Mathlib

Foundations

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

Assumes

PartialOrderSemiringIsStrictOrderedRing