Theorems · Definition · convex and discrete geometry

Convexity.StdSimplex.duple

{R : Type u} →
  [inst : PartialOrder R] →
    [inst_1 : Semiring R] →
      {M : Type u_9} →
        [IsStrictOrderedRing R] → M → M → {s t : R} → 0 ≤ s → 0 ≤ t → s + t = 1 → Convexity.StdSimplex R M

A probability distribution with weight s on x and weight t on y.

Defined in

Mathlib.Geometry.Convex.ConvexSpace.Defs

Cited by

20 results in Mathlib

Foundations

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

Assumes

PartialOrderSemiringIsStrictOrderedRing