Cor. 5.0.2 (LF case, corrected) — weak duals of LF-spaces with an infinite-dimensional step are not complete

Proved

GarrettFA.not_isNetComplete_weakDual_of_isStrictColimit

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

functional-analysistopological-vector-spaces

Let $X$ be an LF-space over $\mathbb K=\mathbb R$ or $\mathbb C$ : the strict colimit of a chain $X_0\subsetneq X_1\subsetneq\cdots$ of closed subspaces, each metrizable and complete. If some step $X_n$ is infinite-dimensional, then the weak dual of $X$ is not complete.

This covers the spaces of test functions $C_c^\infty(\mathbb R^n)$ , $n\ge1$ .

Formalization Note The notes state the corollary for all infinite-dimensional LF-spaces. That is false for the LF-space $\mathbb C^\infty$ of Example 1.3.1, the strict colimit of the finite-dimensional spaces $\mathbb C^n$ . Its topology is the finest locally convex topology, so every linear functional is continuous and its weak dual $\mathbb C^{\mathbb N}$ is complete by Theorem 5.0.1. The hypothesis "some step is infinite-dimensional" excludes exactly the LF-spaces of countable dimension.

Preamble

import Definitions.Def_GarrettFA_IsNetComplete
import Definitions.Def_GarrettFA_IsStrictColimit

Formal statement

namespace GarrettFA
theorem not_isNetComplete_weakDual_of_isStrictColimit {𝕜 : Type*} [RCLike 𝕜] {X : Type*} [AddCommGroup X] [Module 𝕜 X] [Module ℝ X]
    [IsScalarTower ℝ 𝕜 X] [UniformSpace X] [IsUniformAddGroup X] [ContinuousSMul 𝕜 X] [T2Space X]
    {F : ℕ → Submodule 𝕜 X} (hF : IsStrictColimit 𝕜 F)
    (hFr : ∀ n, TopologicalSpace.MetrizableSpace (F n) ∧ IsComplete (F n : Set X))
    (hinf : ∃ n, ¬ FiniteDimensional 𝕜 (F n)) :
    ¬ IsNetComplete (WeakDual 𝕜 X) := 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, Corollary 5.0.2 (LF case; restricted to LF-spaces having an infinite-dimensional step, see the note)

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 $X$ be a $\mathbb K$ -vector space that is also a real vector space with compatible scalar multiplications, carrying a uniform structure for which addition and subtraction are uniformly continuous (so the uniformity is the canonical translation-invariant uniformity of the induced topology), with scalar multiplication $\mathbb K\times X\to X$ jointly continuous, and Hausdorff. Let $F_0,F_1,\dots$ be $\mathbb K$ -subspaces of $X$ forming a strict colimit presentation of $X$ . Strict colimit of the sequence of $\mathbb K$ -subspaces $F_0,F_1,F_2,\dots$ of $V$ (the bundle's definition): (i) $F_n\subsetneq F_m$ whenever $n<m$ ; (ii) every $x\in V$ lies in some $F_n$ ; (iii) for each $n$ , $F_n$ is a closed subset of $F_{n+1}$ , where $F_{n+1}$ has the subspace topology from $V$ ; (iv) $V$ is locally convex as a real topological vector space; (v) every subset $U\subseteq V$ that is balanced over $\mathbb K$ (i.e. $cU\subseteq U$ whenever $|c|\le1$ ) and convex in the real sense, and whose trace $U\cap F_n$ is a neighbourhood of $0$ in $F_n$ (subspace topology from $V$ ) for every $n$ , is a neighbourhood of $0$ in $V$ .

Assume moreover that for every $n$ , $F_n$ with the subspace topology is metrizable and $F_n$ is a complete subset of $X$ for the uniform structure of $X$ , and that some $F_n$ is not finite-dimensional over $\mathbb K$ . Then the weak dual of $X$ (continuous $\mathbb K$ -linear functionals on $X$ with the topology of pointwise convergence) is not net-complete. Net-complete (the bundle's definition): for every index type $I$ (in the same universe as the space) carrying a partial order in which any two elements have a common upper bound, every family $(v_i)_{i\in I}$ that is Cauchy (for every neighbourhood $N$ of $0$ there is $i_0$ with $v_i-v_j\in N$ for all $i,j\ge i_0$ ) has a point $x$ with $v_i-x\in N$ for all $i\ge$ some $i_0$ , for every neighbourhood $N$ of $0$ . No boundedness is required.

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