A polytope is the convex hull of its vertices

This finite-dimensional consequence of Krein--Milman is used when a hollow rational polytope is converted into a finite p-hollow family.

theorem EGZ.RationalPolytope.carrier_eq_convexHull_vertexSet {d : ℕ} (P : RationalPolytope d) : P.carrier = (convexHull ℝ) P.vertexSet

The convex hull of the actual extreme points of a rational polytope is the whole polytope, even when its stored generating finset is redundant.

theorem EGZ.RationalPolytope.mem_convexHull_vertexSet {d : ℕ} (P : RationalPolytope d) {q : RealCoord d} (hq : q ∈ P.carrier) : q ∈ (convexHull ℝ) P.vertexSet

Every point of a polytope is a convex combination of its vertices.