Prove2Me
Navigate
DiscoverCollectionsFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

Cor. 5.0.2 — weak duals of infinite-dimensional Fréchet spaces are not complete

Proved
GarrettFA.not_isNetComplete_weakDual_of_isFrechetSpace

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

functional-analysistopological-vector-spaces

Let XXX be an infinite-dimensional Fréchet space over K=R\mathbb K=\mathbb RK=R or C\mathbb CC, for instance an infinite-dimensional Banach or Hilbert space. Then its weak dual is not complete: some Cauchy net in Xσ∗X^*_\sigmaXσ∗​ does not converge.

Preamble
import Definitions.Def_GarrettFA_IsNetComplete
import Definitions.Def_GarrettFA_IsFrechetSpace
Formal statement
namespace GarrettFA
theorem not_isNetComplete_weakDual_of_isFrechetSpace {𝕜 : Type*} [RCLike 𝕜] {X : Type*} [AddCommGroup X] [Module 𝕜 X] [Module ℝ X]
    [IsScalarTower ℝ 𝕜 X] [UniformSpace X] [IsUniformAddGroup X] [ContinuousSMul 𝕜 X] [T2Space X]
    (hX : IsFrechetSpace 𝕜 X) (hinf : ¬ FiniteDimensional 𝕜 X) :
    ¬ IsNetComplete (WeakDual 𝕜 X) := 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, Corollary 5.0.2 (Hilbert, Banach and Fréchet cases)
Read-back

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

Let K\mathbb KK be a real-or-complex scalar field (in practice R\mathbb RR or C\mathbb CC), and let XXX be a K\mathbb KK-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 K×X→X\mathbb K\times X\to XK×X→X jointly continuous, and Hausdorff. Assume XXX is Fréchet and XXX is not finite-dimensional over K\mathbb KK. 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).

Then the weak dual of XXX (continuous K\mathbb KK-linear functionals on XXX with the topology of pointwise convergence) is not net-complete. Net-complete (the bundle's definition): for every index type III (in the same universe as the space) carrying a partial order in which any two elements have a common upper bound, every family (vi)i∈I(v_i)_{i\in I}(vi​)i∈I​ that is Cauchy (for every neighbourhood NNN of 000 there is i0i_0i0​ with vi−vj∈Nv_i-v_j\in Nvi​−vj​∈N for all i,j≥i0i,j\ge i_0i,j≥i0​) has a point xxx with vi−x∈Nv_i-x\in Nvi​−x∈N for all i≥i\gei≥ some i0i_0i0​, for every neighbourhood NNN of 000. 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

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me