convexHull_rangle_single_eq_stdSimplex

English

This is the formal statement that the convex hull of the canonical basis equals the standard simplex; in particular, conv{Pi.single i 1 | i ∈ ι} = stdSimplex R ι.

Русский

Формулируется равенство выпуклой оболочки канонических базисов и стандартного симплекса: conv{e_i | i ∈ ι} = stdSimplex R ι.

LaTeX

$$$\operatorname{convexHull}_{R}\big(\operatorname{range}(\lambda i. \Pi\text{single } i 1)\big) = \mathrm{stdSimplex}_{R}(ι)$$$

Lean4

/-- `stdSimplex 𝕜 ι` is the convex hull of the points `Pi.single i 1` for `i : `i`. -/
theorem convexHull_rangle_single_eq_stdSimplex [DecidableEq ι] :
    convexHull R (range fun i : ι ↦ Pi.single i 1) = stdSimplex R ι :=
  by
  convert convexHull_basis_eq_stdSimplex R ι
  aesop

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