[proofplan] The previous theorem ([Neighbourhood Separation by Finitely Many Hyperplanes](/theorems/2663)) gives finitely many separating functionals $f_1, \ldots, f_n$. We must collapse this to a single functional, exploiting that $x_0$ is an extreme point. Define $K_i := \{x \in K : f_i(x) \geq \alpha_i\}$. The extremality of $x_0$ inside $K$ shows $x_0 \notin \operatorname{conv}(\bigcup_i K_i)$. The set $\operatorname{conv}(\bigcup_i K_i)$ is compact (image of a compact simplex-by-product under the convex-combination map), so a second Hahn-Banach separation produces a single functional $f$ strictly separating $x_0$ from $\operatorname{conv}(\bigcup_i K_i)$. [/proofplan]

[step:Apply the previous theorem to obtain finitely many separating functionals] By [Neighbourhood Separation by Finitely Many Hyperplanes](/theorems/2663), applied to the locally convex space $X$, the compact set $K$, the point $x_0 \in K$, and the neighbourhood $V$ of $x_0$, there exist $n \in \mathbb{N}$, functionals $f_1, \ldots, f_n \in X^*$, and reals $\alpha_1, \ldots, \alpha_n \in \mathbb{R}$ such that \begin{align*} x_0 \in \{x \in X : f_i(x) < \alpha_i \text{ for all } 1 \leq i \leq n\} \cap K \subset V. \tag{$\dagger$} \end{align*} In particular, $f_i(x_0) < \alpha_i$ for each $i \in \{1, \ldots, n\}$. [/step]

[step:Define the closed sets $K_i$ and verify they are compact and convex] For $i = 1, \ldots, n$, set \begin{align*} K_i := \{x \in K : f_i(x) \geq \alpha_i\} = K \cap f_i^{-1}([\alpha_i, \infty)). \end{align*} *$K_i$ is closed in $K$:* the preimage $f_i^{-1}([\alpha_i, \infty))$ is closed in $X$ (preimage of a closed set under the continuous $f_i$), and $K$ is closed (compact subsets of a Hausdorff space are closed). The intersection of closed sets is closed. *$K_i$ is compact:* it is a closed subset of the compact set $K$. *$K_i$ is convex:* let $x, y \in K_i$ and $t \in [0, 1]$. Then $tx + (1-t)y \in K$ (since $K$ is convex), and \begin{align*} f_i(tx + (1-t)y) = t f_i(x) + (1-t) f_i(y) \geq t \alpha_i + (1-t) \alpha_i = \alpha_i, \end{align*} so $tx + (1-t)y \in K_i$. *$x_0 \notin K_i$:* by Step 1, $f_i(x_0) < \alpha_i$, so $x_0$ fails the defining inequality $f_i(x) \geq \alpha_i$. [/step]

[step:Show $x_0 \notin \operatorname{conv}(\bigcup_{i=1}^n K_i)$ using extremality]Set $L := \bigcup_{i=1}^n K_i \subseteq K$. We show $x_0 \notin \operatorname{conv}(L)$. Suppose for contradiction that $x_0 \in \operatorname{conv}(L)$, i.e.\ there exist $m \in \mathbb{N}$, points $y_1, \ldots, y_m \in L$, and weights $s_1, \ldots, s_m \geq 0$ with $\sum_{j=1}^m s_j = 1$ such that \begin{align*} x_0 = \sum_{j=1}^m s_j y_j. \end{align*} After dropping summands with $s_j = 0$ (which contribute nothing to the sum), we may assume each $s_j > 0$. By induction on $m$, applied to extremality of $x_0$: *$m = 1$:* $x_0 = y_1$, so $y_1 = x_0$. *$m \geq 2$:* set $t := s_1 \in (0, 1]$. If $t = 1$, the assumption $s_j > 0$ for all $j$ forces $m = 1$. Otherwise $t \in (0, 1)$, and $z := \frac{1}{1 - t}\sum_{j=2}^m s_j y_j$ is a convex combination in $K$ (so $z \in K$). The decomposition $x_0 = t y_1 + (1 - t) z$ with $y_1, z \in K$ and $t \in (0, 1)$ forces $y_1 = z = x_0$ by extremality. Apply the inductive hypothesis to $z = x_0 = \sum_{j=2}^m \frac{s_j}{1-t} y_j$ (an $(m-1)$-term convex combination) to conclude $y_j = x_0$ for all $j \geq 2$. Hence $y_j = x_0$ for each $j$ with $s_j > 0$. But $y_j \in L \subseteq \bigcup_i K_i$ means $y_j \in K_{i(j)}$ for some $i(j)$, while Step 2 gives $x_0 \notin K_i$ for any $i$. So $y_j \neq x_0$, a contradiction. Therefore $x_0 \notin \operatorname{conv}(L)$.[/step]

