Remark 3.0.2 — Baire-category form of Banach–Steinhaus

Proved

GarrettFA.baire_banach_steinhaus

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

functional-analysistopological-vector-spaces

Let $X$ be a topological vector space and $Y$ a locally convex topological vector space over $\mathbb K=\mathbb R$ or $\mathbb C$ , and let $E$ be a set of continuous linear maps $X\to Y$ . Put

B_E=\{\,x\in X : E x \text{ is bounded in } Y\,\}.

If $B_E$ is not meagre (not a countable union of nowhere dense sets), then $B_E=X$ and $E$ is equicontinuous.

No completeness or metrizability of $X$ is assumed. Theorem 3.0.1 for Fréchet spaces follows, since Fréchet spaces are Baire spaces.

Preamble

import Definitions.Def_GarrettFA_IsEquicontinuousSet

Formal statement

namespace GarrettFA
theorem baire_banach_steinhaus {𝕜 : Type*} [RCLike 𝕜] {V : Type*} [AddCommGroup V] [Module 𝕜 V] [Module ℝ V]
    [IsScalarTower ℝ 𝕜 V] [TopologicalSpace V] [IsTopologicalAddGroup V] [ContinuousSMul 𝕜 V]
    [T2Space V]
    {Y : Type*} [AddCommGroup Y] [Module 𝕜 Y] [Module ℝ Y] [IsScalarTower ℝ 𝕜 Y]
    [TopologicalSpace Y] [IsTopologicalAddGroup Y] [ContinuousSMul 𝕜 Y] [LocallyConvexSpace ℝ Y]
    [T2Space Y]
    (E : Set (V →L[𝕜] Y))
    (hE : ¬ IsMeagre {x : V | Bornology.IsVonNBounded 𝕜 ((fun T : V →L[𝕜] Y => T x) '' E)}) :
    {x : V | Bornology.IsVonNBounded 𝕜 ((fun T : V →L[𝕜] Y => T x) '' E)} = Set.univ ∧
      IsEquicontinuousSet ((fun T : V →L[𝕜] Y => (T : V → Y)) '' E) := 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. 5, Remark 3.0.2

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$ ). 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 (no completeness, metrizability or local convexity is assumed for $V$ ). Let $Y$ 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 Y\to Y$ is jointly continuous, and which is Hausdorff, which is moreover locally convex as a real topological vector space. Let $E$ be a set of continuous $\mathbb K$ -linear maps $V\to Y$ , and put

G=\{x\in V : \{Tx : T\in E\}\text{ is bounded in } Y\}.

Assume $G$ is not meagre in $V$ (it is not contained in a countable union of closed sets with empty interior). Here bounded means von Neumann bounded over $\mathbb K$ : every neighbourhood of $0$ absorbs the set (for each neighbourhood $U$ of $0$ there is $r>0$ such that the set is contained in $cU$ for all scalars $c\in\mathbb K$ with $|c|\ge r$ ).

Then both: (a) $G=V$ , and (b) $E$ (as a set of functions $V\to Y$ ) is equicontinuous. Equicontinuous (the bundle's definition): for every neighbourhood $U$ of $0$ in the target there is a neighbourhood $N$ of $0$ in the source with $T(N)\subseteq U$ for every map $T$ in the family.

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