Finite PL decompositions on compact sets

A PL map on a compact subset of a real coordinate product admits a finite piecewise-affine decomposition. Compactness thus lets one use finitely many affine pieces to describe a map given by local PL data. The same holds on a compact subset of a finite-dimensional real normed space, read in linear coordinates.

In particular, coning a PL map with compact base can use a finite decomposition at the apex, even though IsPLOn is defined using local decompositions.

Reference: Rourke--Sanderson, Introduction to Piecewise-Linear Topology, Springer (1972), Example 1.5(4), p. 5, and Corollary 2.3, p. 12.

theorem TauCeti.IsPLOn.isPiecewiseAffineOn_of_isCompact {ι : Type u_1} {F : Type u_2} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] {s : Set (ι → ℝ)} {f : (ι → ℝ) → F} (hf : IsPLOn f s) (hs : IsCompact s) : IsPiecewiseAffineOn f s

A PL map on a compact subset of a real coordinate product admits a finite piecewise-affine decomposition on that set.

theorem TauCeti.IsPLOn.isPiecewiseAffineOn_of_isCompact_of_finiteDimensional {F : Type u_2} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {f : E → F} {s : Set E} (hf : IsPLOn f s) (hs : IsCompact s) : IsPiecewiseAffineOn f s

A PL map on a compact subset of a finite-dimensional real normed space admits a finite piecewise-affine decomposition on that set.