Separability of the continuous dual implies separability (source code)

= Separability of the continuous dual implies separability

If the <continuous dual space> $X'$ of a <normed vector space> is norm separable, then $X$ is <separable>. Choose a dense sequence $f_n$ in the dual unit ball and unit-ball points $x_n$ with $|f_n(x_n)|\geq\|f_n\|/2$. If their closed <linear span> were proper, the <Hahn-Banach distance formula> would give a norm-one functional $f$ vanishing on it. An $f_n$ within $1/4$ of $f$ would simultaneously satisfy $|f_n(x_n)|<1/4$ and $|f_n(x_n)|>3/8$, a contradiction. Rational linear combinations give a countable dense subset of $X$.

The converse fails by <duality of l1 and l infinity>: $\ell^1$ is separable, whereas $\ell^\infty$ contains uncountably many zero-one sequences at mutual <distance> one.