Uniform strict separation of compact and closed convex sets

Consider all pairs $(k,N)$ with $k\in K$ and $N$ an open convex zero-neighborhood such that $k+N\subseteq X\setminus C$. There is such a pair above every $k$: since $C$ is closed, $(X\setminus C)-k$ is an open zero-neighborhood, and it admits an open convex refinement. Each $G_{k,N}=K\cap (k+\frac{1}{2}N)$ is open in $K$ and contains $k$. The family of all such sets covers $K$; it is defined by a property, without choosing a neighborhood for every $k$.

Compactness gives finitely many cover members $G_1,\dots ,G_m$ with $m\ge 1$. For each $j$ its set of representing pairs $(k,N)$ is nonempty. Finite choice gives representatives $(k_j,N_j)$ for this finite list. Put $W={\bigcap }_{j=1}^m\frac{1}{2}{N}_j$. It is an open convex zero-neighborhood.

For $k\in K$, some $j$ has $k=k_j+n\mathrm{/}2$ with $n\in N_j$. If $w\in W$, write $w=n^{\mathrm{\prime }}\mathrm{/}2$ with $n^{\mathrm{\prime }}\in N_j$. Convexity gives $n\mathrm{/}2+n^{\mathrm{\prime }}\mathrm{/}2\in N_j$, so $k+w\in k_j+N_j\subseteq X\setminus C$. Therefore $(K+W)\cap C=\mathrm{\varnothing }$. The set $K+W$ is nonempty and open as a union of translates of $W$, and convex because the convex combinations of its $K$ and $W$ components stay in those respective sets.

Apply open separation to $K+W$ and $C$, using HB once. Obtain a nonzero continuous scalar-linear $f$ and $\beta \in \mathbb{R}$ such that $u(k+w)<\beta \le u(c)$, where $u=\mathrm{Re}f$. The restriction $u{\mathrm{\mid }}_K$ is continuous, since real part is continuous and restrictions are continuous. It attains a maximum $d=u(k_{\ast })$ for some $k_{\ast }\in K$. Since $0\in W$, the strict inequality at $k_{\ast }+0$ gives $d<\beta$. This attainment step turns pointwise strict separation into a uniform gap.

Put $\alpha =(d+\beta )\mathrm{/}2$ and $\epsilon =(\beta -d)\mathrm{/}2>0$. Then $\alpha -\epsilon =d$ and $\alpha +\epsilon =\beta$, so $u(k)\le d=\alpha -\epsilon <\alpha +\epsilon =\beta \le u(c)$ for all $k,c$. A singleton $K$ is allowed and simply has its sole value as the maximum. Nonemptiness of $K$ is used for attainment and of $C$ in open separation; no other separation axiom or choice principle is used.