Finite-codimensional weak-star dense dual subspace is norming (source code)

= Finite-codimensional weak-star dense dual subspace is norming
{title2=$c=\operatorname{dist}(S_X,Y^\perp)>0$}

Let $X$ be a <Banach space>, and let $Y\subseteq X^*$ be a norm-closed <linear subspace> with <finite codimension>, dense for the <weak-star topology>. Then $Y$ is a <norming subspace>: some $c>0$ satisfies
$$
\sup_{y\in Y,\ \|y\|\leq1}|y(x)|\geq c\|x\|\qquad(x\in X).
$$
Put $F=Y^\perp\subseteq X^{**}$. <Finite codimension> makes $F$ finite-dimensional, while density for the <weak-star topology> gives $F\cap JX=\{0\}$. The <canonical embedding into the bidual> has closed image $JX$, whose <unit sphere> has positive distance from $F$: otherwise bounded approximants in $F$ have a <convergent subsequence> with a nonzero <limit> in both spaces. The <Hahn-Banach theorem> identifies the <norm> of evaluation restricted to $Y$ with $\operatorname{dist}(Jx,F)$, proving the bound. <Completeness> of $X$ is needed for this closedness argument.