Choice-free Hahn-Banach extension in a separable space (source code)

= Choice-free Hahn-Banach extension in a separable space
{title2=$\widetilde T|_U=T,\quad\|\widetilde T\|=\|T\|$}

In a real <normed vector space> with a specified countable <dense subset>, a <bounded linear functional> on any <vector subspace> admits a norm-preserving extension without the <axiom of choice>. Add the dense vectors one at a time using the supremum endpoint in the <one-dimensional dominated extension of a real linear functional>. This makes the recursion deterministic. Extend from the resulting dense subspace by continuity, using the least index in the dense list which approximates a given vector to within $2^{-n}$.