Math.Simplex

6 nodes 3 formalized 3 proved

Lemma Continuity on the Real Standard Simplex proved

Definition Convex Combination of Simplex Points formalized

Lemma Iterated Weighted Sums Commute proved

Definition Point Mass on the Standard Simplex formalized

Lemma Pointwise Bounds Are Simplex Bounds proved

Definition Weighted Sum over the Standard Simplex formalized