Claim 5.0.4 — $V_{\mathrm{init}}$ is the finest locally convex topology

Proved

GarrettFA.continuous_id_of_isInitTopology

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

functional-analysistopological-vector-spaces

Let $V$ be a vector space over $\mathbb K=\mathbb R$ or $\mathbb C$ whose (Hausdorff) topology is the topology of $V_{\rm init}$ . Let $\tau$ be any locally convex topological vector space topology on $V$ . Then

\mathrm{id} : V_{\rm init} \to (V,\tau) \ \text{ is continuous},

so $V_{\rm init}$ is the finest locally convex topological vector space topology on $V$ .

Preamble

import Definitions.Def_GarrettFA_IsInitTopology

Formal statement

namespace GarrettFA
theorem continuous_id_of_isInitTopology {𝕜 : Type*} [RCLike 𝕜] {V : Type*} [AddCommGroup V] [Module 𝕜 V] [Module ℝ V]
    [IsScalarTower ℝ 𝕜 V] (τ : TopologicalSpace V) (h₁ : @IsTopologicalAddGroup V τ _)
    (h₂ : @ContinuousSMul 𝕜 V _ _ τ) (h₃ : @LocallyConvexSpace ℝ V _ _ _ _ τ)
    [TopologicalSpace V] [IsTopologicalAddGroup V] [ContinuousSMul 𝕜 V] [T2Space V]
    (hV : IsInitTopology 𝕜 V) :
    @Continuous V V _ τ id := 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, Claim 5.0.4

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 a $\mathbb K$ -vector space that is also a real vector space with compatible scalar multiplications (multiplying by a real number $r$ is the same as multiplying by $r\in\mathbb K$ ), carrying a topology in which addition and negation are continuous, scalar multiplication $\mathbb K\times V\to V$ is jointly continuous, and which is Hausdorff, whose topology is the initial topology. $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$ .

Let $\tau$ be any other topology on $V$ for which addition and negation are continuous, scalar multiplication by $\mathbb K$ is jointly continuous, and which is locally convex as a real topological vector space ( $\tau$ is not required to be Hausdorff). Then the identity map from $V$ with its given topology to $V$ with $\tau$ is continuous; that is, the given topology is at least as fine as $\tau$ .

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

Claim 5.0.4 — VinitV_{\mathrm{init}}Vinit​ is the finest locally convex topology

Claim 5.0.4 — $V_{\mathrm{init}}$ is the finest locally convex topology