exact combiInterior_subset_convexHull
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
s t : Finset E
inst✝ : T2Space E
hs : AffineIndependent ℝ Subtype.val
⊢ combiInterior ℝ s ⊆ (convexHull ℝ) ↑s
no goals