English
Same as the previous item: the convex hull of a finite set equals the image of the standard simplex under a natural linear map.
Русский
То же самое, что и предыдущий пункт: выпуклая оболочка конечного множества равна образу стандартного симплекса под естественным линейным отображением.
LaTeX
$$$\operatorname{convexHull}_{R}(s) = (\sum_{x\in s} (\text{LinearMap.proj } x).smulRight(x))'' \mathrm{stdSimplex}_{R}(s)$$$
Lean4
/-- Every vector in `stdSimplex 𝕜 ι` has `max`-norm at most `1`. -/
theorem stdSimplex_subset_closedBall : stdSimplex ℝ ι ⊆ Metric.closedBall 0 1 := fun f hf ↦
by
rw [Metric.mem_closedBall, dist_pi_le_iff zero_le_one]
intro x
rw [Pi.zero_apply, Real.dist_0_eq_abs, abs_of_nonneg <| hf.1 x]
exact (mem_Icc_of_mem_stdSimplex hf x).2
