Convex domination form of the Hahn-Banach theorem (source code)

= Convex domination form of the Hahn-Banach theorem
{title2=$g|_W=f,\quad g\le\phi$}

A <linear functional> $f$ dominated by a finite real <convex function> $\phi$ on a <vector subspace> $W$ extends with the same domination to the whole real <vector space>. To add $v\notin W$, choose $g(v)$ between the supremum of $(f(w)-\phi(w-tv))/t$ and the infimum of $(\phi(w+sv)-f(w))/s$, over $w\in W$ and $s,t>0$. Convexity, applied to $(s(w_1-tv)+t(w_2+sv))/(s+t)$, makes every lower candidate at most every upper candidate. The candidates at $w=0,s=t=1$ bound the interval by finite numbers. Chain unions preserve domination, so <Zorn's lemma> gives a full extension. No homogeneity of $\phi$ is assumed.