Prove2Me

Complete topological vector space (Cauchy nets converge)

Definition
GarrettFA_IsNetComplete

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

functional-analysistopological-vector-spaces

Let EE be a topological vector space. With nets, Cauchy nets and convergence as in the definition of quasi-completeness, EE is complete if every Cauchy net in EE converges. No boundedness condition is imposed.

This is the "stronger general notion of completeness" of the notes. It fails, for example, for weak-star duals of infinite-dimensional Fréchet spaces (Theorem 5.0.1 and Corollary 5.0.2).

Formalization Note Index sets are taken in the same universe as EE.

Definition code
import Mathlib

namespace GarrettFA

open Topology

universe u

/-- Garrett, *Completeness and quasi-completeness*, §4. A topological vector space `E` is
complete when every 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₀`, 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 IsNetComplete (E : Type u) [AddCommGroup E] [TopologicalSpace E] : Prop :=
  ∀ (I : Type u) [PartialOrder I] [IsDirected I (· ≤ ·)] (v : I → E),
    (∀ 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 of completeness preceding Proposition 4.0.1
Read-back

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

Defines a property of a type EE with an additive commutative group structure and a topology (no compatibility between them is required by the definition). EE is called net-complete when: for every index type II in the same universe as EE, with a directed partial order (any two elements have a common upper bound; nonemptiness is not required), and every function v:I→Ev:I\to E satisfying

∀N∈N(0) ∃i0∈I ∀i≥i0 ∀j≥i0: vi−vj∈N,\forall N\in\mathcal N(0)\ \exists i_0\in I\ \forall i\ge i_0\ \forall j\ge i_0:\ v_i-v_j\in N,

there is x∈Ex\in E with

∀N∈N(0) ∃i0∈I ∀i≥i0: vi−x∈N.\forall N\in\mathcal N(0)\ \exists i_0\in I\ \forall i\ge i_0:\ v_i-x\in N.

Here N(0)\mathcal N(0) is the set of neighbourhoods of 00 in EE. No boundedness assumption is made on vv. An empty II never satisfies the hypothesis (take N=EN=E). Index types in larger universes are not considered.

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