Separation of a Point and a Subspace

Separation theorem. Let $X$ be a normed space over $\mathbb K\in\{\mathbb R,\mathbb C\}$ , let $Y\subseteq X$ be a linear subspace, and suppose $x_0\in X$ has positive distance

d(x_0,Y):=\inf_{y\in Y}\|x_0-y\|=d>0.

Then there exists a bounded linear functional $f:X\to\mathbb K$ such that

f|_Y=0,\qquad f(x_0)=1,\qquad \lVert f\rVert=\frac1d.

Proof idea

On $Y\oplus\operatorname{span}\{x_0\}$ , define $f_0(y+\lambda x_0)=\lambda$ . The distance assumption gives $\lVert f_0\rVert=1/d$ , and Hahn–Banach extends $f_0$ to $X$ without increasing its norm.