§5 — existence of the finest locally convex topology $V_{\mathrm{init}}$

Proved

GarrettFA.exists_isInitTopology

by Lucas · Oct 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

functional-analysistopological-vector-spaces

Every vector space $V$ over $\mathbb K=\mathbb R$ or $\mathbb C$ carries a Hausdorff topological vector space topology that is the topology of $V_{\rm init}$ , the locally convex colimit of its finite-dimensional subspaces.

This guarantees that the predicate describing $V_{\rm init}$ is not vacuous.

Preamble

import Definitions.Def_GarrettFA_IsInitTopology

Formal statement

namespace GarrettFA
theorem exists_isInitTopology {𝕜 : Type*} [RCLike 𝕜] {V : Type*}
    [AddCommGroup V] [Module 𝕜 V] [Module ℝ V] [IsScalarTower ℝ 𝕜 V] :
    ∃ τ : TopologicalSpace V, @IsTopologicalAddGroup V τ _ ∧ @ContinuousSMul 𝕜 V _ _ τ ∧
      @T2Space V τ ∧ @IsInitTopology 𝕜 V _ _ _ _ _ τ := by sorry
end GarrettFA

Source

Paul Garrett, *Completeness and quasi-completeness* (lecture notes, April 24, 2014), http://www.math.umn.edu/~garrett/m/fun/notes_2012-13/07d_quasi-completeness.pdf, p. 8, §5 ("V_init = locally-convex colimit of finite-dimensional X ⊂ V"; existence of locally convex colimits, §1)

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic)

Let $\mathbb K$ be a real-or-complex scalar field (in practice $\mathbb R$ or $\mathbb C$ ), and let $V$ be any $\mathbb K$ -vector space that is also a real vector space with compatible scalar multiplications (no topology is given; $V$ may be the zero space or of any dimension). Then there exists a topology $\tau$ on $V$ such that, simultaneously: addition and negation are continuous for $\tau$ ; scalar multiplication $\mathbb K\times V\to V$ is jointly continuous for $\tau$ ; $\tau$ is Hausdorff; and $\tau$ is the initial topology on $V$ . $V$ carries the initial (finest locally convex) topology (the bundle's definition): (i) $V$ is locally convex as a real topological vector space, and (ii) every subset $U\subseteq V$ that is balanced over $\mathbb K$ and convex in the real sense, and whose trace $U\cap W$ is a neighbourhood of $0$ in $W$ (subspace topology from $V$ ) for every finite-dimensional $\mathbb K$ -subspace $W$ of $V$ , is a neighbourhood of $0$ in $V$ .

Human review

Endorsed by Shuze Chen · Oct 13, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 13, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

§5 — existence of the finest locally convex topology VinitV_{\mathrm{init}}Vinit​

§5 — existence of the finest locally convex topology $V_{\mathrm{init}}$