theorem isClosed_convex_eq_iInter_halfSpaces (n : ℕ) (C : Set (Fin n → ℝ)) (hCconv : Convex ℝ C) (hCclosed : IsClosed C) : ⋂ (l : StrongDual ℝ (Fin n → ℝ)), {x : Fin n → ℝ | ∃ y ∈ C, l x ≤ l y} = C

Theorem 11.5: A closed convex set C is the intersection of the closed half-spaces which contain it.

In mathlib, a convenient way to express the closed half-spaces containing C is to quantify over continuous linear functionals l : StrongDual ℝ (Fin n → ℝ) and consider the half-space {x | ∃ y ∈ C, l x ≤ l y}.

theorem closure_convexHull_isClosed (n : ℕ) (S : Set (Fin n → ℝ)) : IsClosed (closure ((convexHull ℝ) S))

closure (convexHull ℝ S) is a closed set.

theorem closure_convexHull_convex (n : ℕ) (S : Set (Fin n → ℝ)) : Convex ℝ (closure ((convexHull ℝ) S))

closure (convexHull ℝ S) is a convex set.

theorem closure_convexHull_eq_iInter_halfSpaces (n : ℕ) (S : Set (Fin n → ℝ)) : closure ((convexHull ℝ) S) = ⋂ (l : StrongDual ℝ (Fin n → ℝ)), {x : Fin n → ℝ | ∃ y ∈ closure ((convexHull ℝ) S), l x ≤ l y}

Corollary 11.5.1. Let S be any subset of ℝ^n. Then cl (conv S) (i.e. closure (convexHull ℝ S)) is the intersection of all the closed half-spaces containing S.