Polyhedral neighbourhoods in real coordinate products

In an arbitrary product of real lines, boxes constraining finitely many coordinates are convex polyhedra and form a neighbourhood basis. Unlike boxes constraining every coordinate, these cylinders remain neighbourhoods when the coordinate type is infinite.

These neighbourhoods allow local affine decompositions to be restricted to polyhedral cells before taking a finite subcover of a compact set.

theorem TauCeti.isConvexPolyhedron_pi_Icc_of_finite {ι : Type u_1} {I : Set ι} (hI : I.Finite) (a b : ι → ℝ) : IsConvexPolyhedron (I.pi fun (i : ι) => Set.Icc (a i) (b i))

A cylinder imposing interval bounds on finitely many coordinates is a convex polyhedron in the product topology, with no finiteness assumption on the ambient coordinate type.

theorem TauCeti.exists_isConvexPolyhedron_mem_nhds_pi {ι : Type u_1} {x : ι → ℝ} {U : Set (ι → ℝ)} (hU : U ∈ nhds x) : ∃ C ∈ nhds x, IsConvexPolyhedron C ∧ C ⊆ U

Every neighbourhood in a real coordinate product contains a convex polyhedral neighbourhood. The product may have infinitely many coordinates.