Theorems · Definition · convex and discrete geometry

stdSimplex

(𝕜 : Type u_2) → (ι : Type u_1) → [Semiring 𝕜] → [PartialOrder 𝕜] → [Fintype ι] → Set (ι → 𝕜)

The standard simplex in the space of functions ι → 𝕜 is the set of vectors with non-negative coordinates with total sum 1. This is the free object in the category of convex spaces.

Defined in

Mathlib.Analysis.Convex.StdSimplex

Cited by

76 results in Mathlib

Foundations

Depth 14 from the axioms · uses propext, Quot.sound

Assumes

SemiringPartialOrderFintype