Theorem: Closed_Vpolytope (src/Polytope.lean)

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
S : Set E
hS : Set.Finite S
⊢ IsClosed (Vpolytope hS)
Tactic:
exact Set.Finite.isClosed_convexHull hS
State after:
no goals