unfold combiInterior
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x : E
⊢ combiInterior 𝕜 {x} = {x}
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x : E
⊢ (convexHull 𝕜) ↑{x} \ combiFrontier 𝕜 {x} = {x}