Theorem: closed_convexHull_extremePoints_of_compact_of_convex (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
⊢ closure ((convexHull ℝ) (extremePoints ℝ s)) = (convexHull ℝ) (extremePoints ℝ s)
Tactic:
rw [closure_convexHull_extremePoints hscomp hsconv, convexHull_extremePoints hscomp hsconv]
State after:
no goals