Geometric Hahn-Banach theorem for radially open sets (source code)

= Geometric Hahn-Banach theorem for radially open sets
{title2=$U\cap C=\varnothing\Longrightarrow U\subseteq\ker L,\quad L(C)<0$}

For a nonempty <radially open convex set> $C$ disjoint from a <vector subspace> $U$, there is a nonzero <linear functional> $L$ whose <kernel of a linear map> contains $U$ and avoids $C$. Choose $a\in C$ and the <Minkowski functional> $p$ of $C-a$. On $U+\mathbb Ra$, set $g(u+ta)=-t$. Disjointness implies $p(u-a)\geq1$, which gives $g\leq p$ for negative $t$; nonnegativity of $p$ gives it for nonnegative $t$. The algebraic <Hahn-Banach theorem> extends $g$ to $L\leq p$. For $x\in C$, $L(x)+1=L(x-a)<1$, so $L(x)<0$. Also $L(a)=-1$ and $L|_U=0$.