Prop. 2.2.1 — equicontinuity on strict colimits

Proved

GarrettFA.isEquicontinuousSet_iff_of_isStrictColimit

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

functional-analysistopological-vector-spaces

Let $V$ be the strict colimit of a chain of closed subspaces $V_0\subsetneq V_1\subsetneq\cdots$ (over $\mathbb K=\mathbb R$ or $\mathbb C$ ), let $Y$ be a locally convex topological vector space, and let $E$ be a set of continuous linear maps $V\to Y$ . Then

E \text{ is equicontinuous} \iff \text{for every } i,\ \{T|_{V_i} : T\in E\} \text{ is equicontinuous}.

Equicontinuity on an LF-space can therefore be checked on its Fréchet steps. This is how Banach–Steinhaus passes from Fréchet spaces to LF-spaces.

Preamble

import Definitions.Def_GarrettFA_IsStrictColimit
import Definitions.Def_GarrettFA_IsEquicontinuousSet

Formal statement

namespace GarrettFA
theorem isEquicontinuousSet_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)
    {Y : Type*} [AddCommGroup Y] [Module 𝕜 Y] [Module ℝ Y] [IsScalarTower ℝ 𝕜 Y]
    [TopologicalSpace Y] [IsTopologicalAddGroup Y] [ContinuousSMul 𝕜 Y] [LocallyConvexSpace ℝ Y]
    [T2Space Y]
    (E : Set (V →L[𝕜] Y)) :
    IsEquicontinuousSet ((fun T : V →L[𝕜] Y => (T : V → Y)) '' E) ↔
      ∀ i, IsEquicontinuousSet ((fun T : V →L[𝕜] Y => fun y : F i => T y) '' E) := 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.2.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$ ). 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, and let $F_0,F_1,\dots$ be $\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$ .

Let $Y$ 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 Y\to Y$ is jointly continuous, and which is Hausdorff, which is moreover locally convex as a real topological vector space. Let $E$ be any set of continuous $\mathbb K$ -linear maps $V\to Y$ . Then

\{T : T\in E\}\text{ is equicontinuous} \iff \text{for every } i,\ \{T|_{F_i} : T\in E\}\text{ is equicontinuous},

where $T|_{F_i}:F_i\to Y$ is the restriction and $F_i$ has the subspace topology from $V$ . Equicontinuous (the bundle's definition): for every neighbourhood $U$ of $0$ in the target there is a neighbourhood $N$ of $0$ in the source with $T(N)\subseteq U$ for every map $T$ in the family.

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