Finite convex function as supremum of affine minorants (source code)

= Finite convex function as supremum of affine minorants
{title2=$\phi(x)=\sup_y[\phi(y)+\ell_y(x-y)]$}

For a finite real <convex function> on an entire real <vector space>, apply the <convex domination form of the Hahn-Banach theorem> to $\phi(y+z)-\phi(y)$ and the zero functional on $\{0\}$. It supplies a <linear functional> $\ell_y$ dominated by this translated function. The <affine function> $a_y(x)=\phi(y)+\ell_y(x-y)$ lies below $\phi$ everywhere and equals it at $y$. Taking the supremum proves the formula. These are algebraic affine minorants; continuity requires additional topological hypotheses.