Claim 5.0.5 — every linear functional on $V_{\mathrm{init}}$ is continuous

Proved

GarrettFA.continuous_linearMap_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}$ . Then every linear functional

\lambda : V\to\mathbb K

is continuous.

Preamble

import Definitions.Def_GarrettFA_IsInitTopology

Formal statement

namespace GarrettFA
theorem continuous_linearMap_of_isInitTopology {𝕜 : Type*} [RCLike 𝕜] {V : Type*} [AddCommGroup V] [Module 𝕜 V] [Module ℝ V]
    [IsScalarTower ℝ 𝕜 V] [TopologicalSpace V] [IsTopologicalAddGroup V] [ContinuousSMul 𝕜 V]
    [T2Space V]
    (hV : IsInitTopology 𝕜 V) (f : V →ₗ[𝕜] 𝕜) :
    Continuous f := 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.5

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$ .

Then every $\mathbb K$ -linear map $f:V\to\mathbb K$ is continuous (for the usual topology on $\mathbb K$ ).

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.5 — every linear functional on VinitV_{\mathrm{init}}Vinit​ is continuous

Claim 5.0.5 — every linear functional on $V_{\mathrm{init}}$ is continuous