Quasi-complete topological vector space

Definition

GarrettFA_IsQuasiComplete

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

functional-analysistopological-vector-spaces

Let $E$ be a topological vector space over a normed field $\mathbb K$ . A net in $E$ is a map $v : I \to E$ from a directed partially ordered set $I$ . The net is Cauchy if for every neighbourhood $N$ of $0$ there is $i_0\in I$ with $v_i - v_j \in N$ for all $i, j \ge i_0$ . It is bounded if its set of values $\{v_i\}$ is a bounded subset of $E$ (absorbed by every neighbourhood of $0$ ). It converges to $x$ if for every neighbourhood $N$ of $0$ there is $i_0$ with $v_i - x \in N$ for all $i\ge i_0$ .

The space $E$ is quasi-complete if every bounded Cauchy net in $E$ converges.

This is the general completeness notion used throughout the notes. It is weaker than completeness but holds for all Fréchet spaces, LF-spaces, weak-star duals of these, and spaces of operators with the pointwise topology.

Formalization Note Boundedness is Mathlib's von Neumann boundedness. Index sets are taken in the same universe as $E$ ; this loses nothing, since every Cauchy net gives a Cauchy filter, which is again represented by a net indexed in that universe.

Definition code

import Mathlib

namespace GarrettFA

open Topology

universe u

/-- Garrett, *Completeness and quasi-completeness*, Definition 4.0.2.
A topological vector space `E` over `𝕜` is quasi-complete when every bounded Cauchy net
converges. A net is a map `v : I → E` from a directed partially ordered set `I`; it is
Cauchy when for every neighbourhood `N` of `0` there is `i₀` with `v i - v j ∈ N` for all
`i, j ≥ i₀`, bounded when its set of values is von Neumann bounded, and it converges to `x`
when for every neighbourhood `N` of `0` there is `i₀` with `v i - x ∈ N` for all `i ≥ i₀`.
Index sets are taken in the same universe as `E`. -/
def IsQuasiComplete (𝕜 : Type*) (E : Type u) [SeminormedRing 𝕜] [AddCommGroup E] [SMul 𝕜 E]
    [TopologicalSpace E] : Prop :=
  ∀ (I : Type u) [PartialOrder I] [IsDirected I (· ≤ ·)] (v : I → E),
    Bornology.IsVonNBounded 𝕜 (Set.range v) →
    (∀ N ∈ 𝓝 (0 : E), ∃ i₀ : I, ∀ i ≥ i₀, ∀ j ≥ i₀, v i - v j ∈ N) →
    ∃ x : E, ∀ N ∈ 𝓝 (0 : E), ∃ i₀ : I, ∀ i ≥ i₀, v i - x ∈ N

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, Definition 4.0.2 (with the definitions of bounded set, directed set, net, convergent net and Cauchy net on pp. 5–6)

Read-back

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

Defines a property of a type $E$ given a seminormed ring of scalars $\mathbb K$ , an additive commutative group structure on $E$ , an action of $\mathbb K$ on $E$ (no compatibility axioms are required by the definition itself), and a topology on $E$ . $E$ is called quasi-complete over $\mathbb K$ when the following holds:

For every index type $I$ lying in the same universe as $E$ , equipped with a partial order $\le$ that is directed (any two elements have a common upper bound; $I$ is not required to be nonempty), and every function $v:I\to E$ such that

the set of values $\{v_i : i\in I\}$ is von Neumann bounded over $\mathbb K$ (every neighbourhood of $0$ absorbs it), and
for every neighbourhood $N$ of $0$ in $E$ there is $i_0\in I$ with $v_i-v_j\in N$ for all $i\ge i_0$ and $j\ge i_0$ ,

there exists $x\in E$ such that for every neighbourhood $N$ of $0$ there is $i_0\in I$ with $v_i-x\in N$ for all $i\ge i_0$ .

Edge cases: if $I$ is empty then condition 2 fails (it asks for some $i_0\in I$ even for $N=E$ ), so empty families impose nothing. Convergence and the Cauchy condition are phrased with differences and neighbourhoods of $0$ , not with a uniform structure. Index types in larger universes are not quantified over.

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