rw [Finset.coe_empty, convexHull_empty]
case h.e'_4
𝕜 : 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 𝕜) ↑∅
no goals