English
The standard simplex is a convex subset of the function space ι → 𝕜.
Русский
Стандартный симплекс является выпуклым подмножеством векторного пространства функций ι → 𝕜.
LaTeX
$$$\mathrm{Convex}_{\mathbb{k}}(\mathrm{stdSimplex}_{\mathbb{k}}(\iota))$$$
Lean4
theorem convex_stdSimplex [IsOrderedRing 𝕜] : Convex 𝕜 (stdSimplex 𝕜 ι) :=
by
refine fun f hf g hg a b ha hb hab => ⟨fun x => ?_, ?_⟩
· apply_rules [add_nonneg, mul_nonneg, hf.1, hg.1]
· simp_rw [Pi.add_apply, Pi.smul_apply]
rwa [Finset.sum_add_distrib, ← Finset.smul_sum, ← Finset.smul_sum, hf.2, hg.2, smul_eq_mul, smul_eq_mul, mul_one,
mul_one]