English
The standard simplex is the intersection of the coordinate-wise nonnegativity constraints with the total-sum constraint: it equals (⋂ x ∈ ι { f : ι → 𝕜 | 0 ≤ f(x) }) ∩ { f : ι → 𝕜 | ∑_{x ∈ ι} f(x) = 1 }.
Русский
Стандартный симплекс – это пересечение ограничений неотрицательности координат и условия, что сумма координат равна 1: он равен (⋂ 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
theorem stdSimplex_eq_inter : stdSimplex 𝕜 ι = (⋂ x, {f | 0 ≤ f x}) ∩ {f | ∑ x, f x = 1} :=
by
ext f
simp only [stdSimplex, Set.mem_inter_iff, Set.mem_iInter, Set.mem_setOf_eq]
