Proof. [03B6]
Original official author HTML, exact retained edition. Historical TeX conversion verdicts remain unchanged. Cited-edition alignment and mathematical self-containment are not assessed.
Complete original source context · Original author HTML
Proof.
Since piecewise -linear functions are dense in the compact case [Gub98, Theorem 7.12], there exists a piecewise -linear function such that on . Since is compact, there is a non-zero such that is piecewise linear. By Proposition 2.6 and Proposition 2.8 applied to the formal metric on associated to , there exists a piecewise -linear function which extends . We then set . By Proposition 2.10 (d), is piecewise -linear. By definition, we have . We have on and is non-negative, hence we have on . Finally, since on we also have that on . ∎