Polyhedral boxes in finite coordinate spaces

Coordinate boxes are convex polyhedra. Consequently the closed balls for the supremum metric on a finite real coordinate space are convex polyhedra. These balls give polyhedral neighbourhoods when restricting local PL decompositions.

theorem TauCeti.isConvexPolyhedron_pi_Icc {ι : Type u_1} [Finite ι] (a b : ι → ℝ) : IsConvexPolyhedron (Set.univ.pi fun (i : ι) => Set.Icc (a i) (b i))

A box cut out by finitely many lower and upper coordinate bounds is a convex polyhedron, including boxes with empty intervals or no coordinates.

theorem TauCeti.isConvexPolyhedron_closedBall_pi {ι : Type u_1} [Fintype ι] (x : ι → ℝ) {r : ℝ} (hr : 0 ≤ r) : IsConvexPolyhedron (Metric.closedBall x r)

Nonnegative-radius closed balls in a finite real coordinate space are convex polyhedra for the supremum metric.