Positive distance between a unit sphere and a disjoint finite-dimensional subspace ($\mathrm{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.