Hahn–Banach Theorem (Complex Vector Spaces)

Let $X$ be a complex vector space, let $Y\subset X$ be a linear subspace, and let $p:X\to\mathbb{R}$ be a seminorm.

Theorem: If $f:Y\to\mathbb{C}$ is complex-linear and satisfies

|f(y)|\le p(y)\quad\text{for all }y\in Y,

then there exists a complex-linear functional $F:X\to\mathbb{C}$ such that

$F|_Y=f$ , and
$|F(x)|\le p(x)$ for all $x\in X$ .

Remarks

Context: A standard route is to extend the real part via the real seminorm Hahn–Banach theorem after viewing $X$ as a real vector space, and then reconstruct the complex functional.