Finite-dimensional separation of open convex sets (source code)

= Finite-dimensional separation of open convex sets

Let $K_1,\ldots,K_n$ be open <convex sets> in a real <locally convex space> $X$, with empty intersection. There is a continuous <linear map> $T:X\to\mathbb R^{n-1}$ for which $\bigcap_iT(K_i)=\varnothing$. If any $K_i$ is empty the conclusion is immediate, so assume all are nonempty and $n\ge2$.

In $X^n$, the open <convex set> $K_1\times\cdots\times K_n$ is disjoint from the diagonal <linear subspace> $D=\{(x,\ldots,x):x\in X\}$. <Hahn-Banach separation theorem for two convex sets> gives a continuous linear functional $F=\sum_i f_i(x_i)$ that vanishes on $D$ and is strictly positive on the product. Thus $\sum_i f_i=0$.

Take $T(x)=(f_1(x),\ldots,f_{n-1}(x))$. If a point belonged to every $T(K_i)$, choose $k_i\in K_i$ with the same $T$-value. Then
$$
\sum_{i=1}^nf_i(k_i)=\sum_{i=1}^{n-1}f_i(k_i)-\sum_{i=1}^{n-1}f_i(k_n)=0,
$$
contradicting positivity of $F$ on the product. The linear dependence among the separating functionals explains the dimension $n-1$.