Is the (algebraic) span a finite set of vectors in a Hausdorff topological vector space over a complete field always closed?


I suspect yes, but I can't come up with a proof, and it seems like locally convex might be needed to get this.



Closedness of finite-dimensional subspaces
This holds indeed for complete fields: see Theorem 2, Section I.2.3, of Bourbaki's "Espaces Vectoriels Topologiques".


Here is the argument.


Let $K$ be a (not necessarily commutative) field equipped with a complete nontrivial [absolute value](http://en.wikipedia.org/wiki/Absolute_value#Fields) $x\mapsto|x|$, let $n$ be a positive integer, let $\tau$ be a Hausdorff vector space topology on $K^n$, and let $\pi$ be the product topology on $K^n$.


**THEOREM** $\tau=\pi$. 


**REMINDER** A topological group $G$ is Hausdorff iff {1} is closed. [Proof: {1} is closed $\Rightarrow$ the diagonal of $G\times G$ is closed (because it's the inverse image of {1} under $(x,y)\mapsto xy^{-1}$) $\Rightarrow$ $G$ is Hausdorff.]


**LEMMA** The Theorem holds for $n=1$.


**The Lemma implies the Theorem.** We argue by induction on $n$. The continuity of the identity from $K^n\_\pi$ to $K^n\_\tau$ (obvious notation) is clear (and doesn't use the Lemma). To prove the continuity of the identity from $K^n\_\tau$ to $K^n\_\pi$, it suffices to prove the continuity of an arbitrary nonzero linear form $f$ from $K^n\_\tau$ to $K\_\pi$. By induction hypothesis, the kernel of $f$ is closed, and the Theorem follows from the Reminder and the Lemma.


**Proof of the Lemma.** We'll use several times the fact that $K^\times$ contains elements of arbitrary large and arbitrary small absolute value. As already observed, we have $\tau\subset\pi$. If $x$ is in $K^\times$, write $B\_x$ for the open ball of radius $|x|$ and center 0 in $K$. Let $a$ be in $K^\times$, and let $\tau\_0$ be the set of those $U$ such that $0\in U\in\tau$. 


It suffices to check that $B\_a$ contains some $U$ in $\tau\_0$. 


We can find a $b$ in $K^\times$ and a $V$ in $\tau\_0$ such that $a$ is not in $B\_bV$, and then a $c$ in $K$ with $|c|>1$ and a $W$ in $\tau\_0$ such that $a$ is not in $B\_cW$. Then $U:=c^{-1}W$ does the job. 


