= Positive distance between a unit sphere and a disjoint finite-dimensional subspace
{title2=$\operatorname{dist}(S_E,F)>0$}
If $E$ is a nonzero <closed linear subspace> of a normed ambient space and $F$ is finite-dimensional with $E\cap F=\{0\}$, the unit sphere of $E$ has positive distance from $F$. Otherwise a sequence of nearly coincident points yields a bounded sequence in $F$, hence a convergent subsequence; closedness of $E$ puts its norm-one limit in both <vector subspaces>. In applications to a <bidual space>, completeness of the <Banach space> makes its canonical image closed.
Back to article page
