The following result is presented in many sources on topological vector spaces (TVSes):
Any finite-dimensional subspace of a Hausdorff TVS is closed.
However, having had a look at various sources, I've yet to come across one that doesn't seem to have something "off" about the proof. Here for example is the proof given by Terry Tao (https://terrytao.wordpress.com/2011/05/24/locally-compact-topological-vector-spaces/):
Corollary 3 In a Hausdorff topological vector space $V$, every finite-dimensional subspace $W$ is closed.
Proof: It suffices to show that every vector $x \in V \setminus W$ is in the exterior of $W$. But this follows from Theorem 2 [which states that every finite-dimensional Hausdorff TVS is linearly homeomorphic to $\mathbb R^n$ – kahen] after restricting to the finite-dimensional space spanned by $W$ and $x$.
But as far as I can tell this only tells us that $x$ is in the exterior of $W$ in $\operatorname{span}(\{x\} \cup W)$, from which it doesn't seem to follow that $x$ is in the exterior of $W$ in all of $V$.
Another proof strategy would be to appeal to completeness of the finite-dimensional subspace. But I've yet to see a proof that doesn't appear to implicitly assume that the uniformity induced on the subspace from the enclosing space must be the same as the one produced by pulling one back through a linear homeomorphism with $\mathbb R^n$.
One could also try to appeal to some continuity and/or compactness argument such as Corollary 0.9 in this short note: http://users.mat.unimi.it/users/libor/AnConvessa/TVS.pdf. Here the enclosing space is named $X$ and the subspace $Y$, and the proof goes by taking an $x_0 \in \overline Y$ and trying to show that it is actually in $Y$. First continuity of the product is used to show that there is an open neighbourhood $V$ of $0$ in $X$ such that $V \cap Y$ is a subset of a unit ball w.r.t. some norm on $Y$, and that there is a $\lambda > 0$ such that $x_0 \in \lambda V$. Putting it all together we get $x_0 \in \lambda V \cap Y = \lambda(V \cap Y)$ which is a subset of $\lambda$ times the unit ball in $Y$ which is closed.
So far, so good, but then the proof states that $x_0 \in \overline{\lambda V \cap Y}$ (from which the result follows readily). But this doesn't seem quite right to me since we know $x_0 \in \lambda V$ and $x_0 \in \overline Y$, so certainly we have $x_0 \in \overline{\lambda V \cap \overline Y}$ as well as $x_0 \in \overline{\lambda V} \cap \overline Y$, but there doesn't seem to be a way to get from either of those to $x_0 \in \overline{\lambda V \cap Y}$.
Does anyone have a good (preferably online) reference for a proof of this result?
Tao's proof does work. Letting $X=\operatorname{span}(\{x\} \cup W)$, you know that $x$ is in the exterior of $W$ in $X$. By definition of the topology on $X$, this means there is an open set $U\subseteq V$ such that $x\in U\cap X$ and $U\cap X$ is disjoint from $W$. But then $U$ itself is also disjoint from $W$, so $U$ witnesses that $x$ is in the exterior of $W$ in $V$ as well.