English
The standard simplex is the intersection of the nonnegative coordinate half-spaces with the sum-equals-one hyperplane: stdSimplex 𝕜 ι = (⋂ x, {f : ι → 𝕜 | 0 ≤ f x}) ∩ {f : ι → 𝕜 | ∑ x, f x = 1}.
Русский
Стандартный симплекс — это пересечение полуплощадок неотрицательности координат и гиперплоскости суммы равной единице.
LaTeX
$$$\mathrm{stdSimplex}_{\mathbb{k}}(\iota) = \Bigl( \bigcap_{x \in\iota} \{ f: \iota \to \mathbb{k} \mid 0 \le f(x) \} \Bigr) \cap \{ f: \iota \to \mathbb{k} \mid \sum_{x \in \iota} f(x) = 1 \}$$$
Lean4
/-- All values of a function `f ∈ stdSimplex 𝕜 ι` belong to `[0, 1]`. -/
theorem mem_Icc_of_mem_stdSimplex [IsOrderedAddMonoid 𝕜] {f : ι → 𝕜} (hf : f ∈ stdSimplex 𝕜 ι) (x) :
f x ∈ Icc (0 : 𝕜) 1 :=
⟨hf.1 x, hf.2 ▸ Finset.single_le_sum (fun y _ => hf.1 y) (Finset.mem_univ x)⟩
