Prove2Me

Claim 5.0.6 — the weak dual embeds in the limit of the finite-dimensional spaces VΦ∗V^*_\Phi

Proved
GarrettFA.isEmbedding_weakDual_coeFn

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

functional-analysistopological-vector-spaces

Let VV be a Hausdorff locally convex topological vector space over K=R\mathbb K=\mathbb R or C\mathbb C. The map sending a continuous linear functional λ\lambda to its values (λ(v))v∈V(\lambda(v))_{v\in V},

Vσ∗⟶KV,V^*_\sigma \longrightarrow \mathbb K^V,

is a topological embedding, and its image consists of linear functionals.

Formalization Note In the notes, V∗V^* injects continuously into the projective limit lim⁡ΦVΦ∗\lim_\Phi V^*_\Phi over finite subsets Φ⊂V\Phi\subset V, where VΦ∗V^*_\Phi is the (finite-dimensional) Hausdorff completion of V∗V^* for the seminorm pΦ(λ)=∑v∈Φ∣λ(v)∣p_\Phi(\lambda)=\sum_{v\in\Phi}|\lambda(v)|, and the weak topology is the subspace topology. VΦ∗V^*_\Phi is identified with the image of V∗V^* in KΦ\mathbb K^\Phi, so the projective limit is a subspace of KV=lim⁡ΦKΦ\mathbb K^V=\lim_\Phi\mathbb K^\Phi, contained in the linear functionals. The formal statement is the embedding into KV\mathbb K^V with image among the linear functionals.

Preamble
import Mathlib
Formal statement
namespace GarrettFA
theorem isEmbedding_weakDual_coeFn {𝕜 : Type*} [RCLike 𝕜] {V : Type*} [AddCommGroup V] [Module 𝕜 V] [Module ℝ V]
    [IsScalarTower ℝ 𝕜 V] [TopologicalSpace V] [IsTopologicalAddGroup V] [ContinuousSMul 𝕜 V]
    [T2Space V]
    [LocallyConvexSpace ℝ V] :
    Topology.IsEmbedding (fun f : WeakDual 𝕜 V => (f : V → 𝕜)) ∧
      Set.range (fun f : WeakDual 𝕜 V => (f : V → 𝕜)) ⊆ {g : V → 𝕜 | IsLinearMap 𝕜 g} := 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, pp. 8–9, Claim 5.0.6
Read-back

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

Let K\mathbb K be a real-or-complex scalar field (in practice R\mathbb R or C\mathbb C), and let VV be a K\mathbb K-vector space that is also a real vector space with compatible scalar multiplications (multiplying by a real number rr is the same as multiplying by r∈Kr\in\mathbb K), carrying a topology in which addition and negation are continuous, scalar multiplication K×V→V\mathbb K\times V\to V is jointly continuous, and which is Hausdorff, which is moreover locally convex as a real topological vector space. Consider the map sending each element of the weak dual of VV (continuous K\mathbb K-linear functionals, with the topology of pointwise convergence) to the underlying function V→KV\to\mathbb K, the target KV\mathbb K^V carrying the product topology. The statement asserts both: (1) this map is a topological embedding (injective, and a homeomorphism onto its image with the subspace topology), and (2) every function in its image is K\mathbb K-linear.

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