convex_stdSimplex — Mathlib

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]

Похожие утверждения