LF-space (strict colimit of Fréchet spaces)

Definition

GarrettFA_IsLFSpace

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

functional-analysistopological-vector-spaces

A topological vector space $V$ over $\mathbb K=\mathbb R$ or $\mathbb C$ is an LF-space if there is a chain of subspaces $V_0\subsetneq V_1\subsetneq\cdots$ such that $V$ is the strict colimit of the $V_n$ and every $V_n$ , with the subspace topology, is a Fréchet space, i.e. metrizable and complete. Each $V_n$ is locally convex automatically, as a subspace of the locally convex space $V$ .

Examples are the spaces of test functions $C_c^\infty(\mathbb R^n)$ and $C_c^o(\mathbb R^n)$ , and $\mathbb C^\infty$ .

Formalization Note Completeness of $V_n$ is completeness of $V_n$ as a subset of $V$ for the uniform structure of $V$ .

Definition code

import Definitions.Def_GarrettFA_IsStrictColimit

namespace GarrettFA

/-- Garrett, *Completeness and quasi-completeness*, §1.3: an LF-space is a strict colimit of a
countable chain of Fréchet spaces. Here `V` is the strict colimit of the chain `F` and each
`F n`, with the subspace topology and uniformity from `V`, is metrizable and complete
(it is automatically locally convex, being a subspace of a locally convex space). -/
def IsLFSpace (𝕜 : Type*) (V : Type*) [RCLike 𝕜] [AddCommGroup V] [Module 𝕜 V]
    [Module ℝ V] [IsScalarTower ℝ 𝕜 V] [UniformSpace V] : Prop :=
  ∃ F : ℕ → Submodule 𝕜 V, IsStrictColimit 𝕜 F ∧
    ∀ n, TopologicalSpace.MetrizableSpace (F n) ∧ IsComplete (F n : Set V)

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. 1 and p. 2, §1.3 ("A strict colimit of Fréchet spaces is an LF-space")

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic)

Defines a property of a type $V$ given a real-or-complex scalar field $\mathbb K$ (in practice $\mathbb R$ or $\mathbb C$ ), a $\mathbb K$ -vector space structure on $V$ , a compatible real vector space structure, and a uniform structure on $V$ . $V$ is an LF-space when there exists a sequence $F_0,F_1,\dots$ of $\mathbb K$ -subspaces of $V$ such that

$(F_n)$ is a strict colimit presentation of $V$ (all five conditions: proper inclusions $F_n\subsetneq F_m$ for $n<m$ ; $V=\bigcup_n F_n$ ; $F_n$ closed in $F_{n+1}$ ; $V$ locally convex in the real sense; every $\mathbb K$ -balanced real-convex $U\subseteq V$ whose trace on each $F_n$ is a neighbourhood of $0$ in $F_n$ is a neighbourhood of $0$ in $V$ , all subspaces carrying the topology induced from $V$ ), and
for every $n$ : $F_n$ with the subspace topology from $V$ is metrizable, and $F_n$ is a complete subset of $V$ for the uniform structure of $V$ (every Cauchy filter on $V$ containing $F_n$ converges to a point of $F_n$ ).

Local convexity of each $F_n$ is not stated separately. The definition does not itself require continuity of the vector operations.

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