[guided]We now use the extremality of $x_0$ in $K$. Recall: $x_0 \in \operatorname{Ext}(K)$ means that whenever $x_0 = ty + (1-t)z$ with $y, z \in K$ and $t \in (0, 1)$, we must have $y = z = x_0$. By induction on $m$, this implies that any *finite* convex combination $x_0 = \sum_{j=1}^m s_j y_j$ with $y_j \in K$ and $s_j > 0$, $\sum s_j = 1$, forces $y_j = x_0$ for each $j$ with $s_j > 0$. *Base case $m = 1$:* $x_0 = s_1 y_1$ with $s_1 = 1$, so $x_0 = y_1$. *Inductive step:* assume the claim for $m - 1$ summands. Suppose $x_0 = \sum_{j=1}^m s_j y_j$ with $s_j > 0$, $\sum s_j = 1$, $y_j \in K$. Set $t := s_1 \in (0, 1]$. If $t = 1$, then $m = 1$ (all other $s_j = 0$ would contradict $s_j > 0$, so we are reduced to base case). If $t \in (0, 1)$, set $z := \frac{1}{1 - t} \sum_{j=2}^m s_j y_j$. Then $\sum_{j=2}^m \frac{s_j}{1-t} = 1$ and each $\frac{s_j}{1-t} \geq 0$, so $z$ is a convex combination of points $y_2, \ldots, y_m \in K$, hence $z \in K$ by convexity of $K$. We have $x_0 = t y_1 + (1-t) z$ with $y_1, z \in K$ and $t \in (0, 1)$. Extremality forces $y_1 = z = x_0$. Now $z = x_0$ is itself a convex combination of $y_2, \ldots, y_m$ in $K$ with $m - 1$ summands, so by the inductive hypothesis $y_j = x_0$ for each $j \geq 2$ with $\frac{s_j}{1-t} > 0$. Hence $y_j = x_0$ for every $j$ with $s_j > 0$. *Removing zero-weight summands.* Drop indices $j$ with $s_j = 0$ from the sum (they do not contribute). After this reduction, all $s_j > 0$. By the above, each remaining $y_j$ equals $x_0$. But each $y_j \in L = \bigcup_i K_i$, so each $y_j$ lies in some $K_{i(j)}$. By Step 2, $x_0 \notin K_{i(j)}$. Hence $y_j \neq x_0$. Contradiction.[/guided]

[step:Show $\operatorname{conv}(L)$ is compact] Let $\Delta_n := \{(t_1, \ldots, t_n) \in \mathbb{R}^n : t_i \geq 0, \sum_{i=1}^n t_i = 1\}$ be the standard $(n-1)$-simplex; it is compact in $\mathbb{R}^n$ (closed and bounded). Define the convex-combination map \begin{align*} \Phi : \Delta_n \times K_1 \times \cdots \times K_n &\to X \\ ((t_i)_{i=1}^n, x_1, \ldots, x_n) &\mapsto \sum_{i=1}^n t_i x_i. \end{align*} $\Phi$ is continuous: it is built from the addition $X \times X \to X$ and scalar multiplication $\mathbb{R} \times X \to X$, both continuous in the locally convex space $X$. The domain $\Delta_n \times K_1 \times \cdots \times K_n$ is compact: it is a finite product of compact spaces (Step 2 gives $K_i$ compact; $\Delta_n$ is compact in $\mathbb{R}^n$). The continuous image of a compact set is compact, so $\Phi(\Delta_n \times K_1 \times \cdots \times K_n)$ is compact in $X$. [claim:$\Phi(\Delta_n \times K_1 \times \cdots \times K_n) = \operatorname{conv}(L)$] The image of $\Phi$ equals $\operatorname{conv}(L) = \operatorname{conv}(\bigcup_{i=1}^n K_i)$. [/claim] [proof] *$\subseteq$:* Every point in $\Phi(\Delta_n \times K_1 \times \cdots \times K_n)$ has the form $\sum_{i=1}^n t_i x_i$ with $x_i \in K_i \subseteq L$, $t_i \geq 0$, $\sum t_i = 1$. This is a convex combination of points of $L$, so it lies in $\operatorname{conv}(L)$. *$\supseteq$:* Let $y \in \operatorname{conv}(L)$. Then $y = \sum_{j=1}^m s_j y_j$ with $y_j \in L$, $s_j \geq 0$, $\sum s_j = 1$. Each $y_j$ lies in some $K_{i(j)}$. Group summands by index $i \in \{1, \ldots, n\}$: for each $i$, let $S_i := \{j : i(j) = i\}$ and $t_i := \sum_{j \in S_i} s_j$. If $t_i > 0$, set $x_i := \frac{1}{t_i} \sum_{j \in S_i} s_j y_j \in K_i$ (convex combination of points in the convex set $K_i$). If $t_i = 0$, choose any $x_i \in K_i$ (which exists since $K_i \neq \varnothing$ by hypothesis — note that if some $K_i$ is empty, drop it from the union $L$, reducing $n$). Then $\sum_{i=1}^n t_i = \sum_{j=1}^m s_j = 1$, $t_i \geq 0$, $x_i \in K_i$, and \begin{align*} \sum_{i=1}^n t_i x_i = \sum_{i : t_i > 0} \sum_{j \in S_i} s_j y_j = \sum_{j=1}^m s_j y_j = y. \end{align*} So $y \in \Phi(\Delta_n \times K_1 \times \cdots \times K_n)$. (If some $K_i$ is empty, the corresponding constraint $f_i(x) \geq \alpha_i$ is infeasible on $K$, meaning $f_i(x) < \alpha_i$ for all $x \in K$; then dropping the index $i$ from our list does not change the conclusion of $(\dagger)$ — the slice on the remaining indices is contained in the original slice. We may therefore assume each $K_i$ is non-empty.) [/proof] Therefore $\operatorname{conv}(L)$ is compact in $X$. [/step]

