The Minkowski-Carathéodory theorem

theorem convexHull_extremePoints {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E} (hscomp : IsCompact s) (hsconv : Convex ℝ s) : (convexHull ℝ) (Set.extremePoints ℝ s) = s

The Minkowski-Carathéodory Theorem. A compact convex set in a finite dimensional space is the convex hull of its extreme points.

theorem closed_convexHull_extremePoints_of_compact_of_convex {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E} (hscomp : IsCompact s) (hsconv : Convex ℝ s) : IsClosed ((convexHull ℝ) (Set.extremePoints ℝ s))