Proof of Strong Separation of a Closed Convex Set and a Disjoint Compact Convex Set in $\mathbb{R}^n$

Throughout, closedness and compactness in $\mathbb{R}^{n}$ refer to the metric topology $\mathcal{T}_{d_{E}}$, which exists by The Open Sets of a Metric Space Form a Set, Given by a Predicative Formula (ii).

We first show that $C$ and $K$ are a positive distance apart. For $k\in K$ let $f(k)=\operatorname{dist}(k,C)$ be the distance in $(\mathbb{R}^{n},d_{E})$ from $k$ to the nonempty set $C$. Since $C$ is closed and $k\notin C$, as $C\cap K=\emptyset$, we have $f(k)>0$ by The Distance to a Subset of a Metric Space: Bounds, the Lipschitz Estimate, Continuity, and Vanishing Exactly on the Closure (v). The function $f:K\to\mathbb{R}$ is continuous on $K$ by The Distance to a Subset of a Metric Space: Bounds, the Lipschitz Estimate, Continuity, and Vanishing Exactly on the Closure (iii), and $K$ is nonempty and compact, so Extreme Value Theorem on a Compact Subset of a Metric Space (i) gives $k_{0}\in K$ with $f(k_{0})\le f(k)$ for every $k\in K$. Put $\delta=f(k_{0})>0$. For $c\in C$ and $k\in K$, The Distance to a Subset of a Metric Space: Bounds, the Lipschitz Estimate, Continuity, and Vanishing Exactly on the Closure (i) gives

$$\lVert c-k\rVert=d_{E}(k,c)\ge f(k)\ge\delta.$$

Next let $M=C-K=\{c-k:c\in C,\ k\in K\}$, which is convex by Operations Preserving Convexity in $\mathbb{R}^n$: Intersections, Translates, Scalar Multiples, Sums, Affine Images and Preimages, Closure and Interior (v). Its closure $\operatorname{cl}M$ is convex by Operations Preserving Convexity in $\mathbb{R}^n$: Intersections, Translates, Scalar Multiples, Sums, Affine Images and Preimages, Closure and Interior (viii) and closed by Closure and Interior in a Metric Space: Containments, the Closure is Closed, the Interior is Open (ii). For $c\in C$ and $k\in K$ we have $d_{E}(0,c-k)=\lVert c-k\rVert\ge\delta$ by the estimate above, so $B(0,\delta)\cap M=\emptyset$, and the origin is not in $\operatorname{cl}M$ (Closure of a Subset of a Metric Space (ii)).

By Strong Separation of a Point from a Closed Convex Subset of $\mathbb{R}^n$ (i), applied to $\operatorname{cl}M$ and the origin, there is $b\in\mathbb{R}^{n}$ with $b\neq0$ and

$$b\cdot w\le b\cdot0-\lVert b\rVert^{2}=-\lVert b\rVert^{2}\qquad\text{for every }w\in\operatorname{cl}M,$$

in particular for every $w\in M$, as $M\subseteq\operatorname{cl}M$ (Closure and Interior in a Metric Space: Containments, the Closure is Closed, the Interior is Open (i)). Taking $w=c-k$ and using bilinearity,

$$b\cdot c\le b\cdot k-\lVert b\rVert^{2}\qquad\text{for all }c\in C\text{ and }k\in K.$$

It remains to choose the level. The set $\{b\cdot c:c\in C\}$ is nonempty and bounded above by $b\cdot k_{0}-\lVert b\rVert^{2}$, so it has a supremum $\sigma$ (The Real Numbers, with the Natural Numbers, Integers and Rationals Identified with Subsets of the Reals, and Completeness (vii)). By the last display each number $b\cdot k-\lVert b\rVert^{2}$ with $k\in K$ is an upper bound of this set, so $\sigma\le b\cdot k-\lVert b\rVert^{2}$, the supremum being the least upper bound (Bounds, Least and Greatest Elements, Suprema and Infima for a Partial Order (iv)). Let $a=b$, let $\varepsilon=\tfrac{1}{2}\lVert b\rVert^{2}$, which is positive as $b\neq0$, and let $\alpha=\sigma+\varepsilon$. Then

$$a\cdot c\le\sigma=\alpha-\varepsilon\quad(c\in C)\qquad\text{and}\qquad a\cdot k\ge\sigma+\lVert b\rVert^{2}=\alpha+\varepsilon\quad(k\in K),$$

which is (i); so $H(a,\alpha)$ strongly separates $C$ and $K$ by Separating Hyperplanes in $\mathbb{R}^n$: Separation, Strict Separation and Strong Separation (iii).