theorem closedConvexHull_eq_iInter_closed_convex_supersets {𝓗 : Type u} [NormedAddCommGroup 𝓗] [InnerProductSpace ℝ 𝓗] (C : Set 𝓗) : (closedConvexHull ℝ) C = ⋂ (D : Set 𝓗), ⋂ (_ : C ⊆ D), ⋂ (_ : Convex ℝ D), ⋂ (_ : IsClosed D), D

The closed convex hull of C is the intersection of all closed convex subsets of the ambient Hilbert space that contain C.