Theorem: extremePoints_subset_closure_exposedPoints (LeanCamCombi/Mathlib/Analysis/Convex/Exposed.lean)

State before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
s t C : Set E
X : Finset E
l : E →L[ℝ] ℝ
hs₁ : Convex ℝ s
hs₂ : IsClosed s
⊢ extremePoints ℝ s ⊆ closure (exposedPoints ℝ s)
Tactic:
sorry
State after:
no goals