[proofplan] The Minkowski functional $\mu_C$ of the open convex set $C \ni 0$ is positively homogeneous and subadditive, with $C = \{x : \mu_C(x) < 1\}$. Since $x_0 \notin C$, we have $\mu_C(x_0) \geq 1$. Define a linear functional $g$ on the one-dimensional subspace $\operatorname{span}\{x_0\}$ by $g(\lambda x_0) = \lambda \mu_C(x_0)$, dominated by $\mu_C$ on this line. By [Hahn-Banach (Real Version)](/theorems/2627) extend $g$ to a linear $f : X \to \mathbb{R}$ with $f \leq \mu_C$ pointwise. The two-sided bound $|f(x)| \leq \max(\mu_C(x), \mu_C(-x))$ together with continuity of $\mu_C$ at $0$ yields continuity of $f$, hence $f \in X^*$. Finally, for $x \in C$ we use $\mu_C(x) < 1 \leq \mu_C(x_0) = f(x_0)$ together with $f \leq \mu_C$. The complex case reduces to the real case by passing to the underlying real-linear structure and recovering complex linearity from the real part. [/proofplan] [step:Set up the Minkowski functional and verify the key inequality $\mu_C(x_0) \geq 1$] Since $C$ is convex, open, and $0 \in C$, the Minkowski functional \begin{align*} \mu_C : X &\to [0, \infty), \\ x &\mapsto \inf\{t > 0 : x \in tC\} \end{align*} is well defined, finite-valued (since $0$ is an interior point of $C$, $C$ absorbs every $x \in X$), positively homogeneous, and subadditive by **Properties of the Minkowski Functional**. Moreover, since $C$ is open, the same theorem gives \begin{align*} C = \{x \in X : \mu_C(x) < 1\}. \end{align*} Because $x_0 \notin C$, we conclude $\mu_C(x_0) \geq 1$. [/step] [step:Define a dominated linear functional on $\operatorname{span}\{x_0\}$] Let $Y = \operatorname{span}\{x_0\} = \{\lambda x_0 : \lambda \in \mathbb{R}\}$, a one-dimensional linear subspace of $X$. Define \begin{align*} g : Y &\to \mathbb{R}, \\ \lambda x_0 &\mapsto \lambda \mu_C(x_0). \end{align*} The map is well defined and linear (any $y \in Y$ is uniquely $\lambda x_0$ since $x_0 \neq 0$ — note $x_0 \neq 0$ because $0 \in C$ and $x_0 \notin C$). We verify $g(y) \leq \mu_C(y)$ for all $y \in Y$. Fix $\lambda \in \mathbb{R}$. - If $\lambda \geq 0$: by positive homogeneity, $\mu_C(\lambda x_0) = \lambda \mu_C(x_0) = g(\lambda x_0)$, so equality holds. - If $\lambda < 0$: $g(\lambda x_0) = \lambda \mu_C(x_0) \leq 0 \leq \mu_C(\lambda x_0)$, since $\mu_C \geq 0$ and $\lambda \mu_C(x_0) \leq 0$. Hence $g \leq \mu_C$ on $Y$. [guided] The goal is to construct a separating functional. The Hahn-Banach extension theorem requires three ingredients: (a) a sublinear functional $p$ on $X$ (positively homogeneous and subadditive), (b) a linear subspace $Y \subseteq X$, (c) a linear functional $g$ on $Y$ with $g \leq p$ on $Y$. Then $g$ extends to a linear $f$ on $X$ with $f \leq p$ on $X$. Our $p$ is the Minkowski functional $\mu_C$, which is sublinear by **Properties of the Minkowski Functional**. The natural choice of $Y$ is the one-dimensional subspace through $x_0$ — we want to control $f$ at $x_0$ specifically (we want $f(x_0) \geq 1$ to separate from $C$). The natural choice of $g$ is the linear functional on $Y$ that equals $\mu_C(x_0)$ at $x_0$, i.e.\ $g(\lambda x_0) := \lambda \mu_C(x_0)$. Why is $g$ well-defined? We need $x_0 \neq 0$ so the representation $y = \lambda x_0$ is unique. Indeed $x_0 \neq 0$: if $x_0 = 0$, then $x_0 \in C$ (since $0 \in C$), contradicting $x_0 \notin C$. Now the domination check $g \leq \mu_C$ on $Y$. Two cases by the sign of $\lambda$: - For $\lambda \geq 0$: positive homogeneity of $\mu_C$ gives $\mu_C(\lambda x_0) = \lambda \mu_C(x_0)$, which matches $g(\lambda x_0)$ exactly. So $g(\lambda x_0) = \mu_C(\lambda x_0)$, in particular $\leq$. - For $\lambda < 0$: $g(\lambda x_0) = \lambda \mu_C(x_0)$ is non-positive (negative times non-negative), while $\mu_C(\lambda x_0) \geq 0$. So $g \leq 0 \leq \mu_C$. Note we cannot use positive homogeneity for $\lambda < 0$ — that would require the absolute homogeneity property of a seminorm, which $\mu_C$ generally lacks. [/guided] [/step] [step:Extend to $f : X \to \mathbb{R}$ via Hahn-Banach] The functional $\mu_C : X \to \mathbb{R}$ is positively homogeneous and subadditive (Step 1), and $g : Y \to \mathbb{R}$ is linear with $g \leq \mu_C$ on $Y$ (Step 2). By [Hahn-Banach (Real Version)](/theorems/2627), $g$ extends to a linear functional \begin{align*} f : X \to \mathbb{R} \end{align*} satisfying $f|_Y = g$ and $f(x) \leq \mu_C(x)$ for all $x \in X$. In particular, $f(x_0) = g(x_0) = \mu_C(x_0) \geq 1$. [/step] [step:Establish continuity of $f$ from the bound $|f(x)| \leq \max(\mu_C(x), \mu_C(-x))$] For any $x \in X$: \begin{align*} f(x) &\leq \mu_C(x), \\ -f(x) = f(-x) &\leq \mu_C(-x), \end{align*} so $|f(x)| \leq \max(\mu_C(x), \mu_C(-x))$. We show that $\mu_C$ is small near $0$ in the sense of the topology on $X$. Fix $\varepsilon > 0$. The set $\varepsilon C$ is open (as the dilation of the open set $C$ by the homeomorphism $x \mapsto \varepsilon x$), contains $0$, and equals $\{x : \mu_C(x) < \varepsilon\}$ by **Properties of the Minkowski Functional** applied to $\varepsilon C$ — equivalently, by positive homogeneity, $\mu_C(x) < \varepsilon \iff \mu_C(x/\varepsilon) < 1 \iff x/\varepsilon \in C \iff x \in \varepsilon C$. Similarly $-\varepsilon C = \{x : \mu_C(-x) < \varepsilon\}$ is an open neighbourhood of $0$. Set \begin{align*} U_\varepsilon = (\varepsilon C) \cap (-\varepsilon C), \end{align*} an open neighbourhood of $0$ (intersection of two open neighbourhoods of $0$). For $x \in U_\varepsilon$, $\mu_C(x) < \varepsilon$ and $\mu_C(-x) < \varepsilon$, so \begin{align*} |f(x)| \leq \max(\mu_C(x), \mu_C(-x)) < \varepsilon. \end{align*} This shows $f$ is continuous at $0$. Since $f$ is linear, continuity at $0$ implies continuity everywhere, so $f \in X^*$. [guided] We have a linear functional $f$ with $f \leq \mu_C$. To conclude $f \in X^*$ we need continuity. In a TVS, a linear functional is continuous iff it is continuous at $0$ — translation invariance and linearity propagate continuity from one point to all points. So we must show: for every $\varepsilon > 0$ there is an open neighbourhood $U$ of $0$ with $|f(x)| < \varepsilon$ for $x \in U$. The bound $f \leq \mu_C$ controls $f$ from above. The trick is to also control $-f$ from above by applying the bound to $-x$: \begin{align*} -f(x) = f(-x) \leq \mu_C(-x). \end{align*} Combining, $|f(x)| \leq \max(\mu_C(x), \mu_C(-x))$. Now we need to show that both $\mu_C(x)$ and $\mu_C(-x)$ are small near $0$. The neighbourhood $\{\mu_C(x) < \varepsilon\}$ equals $\varepsilon C$ by the equality $\{\mu_C < 1\} = C$ for open $C$ (proved in **Properties of the Minkowski Functional**) combined with positive homogeneity: \begin{align*} \mu_C(x) < \varepsilon \iff \mu_C(x/\varepsilon) < 1 \iff x/\varepsilon \in C \iff x \in \varepsilon C. \end{align*} The set $\varepsilon C$ is open: $\varepsilon C$ is the image of the open set $C$ under the homeomorphism $x \mapsto \varepsilon x$ (a homeomorphism of $X$ to itself by the TVS axioms). Similarly $-\varepsilon C = \{x : \mu_C(-x) < \varepsilon\}$ is an open neighbourhood of $0$ ($0 \in C$ implies $0 = -0 \in -\varepsilon C$). The intersection $U_\varepsilon = (\varepsilon C) \cap (-\varepsilon C)$ is an open neighbourhood of $0$ (finite intersections of open neighbourhoods are open neighbourhoods). For $x \in U_\varepsilon$, $\mu_C(x) < \varepsilon$ and $\mu_C(-x) < \varepsilon$, so $|f(x)| < \varepsilon$. This is exactly the $\varepsilon$-$U$ statement of continuity at $0$, and linearity then gives continuity everywhere. [/guided] [/step] [step:Combine to obtain strict separation $f(x) < f(x_0)$ on $C$] Let $x \in C$. Since $C$ is open, $\mu_C(x) < 1$ by **Properties of the Minkowski Functional**. Hence \begin{align*} f(x) \leq \mu_C(x) < 1 \leq \mu_C(x_0) = f(x_0). \end{align*} This is the strict inequality $f(x) < f(x_0)$ for all $x \in C$, with $f \in X^*$ as established in Step 4. The real case is complete. [/step] [step:Reduce the complex case to the real case via the underlying real space] Now suppose $X$ is complex. The space $X$ may be viewed as a real locally convex space $X_\mathbb{R}$ with the same topology — restricting scalar multiplication to $\mathbb{R}$ does not change the seminorms or the topology. The set $C$ is still open and convex in $X_\mathbb{R}$ (real convexity is weaker than complex convexity), and $0 \in C$, $x_0 \notin C$. Apply the real case (Steps 1-5) to $X_\mathbb{R}$: there exists a continuous real-linear functional $u : X_\mathbb{R} \to \mathbb{R}$ with $u(x) < u(x_0)$ for all $x \in C$. Define \begin{align*} f : X &\to \mathbb{C}, \\ x &\mapsto u(x) - i \, u(ix). \end{align*} We verify $f \in X^*$ (the complex dual) with $\operatorname{Re}(f) = u$. *Real-linearity:* immediate, as $u$ is real-linear. *Complex-linearity:* it suffices to check $f(ix) = i f(x)$ for $x \in X$. Compute: \begin{align*} f(ix) = u(ix) - i\, u(i \cdot ix) = u(ix) - i\, u(-x) = u(ix) + i\, u(x) = i(u(x) - i\, u(ix)) = i f(x), \end{align*} using real-linearity of $u$ to extract the sign $u(-x) = -u(x)$. *Continuity:* $f = u - i\, u \circ M_i$ where $M_i : X \to X$, $x \mapsto ix$ is continuous (TVS axiom). Hence $f$ is a $\mathbb{C}$-linear combination of continuous functions, so continuous. *Real part:* $\operatorname{Re}(f(x)) = u(x)$ by construction. For $x \in C$, $\operatorname{Re}(f(x)) = u(x) < u(x_0) = \operatorname{Re}(f(x_0))$, completing the complex case. [guided] The complex case reduces to the real case by a standard device. The space $X$ regarded as a real vector space $X_\mathbb{R}$ has the same underlying set, addition, and topology — only the scalar field changes. Open sets, convex sets (in the **real** sense, which is weaker than complex convex), and continuous real-linear functionals all make sense in $X_\mathbb{R}$. Apply the real case to obtain a continuous $u : X_\mathbb{R} \to \mathbb{R}$ with $u(x) < u(x_0)$ for $x \in C$. The question is: how to upgrade $u$ to a complex-linear $f$? The standard formula is \begin{align*} f : X &\to \mathbb{C}, \\ x &\mapsto u(x) - i\, u(ix). \end{align*} Let us see why this works. Real-linearity of $f$ is inherited from $u$ (and from the fact that $x \mapsto ix$ is real-linear). To get complex-linearity from real-linearity, the only extra check is multiplication by $i$: \begin{align*} f(ix) &= u(ix) - i\, u(i \cdot ix) = u(ix) - i\, u(-x). \end{align*} Since $u$ is real-linear, $u(-x) = -u(x)$, so \begin{align*} f(ix) = u(ix) + i\, u(x) = i(u(x) - i\, u(ix)) = i f(x). \end{align*} This is complex-linearity at $i$, which together with real-linearity gives complex-linearity at every $\alpha + i\beta \in \mathbb{C}$. Continuity: $f$ is the linear combination $u - i \cdot (u \circ M_i)$ where $M_i : x \mapsto ix$ is the multiplication-by-$i$ map. $M_i$ is continuous (TVS axiom: scalar multiplication is jointly continuous, hence continuous in each variable). $u$ is continuous by the real case. So $f$ is continuous. The real part is $\operatorname{Re}(f(x)) = u(x)$ by construction, so the separation $u(x) < u(x_0)$ for $x \in C$ becomes $\operatorname{Re}(f(x)) < \operatorname{Re}(f(x_0))$ for $x \in C$, which is the complex statement. [/guided] [/step]