Claim 5.0.7 — the weak dual of $V_{\mathrm{init}}$ is the whole limit

Proved

GarrettFA.range_weakDual_coeFn_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 the image of its weak dual under $\lambda\mapsto(\lambda(v))_{v\in V}$ is exactly the set of all linear functionals:

\{\,(\lambda(v))_{v\in V} : \lambda\in V_{\rm init}^*\,\} = \{\, g:V\to\mathbb K \ :\ g \text{ linear}\,\}.

Formalization Note With the identification described for Claim 5.0.6, $\lim_\Phi V^*_\Phi$ is the space of all linear functionals on $V$ inside $\mathbb K^V$ , so "the weak dual of $V_{\rm init}$ is the limit" becomes the equality of images above.

Preamble

import Definitions.Def_GarrettFA_IsInitTopology

Formal statement

namespace GarrettFA
theorem range_weakDual_coeFn_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) :
    Set.range (fun f : WeakDual 𝕜 V => (f : V → 𝕜)) = {g : V → 𝕜 | IsLinearMap 𝕜 g} := 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. 9, Claim 5.0.7

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 the set of underlying functions $V\to\mathbb K$ of elements of the weak dual of $V$ (continuous $\mathbb K$ -linear functionals) is exactly the set of all $\mathbb K$ -linear functions $V\to\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.7 — the weak dual of VinitV_{\mathrm{init}}Vinit​ is the whole limit

Claim 5.0.7 — the weak dual of $V_{\mathrm{init}}$ is the whole limit