English
The convex hull of the canonical basis vectors in ι → R equals the standard simplex: conv{Pi.single i 1 | i ∈ ι} = stdSimplex R ι.
Русский
выпуклая оболочка канонических векторов-базисов в ι → R равна стандартному симплексу: conv {e_i} = stdSimplex R ι.
LaTeX
$$$\operatorname{convexHull}_{R}\big(\{ \Pi\text{single } i\ 1 \,|\, i \in ι\} \big) = \mathrm{stdSimplex}_{R}(ι)$$$
Lean4
/-- `stdSimplex 𝕜 ι` is the convex hull of the canonical basis in `ι → 𝕜`. -/
theorem convexHull_basis_eq_stdSimplex [DecidableEq ι] :
convexHull R (range fun i j : ι => if i = j then (1 : R) else 0) = stdSimplex R ι :=
by
refine Subset.antisymm (convexHull_min ?_ (convex_stdSimplex R ι)) ?_
· rintro _ ⟨i, rfl⟩
exact ite_eq_mem_stdSimplex R i
· rintro w ⟨hw₀, hw₁⟩
rw [pi_eq_sum_univ w]
rw [← Finset.univ.centerMass_eq_of_sum_1 _ hw₁]
exact Finset.univ.centerMass_mem_convexHull (fun i _ => hw₀ i) (hw₁.symm ▸ zero_lt_one) fun i _ => mem_range_self i
