Separation of a point and an open convex set (source code)

= Separation of a point and an open convex set

If $C$ is a nonempty open convex subset of a real locally convex space and $x_0\notin C$, a continuous linear functional strictly separates them: after choosing a sign, $f(c)<f(x_0)$ for every $c\in C$. Apply the <Hahn-Banach theorem> to the <Minkowski functional> of a translate of $C$.