Simplices are convex polyhedra

The convex hull of an affinely independent family in a finite-dimensional real normed space is a convex polyhedron. This includes simplices of positive codimension: coordinates outside the chosen face vanish, rather than merely being nonnegative. Consequently the simplices of a geometric simplicial complex can serve as the polyhedral cells of a piecewise-affine map.

The construction uses Mathlib's extension of an affinely independent set to an affine basis and its barycentric-coordinate description of the convex hull. The half-space description of a simplex follows Rourke--Sanderson, Introduction to Piecewise-Linear Topology, Chapter 1.

theorem AffineBasis.isConvexPolyhedron_convexHull_image {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {ι : Type u_2} (b : AffineBasis ι ℝ E) (s : Set ι) : TauCeti.IsConvexPolyhedron ((convexHull ℝ) (⇑b '' s))

Every face of the simplex spanned by an affine basis is a convex polyhedron, including the empty face and faces of positive codimension.

theorem AffineIndependent.isConvexPolyhedron_convexHull {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E} (hs : AffineIndependent ℝ Subtype.val) : TauCeti.IsConvexPolyhedron ((convexHull ℝ) s)

An affinely independent set in a finite-dimensional real normed space spans a convex polyhedron. No assumption that its affine span is the whole ambient space is needed.