English
Let ι be a finite index set and 𝕜 a semiring with a partial order. The standard simplex in ι → 𝕜 consists of all functions f: ι → 𝕜 such that f(x) ≥ 0 for every x and the sum over x ∈ ι of f(x) equals 1.
Русский
Пусть ι — конечный индексный набор, а 𝕜 — полукольцо с частичным порядком. Стандартный симплекс в пространстве функций ι → 𝕜 состоит из всех функций f: ι → 𝕜, для которых f(x) ≥ 0 для всех x и сумма по x ∈ ι равна 1.
LaTeX
$$$\mathrm{stdSimplex}_{\mathbb{k}}(\iota) = \{ f: \iota \to \mathbb{k} \mid (\forall x \in \iota, \; f(x) \ge 0) \land (\sum_{x \in \iota} f(x) = 1) \}$$$
Lean4
/-- 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. -/
def stdSimplex : Set (ι → 𝕜) :=
{f | (∀ x, 0 ≤ f x) ∧ ∑ x, f x = 1}