[step:Apply Hahn-Banach to separate $x_0$ from $\operatorname{conv}(L)$] The set $\operatorname{conv}(L)$ is compact (Step 4) and convex (the convex hull of any set is convex). The singleton $\{x_0\}$ is compact and convex. By Step 3, $x_0 \notin \operatorname{conv}(L)$, so the two sets are disjoint. By [Hahn-Banach for Locally Convex Spaces](/theorems/2638) (geometric form, separating two disjoint compact convex sets — a fortiori a singleton from a compact convex set), there exist a continuous $\mathbb{R}$-linear functional $f : X \to \mathbb{R}$ and a real $\alpha \in \mathbb{R}$ with \begin{align*} f(x_0) < \alpha < \inf_{y \in \operatorname{conv}(L)} f(y). \tag{$\ddagger$} \end{align*} (In the complex case, $f$ is the real part of a continuous complex-linear functional, identified canonically with an element of the real-dual; the conclusion below uses only the real-linear structure.) Note that $\operatorname{conv}(L) \neq \varnothing$ requires $L \neq \varnothing$, which holds when $V \neq X$ (otherwise the conclusion is trivial — we could take $f \equiv 0$ and $\alpha = 1$, giving $\{f < \alpha\} = X$ and $\{f < \alpha\} \cap K = K \subseteq V = X$). If $L = \varnothing$ — equivalently, all $K_i$ are empty — then by the parenthetical in Step 4 we have $f_i(x) < \alpha_i$ on $K$ for every $i$, so $K \subseteq \{f_i < \alpha_i \text{ for all } i\} \cap K \subseteq V$ by $(\dagger)$. Then $f := f_1 \in X^*$ and $\alpha := \alpha_1$ satisfy $f(x_0) < \alpha$ and $\{f < \alpha\} \cap K \subseteq K \subseteq V$, giving the conclusion. Henceforth assume $L \neq \varnothing$ and $(\ddagger)$ holds. [/step]

[step:Verify the slice satisfies the required containments] We claim that $f$ and $\alpha$ from Step 5 satisfy \begin{align*} x_0 \in \{x \in X : f(x) < \alpha\} \cap K \subseteq V. \end{align*} *First containment:* by $(\ddagger)$, $f(x_0) < \alpha$, and $x_0 \in K$, so $x_0 \in \{f < \alpha\} \cap K$. *Second containment:* let $y \in K$ with $f(y) < \alpha$. We must show $y \in V$. Suppose for contradiction $y \notin V$. Then by $(\dagger)$, $y$ fails some $f_i(y) < \alpha_i$, i.e.\ $f_i(y) \geq \alpha_i$ for some $i$. But this means $y \in K_i \subseteq L \subseteq \operatorname{conv}(L)$. By $(\ddagger)$, $f(y) \geq \inf_{\operatorname{conv}(L)} f > \alpha$, contradicting $f(y) < \alpha$. Hence $y \in V$. This proves \begin{align*} x_0 \in \{x \in X : f(x) < \alpha\} \cap K \subset V, \end{align*} as required. [/step]