Theorem: convexHull_extremePoints (LeanCamCombi/MinkowskiCaratheodory.lean)

State before:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
x : E
s B : Set E
hscomp : IsCompact s
hsconv : Convex ℝ s
⊢ (convexHull ℝ) (extremePoints ℝ s) = s
Tactic:
sorry
State after:
no goals