1 Mise en bouche
The usual topology on \(\mathbb {R}^{n}\) is the only Hausdorff topology that makes it a topological vector space.
Let \(\mathcal{T}\) be a Hausdorff topology on \(\mathbb {R}^n\) making it a topological vector space. The identity map \(\operatorname {id}\colon \bigl(\mathbb {R}^n\bigr){\text{can}}\to \bigl(\mathbb {R}^n\bigr)_{\mathcal{T}}\), where the first space is endowed with the usual topology and the second with \(\mathcal{T}\) is a continuous (linear) bijection between Hausdorff spaces, and it is therefore a homeomorphism.
Of course, the whole point is to state this in Lean.
The only topological vector space over \(\mathbb {R}\) with the discrete topology is the zero space.
Let \(E\) be a discrete, real, topological vector space: for every \(v\in E\), y continuity of the multiplication, the line \(\mathbb {R}\cdot v\) is both connected and discrete, so it is a singleton. This shows \(v=0\).