Theorems · Inductive type · convex and discrete geometry

Convexity.StdSimplex

(R : Type u) → [LE R] → [AddCommMonoid R] → [One R] → Type v → Type (max u v)

A finitely supported probability distribution over elements of M with coefficients in R. The weights are non-negative and sum to 1.

Defined in

Mathlib.Geometry.Convex.ConvexSpace.Defs

Cited by

123 results in Mathlib

Foundations

Depth 1 from the axioms, rests on 4 definitions · uses no axioms

Assumes

LEAddCommMonoidOne