theorem Lemma_13_19_InteriorWeights.strictly_positive_stdSimplex_weighted_sum_mem_interior_convexHull {n l : ℕ} {a : Fin l → Fin n → ℝ} {w : Fin l → ℝ} (hΩ : (interior ((convexHull ℝ) (Set.range a))).Nonempty) (hw : w ∈ stdSimplex ℝ (Fin l)) (hwPos : ∀ (j : Fin l), 0 < w j) : ∑ j : Fin l, w j • a j ∈ interior ((convexHull ℝ) (Set.range a))

Helper for Lemma 13.19: a strictly positive simplex-weighted combination of the vertices lies in the interior of the finite convex hull whenever that convex hull has nonempty interior.