Prop. 2.1.1 — bounded sets in strict colimits

Proved

GarrettFA.isVonNBounded_iff_of_isStrictColimit

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

functional-analysistopological-vector-spaces

Let $V$ be a locally convex space over $\mathbb K=\mathbb R$ or $\mathbb C$ that is the strict colimit of a chain of closed subspaces $V_0\subsetneq V_1\subsetneq\cdots$ . Then a subset $B\subseteq V$ is bounded if and only if

\exists\, i:\quad B\subseteq V_i\ \text{ and } B \text{ is bounded in } V_i .

This is the Dieudonné–Schwartz description of bounded sets. It reduces boundedness, and hence quasi-completeness, in an LF-space to its Fréchet steps.

Formalization Note $V_i$ carries the subspace topology from $V$ , and "bounded in $V_i$ " is von Neumann boundedness of the preimage of $B$ in the subtype $V_i$ .

Preamble

import Definitions.Def_GarrettFA_IsStrictColimit

Formal statement

namespace GarrettFA
theorem isVonNBounded_iff_of_isStrictColimit {𝕜 : Type*} [RCLike 𝕜] {V : Type*} [AddCommGroup V] [Module 𝕜 V] [Module ℝ V]
    [IsScalarTower ℝ 𝕜 V] [TopologicalSpace V] [IsTopologicalAddGroup V] [ContinuousSMul 𝕜 V]
    [T2Space V] {F : ℕ → Submodule 𝕜 V} (hF : IsStrictColimit 𝕜 F)
    (B : Set V) :
    Bornology.IsVonNBounded 𝕜 B ↔
      ∃ i, B ⊆ F i ∧ Bornology.IsVonNBounded 𝕜 {y : F i | (y : V) ∈ B} := 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. 4, Proposition 2.1.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 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. Let $F_0,F_1,\dots$ be a sequence of $\mathbb K$ -subspaces of $V$ forming a strict colimit presentation of $V$ . 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$ .

Then for every subset $B\subseteq V$ :

B \text{ is bounded in } V \iff \exists i:\ B\subseteq F_i \text{ and } B \text{ (viewed inside } F_i\text{) is bounded in } F_i,

where $F_i$ carries the subspace topology from $V$ . Here bounded means von Neumann bounded over $\mathbb K$ : every neighbourhood of $0$ absorbs the set (for each neighbourhood $U$ of $0$ there is $r>0$ such that the set is contained in $cU$ for all scalars $c\in\mathbb K$ with $|c|\ge r$ ).

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