Topological Dual Space of Hausdorff Locally Convex Space Separates Points

Theorem

Let $\GF \in \set {\R, \C}$.

Let $\struct {X, \PP}$ be a Hausdorff locally convex space over $\GF$.

Let $X^\ast$ be the topological dual of $X$.

Let $x \in X$.

Then $X^\ast$ separates points.

That is, if $x, y \in X$ are such that:

$\map f x = \map f y$ for all $f \in X^\ast$

we have that $x = y$.

Proof

Suppose $x \ne y$.

It suffices to find $f \in X^\ast$ such that $\map f x \ne \map f y$.

From Finite Topological Space is Compact, $\set {\mathbf 0_X}$ is compact.

From Compact Subspace of Hausdorff Space is Closed, $\set {\mathbf 0_X}$ is closed.

Since $x \ne y$, we have:

$x - y \not \in X \setminus \set {\mathbf 0_X}$

From Existence of Non-Zero Continuous Linear Functional vanishing on Proper Closed Subspace of Hausdorff Locally Convex Space, there exists $f \in X^\ast$ such that:

$\map f {x - y} \ne 0$

That is:

$\map f x \ne \map f y$

$\blacksquare$