Thm. 5.0.1 — completeness of weak duals

Proved

GarrettFA.weakDual_isNetComplete_iff

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

functional-analysistopological-vector-spaces

Let $V$ be a Hausdorff locally convex topological vector space over $\mathbb K=\mathbb R$ or $\mathbb C$ , and let $V^*_\sigma$ be its weak dual: the continuous linear functionals with the topology of pointwise convergence on $V$ . Then

V^*_\sigma \text{ is complete} \iff \text{every linear functional } V\to\mathbb K \text{ is continuous}.

Here complete means that every Cauchy net converges.

Formalization Note The weak dual is Mathlib's WeakDual 𝕜 V.

Preamble

import Definitions.Def_GarrettFA_IsNetComplete

Formal statement

namespace GarrettFA
theorem weakDual_isNetComplete_iff {𝕜 : Type*} [RCLike 𝕜] {V : Type*} [AddCommGroup V] [Module 𝕜 V] [Module ℝ V]
    [IsScalarTower ℝ 𝕜 V] [TopologicalSpace V] [IsTopologicalAddGroup V] [ContinuousSMul 𝕜 V]
    [T2Space V]
    [LocallyConvexSpace ℝ V] :
    IsNetComplete (WeakDual 𝕜 V) ↔ ∀ f : V →ₗ[𝕜] 𝕜, Continuous f := 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. 8, Theorem 5.0.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$ ), and 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, which is moreover locally convex as a real topological vector space. Let $V'_\sigma$ be the weak dual of $V$ : the continuous $\mathbb K$ -linear functionals $V\to\mathbb K$ , with the topology of pointwise convergence on $V$ (weak- $*$ topology). Then

V'_\sigma \text{ is net-complete} \iff \text{every } \mathbb K\text{-linear map } f:V\to\mathbb K \text{ is continuous}.

Net-complete (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, every family $(v_i)_{i\in I}$ that 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$ ) has a point $x$ with $v_i-x\in N$ for all $i\ge$ some $i_0$ , for every neighbourhood $N$ of $0$ . No boundedness is required.

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