Positive extension from a unital subspace of C(K) (source code)

= Positive extension from a unital subspace of C(K)

A real <positive linear functional> on a <vector subspace> of $C(K)$ containing $1$ extends positively to all of $C(K)$. Its norm is $\phi(1)$ by order bounds. If this is positive, apply the <Hahn-Banach theorem> to obtain an extension of the same norm, normalize it to value one at $1$, and use the <unital contraction positivity criterion>. If $\phi(1)=0$, the functional is zero and its zero extension suffices.