Thm. 4.1.1 — quasi-completeness of $\mathrm{Hom}^o(X,Y)$ with the pointwise topology

Proved

GarrettFA.isQuasiComplete_pointwiseConvergenceCLM

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

functional-analysistopological-vector-spaces

Let $X$ be a Fréchet space or an LF-space and let $Y$ be a Hausdorff, locally convex, quasi-complete topological vector space, both over $\mathbb K=\mathbb R$ or $\mathbb C$ . Let $\mathrm{Hom}^o(X,Y)$ be the space of continuous linear maps $X\to Y$ with the topology given by the seminorms

p_{x,U}(T)=\inf\{\,t>0 : Tx\in tU\,\}\qquad(x\in X,\ U \text{ a convex balanced neighbourhood of } 0 \text{ in } Y).

Then

\mathrm{Hom}^o(X,Y)\ \text{ is quasi-complete.}

For Hilbert spaces $X,Y$ this topology is the strong operator topology; replacing $Y$ by its weak topology gives the weak operator topology.

Formalization Note $\mathrm{Hom}^o(X,Y)$ is Mathlib's space X →Lₚₜ[𝕜] Y of continuous linear maps with the topology of pointwise convergence. Since $Y$ is locally convex, convex balanced neighbourhoods form a basis at $0$ , so this is the $p_{x,U}$ -topology. $Y$ is assumed locally convex and Hausdorff, the standing conventions of the notes; the notes' proof uses both.

Preamble

import Definitions.Def_GarrettFA_IsQuasiComplete
import Definitions.Def_GarrettFA_IsFrechetSpace
import Definitions.Def_GarrettFA_IsLFSpace
open scoped PointwiseConvergenceCLM

Formal statement

namespace GarrettFA
theorem isQuasiComplete_pointwiseConvergenceCLM {𝕜 : Type*} [RCLike 𝕜] {X : Type*} [AddCommGroup X] [Module 𝕜 X] [Module ℝ X]
    [IsScalarTower ℝ 𝕜 X] [UniformSpace X] [IsUniformAddGroup X] [ContinuousSMul 𝕜 X] [T2Space X]
    (hX : IsFrechetSpace 𝕜 X ∨ IsLFSpace 𝕜 X)
    {Y : Type*} [AddCommGroup Y] [Module 𝕜 Y] [Module ℝ Y] [IsScalarTower ℝ 𝕜 Y]
    [TopologicalSpace Y] [IsTopologicalAddGroup Y] [ContinuousSMul 𝕜 Y] [LocallyConvexSpace ℝ Y]
    [T2Space Y]
    (hY : IsQuasiComplete 𝕜 Y) :
    IsQuasiComplete 𝕜 (X →Lₚₜ[𝕜] Y) := 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. 6, Theorem 4.1.1 (with the topology of §4.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 $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, and assume $X$ is Fréchet or $X$ is an LF-space. Fréchet (the bundle's definition, applied to the given uniform structure): locally convex as a real topological vector space, the topology is metrizable, and the space is complete for its uniform structure (every Cauchy filter converges). LF-space (the bundle's definition): there exists a sequence of $\mathbb K$ -subspaces $F_0,F_1,\dots$ of the space such that the space is the strict colimit of $(F_n)$ in the sense above, and for every $n$ the subspace $F_n$ , with the subspace topology, is metrizable, and $F_n$ is a complete subset for the ambient uniform structure.

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, and assume $Y$ is quasi-complete over $\mathbb K$ .

Then the space $\mathcal L_p(X,Y)$ of continuous $\mathbb K$ -linear maps $X\to Y$ , with pointwise addition and scalar multiplication and with the topology of pointwise convergence (the coarsest topology making every evaluation $T\mapsto Tx$ , $x\in X$ , continuous), is quasi-complete over $\mathbb K$ . Quasi-complete over $\mathbb K$ (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, and every family $(v_i)_{i\in I}$ whose set of values is von Neumann bounded over $\mathbb K$ and which 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$ ), there is a point $x$ with $v_i-x\in N$ eventually (for all $i\ge$ some $i_0$ ) for every neighbourhood $N$ of $0$ .

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

Thm. 4.1.1 — quasi-completeness of Homo(X,Y)\mathrm{Hom}^o(X,Y)Homo(X,Y) with the pointwise topology

Thm. 4.1.1 — quasi-completeness of $\mathrm{Hom}^o(X,Y)$ with the pointwise topology