Alphabeta Math
Pipeline-generated
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

✓ 12 results · all verified · 8 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 4 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

The Baire Principles of Functional Analysis

1 · Prerequisites

2 · Summary

The Baire theorem turns pointwise information into uniform bounds, then supplies the open-mapping and closed-graph principles. Completeness of the domain and the precise closure-to-image lifting step are kept explicit.

3 · Logical flowchart

4 · Definitions, theorems and proofs

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-07Open item page →

Uniform boundedness principle

Statement

Assume DC. Let X be a Banach space, Y a normed space, and let F be a family of bounded linear operators X→Y (A bounded linear operator between normed spaces). If sup⁡T∈F∥Tx∥<∞ for every x∈X, then sup⁡T∈F∥T∥<∞, where the norm is The operator norm as the least bound and as the unit-sphere or unit-ball supremum.

Facts & Assumptions

Given: DC, X,Y,F as in the statement, and pointwise boundedness.

Proof

technique · direct
1.1given

Put En={x:sup⁡T∈F∥Tx∥≤n}. Each En is closed (an intersection of inverse images of closed balls), and pointwise boundedness gives X=⋃n≥1En.

3.1step 2.1

For ∥h∥<r, both x0 and x0+h lie in that ball, so ∥Th∥≤∥T(x0+h)∥+∥Tx0∥≤2N for every T.

4.1step 3.1algebra∎

Rescaling a nonzero x to h=rx/(2∥x∥) yields ∥Tx∥≤4N∥x∥/r; the same is clear for x=0. Thus ∥T∥≤4N/r for every T.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-07Open item page →

Baire dichotomy for a pointwise-defined family of bounded linear operators

Statement

Assume DC. Let X be Banach, Y normed, and F⊆B(X,Y) (A bounded linear operator between normed spaces). Either sup⁡T∈F∥T∥<∞ (The operator norm as the least bound and as the unit-sphere or unit-ball supremum), or

S:={x∈X:sup⁡T∈F∥Tx∥=∞}

is a dense Gδ subset of X.

Facts & Assumptions

Given: DC and X,Y,F as in the statement.

Proof

technique · direct
1.1given

Let En={x:sup⁡T∥Tx∥≤n}. These sets are closed, and X∖S=⋃nEn.

2.1step 1.1

If some En has nonempty interior, the translation-and-rescaling argument of Uniform boundedness principle gives a common operator-norm bound.

2.2step 1.1

Otherwise every En is closed with empty interior. Its complement is open dense, so S=⋂n(X∖En) is Gδ and dense by Under Dependent Choice, a nonempty complete metric space is not a countable union of closed sets with empty interior.

3.1step 2.1step 2.2∎

The two alternatives exhaust the cases from step 2.1, proving the dichotomy.

CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-09-07Open item page →

A pointwise limit of bounded operators is bounded with the liminf norm bound

Statement

Assume DC. Let X be Banach, Y normed, and Tn:X→Y bounded linear (A bounded linear operator between normed spaces). If Tnx→Tx in Y for every x∈X, then T is bounded linear and

∥T∥≤lim inf⁡n→∞∥Tn∥,

with the operator norm of The operator norm as the least bound and as the unit-sphere or unit-ball supremum.

Facts & Assumptions

Given: DC and X,Y,(Tn),T with pointwise convergence as in the statement.

Proof

technique · direct
1.1given

Pointwise convergence makes (Tnx)n bounded for each x. Thus Uniform boundedness principle gives M:=sup⁡n∥Tn∥<∞.

2.1step 1.1

Passing Tn(x+y)=Tnx+Tny and Tn(λx)=λTnx to limits shows that T is linear.

2.2step 1.1

For each x, continuity of the norm gives ∥Tx∥=lim⁡n∥Tnx∥≤M∥x∥, so T is bounded.

3.1step 2.2∎

If lim inf⁡n∥Tn∥=∞, the asserted bound is immediate. Otherwise select a subsequence whose norms tend to the finite liminf. The preceding inequality along that subsequence gives ∥Tx∥≤(lim inf⁡n∥Tn∥)∥x∥ for every x, hence the asserted norm bound.

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-07Open item page →

A nonzero bounded linear operator is large on one of two nearby points

Statement

Let T:X→Y be nonzero and bounded (A bounded linear operator between normed spaces), let x∈X, and let r>0. There is a y∈B(x,r) such that

∥Ty∥>2r3∥T∥,

where ∥T∥ is The operator norm as the least bound and as the unit-sphere or unit-ball supremum.

Facts & Assumptions

Given: A nonzero bounded linear operator T, x∈X, and r>0.

Proof

technique · direct
1.1givenchoose

The unit-ball definition of the operator norm supplies z with ∥z∥≤1 and ∥Tz∥>8∥T∥/9.

2.1step 1.1algebra

Put w=(3r/4)z. Then both x+w and x−w lie in B(x,r), and ∥Tw∥>2r∥T∥/3.

3.1step 2.1algebra

The triangle inequality applied to T(x+w)−T(x−w)=2Tw gives max⁡{∥T(x+w)∥,∥T(x−w)∥}≥∥Tw∥>2r3∥T∥.

4.1step 2.1step 3.1∎

Choosing the corresponding one of x+w,x−w proves the claim.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-07Open item page →

Sokal's gliding-hump proof of uniform boundedness

Statement

Assume ACω and DC. If X is Banach, Y is normed, and a family F of bounded linear maps X→Y is pointwise bounded, then sup⁡T∈F∥T∥<∞.

Facts & Assumptions

Given: The stated choice principles, X,Y,F, and pointwise boundedness.

Proof

technique · constructive
1.1givenconstruct

Suppose the norms are unbounded. Countable choice selects Tn∈F with ∥Tn∥≥4n for n≥1. Set x0=0.

2.1step 1.1construct

Recursively, apply A nonzero bounded linear operator is large on one of two nearby points with centre xn−1 and radius 3−n to choose xn with ∥xn−xn−1∥<3−n and ∥Tnxn∥>(2/3)3−n∥Tn∥. DC licenses these dependent choices.

3.1step 2.1

The sequence (xn) is Cauchy, since its tails are bounded by a tail of ∑n≥13−n; completeness gives xn→x∈X. Moreover ∥x−xn∥≤∑k>n3−k=3−n/2.

4.1step 1.1step 2.1step 3.1algebradischarge-construct∎

Hence ∥Tnx∥≥∥Tnxn∥−∥Tn∥ ∥x−xn∥>16 3−n∥Tn∥≥16(4/3)n, which contradicts pointwise boundedness at x.

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passverified 2026-09-26 (gpt-6-sol)Open item page →

The closure of a bounded image contains a ball

Statement

Assume DC. If T:X→Y is a surjective bounded linear map between Banach spaces, then for some r>0,

BY(0,r)⊆T(BX(0,1))‾.

Facts & Assumptions

Given: DC and a surjective bounded linear map T:X→Y with X,Y Banach.

[F1]

Dependent Choice is the stated countable-selection premise for the Baire category theorem used below (The axiom of dependent choice: a relation in which every element is related to something admits an N-indexed chain).

Proof

technique · direct
1.1givenF1

Surjectivity gives Y=⋃n≥1T(BX(0,n))‾. Baire applied to Y under the stated DC premise gives n, y0, and ρ>0 with B(y0,ρ) inside this closure.

2.1step 1.1algebra

Subtracting two points in this ball shows B(0,ρ)⊆T(B(0,2n))‾.

3.1step 2.1algebra∎

Scaling by 2n gives B(0,ρ/(2n))⊆T(B(0,1))‾, as required.

LemmaStatement: Literature-sourcedProof: AI-adaptedverified 2026-09-26 (gpt-6-sol)Open item page →

Successive approximation turns a closure-ball inclusion into an actual preimage

Statement

Assume DC. Let T:X→Y be bounded linear, with X Banach. If BY(0,r)⊆T(BX(0,1))‾ for some r>0, then

BY(0,r/2)⊆T(BX(0,1)).

Facts & Assumptions

Given: DC and T,X,Y,r with the displayed closure inclusion.

[F1]

Dependent Choice licenses a sequence of witnesses when each next choice depends on the current residual (The axiom of dependent choice: a relation in which every element is related to something admits an N-indexed chain).

Proof

technique · constructive
1.1givenF1construct

Given y with ∥y∥<r/2, choose a real θ with ∥y∥/r<θ<1/2. Repeatedly use the closure inclusion after scaling to choose xn with ∥xn∥<θ2−n and residual y−T∑k≤nxk of norm <rθ2−n−1. The initial residual has norm below rθ; each later residual lies in the ball to which the next scaled closure inclusion applies. [F1] licenses this dependent recursive selection.

2.1step 1.1

The series ∑nxn converges in X by Series criterion for Banach spaces, and its sum x has ∥x∥≤∑n∥xn∥≤2θ<1.

3.1step 1.1step 2.1discharge-construct∎

Boundedness makes T continuous by For a linear operator, boundedness, continuity at 0, continuity, and Lipschitz continuity are equivalent, so Tx=lim⁡nT∑k≤nxk=y as the residuals vanish.

TheoremStatement: Literature-sourcedProof: AI-adaptedverified 2026-09-26 (gpt-6-sol)Open item page →

Open mapping theorem

Statement

Assume DC. A surjective bounded linear map T:X→Y between Banach spaces is open: it maps every open subset of X to an open subset of Y.

Facts & Assumptions

Given: DC and a surjective bounded linear map T:X→Y between Banach spaces.

[A1]

The stated Dependent Choice is the direct premise for the two open-mapping lemmas (The axiom of dependent choice: a relation in which every element is related to something admits an N-indexed chain).

Proof

technique · direct
1.1givenA1

Under [A1], The closure of a bounded image contains a ball gives some r>0 with BY(0,r)⊆T(BX(0,1))‾. The successive-approximation lemma Successive approximation turns a closure-ball inclusion into an actual preimage then gives BY(0,r/2)⊆T(BX(0,1)). Put ε=r/2>0.

2.1step 1.1algebra

For every x∈X and a>0, linearity gives BY(Tx,aε)⊆T(BX(x,a)).

3.1step 2.1∎

Let U⊆X be open and y=Tx∈T(U). Choose a>0 with BX(x,a)⊆U. Then step 2.1 gives BY(y,aε)⊆T(U). Thus every point of T(U) is interior, so T(U) is open.

CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passverified 2026-09-26 (gpt-6-sol)Open item page →

Quantitative lifting form of the open mapping theorem

Statement

Assume DC. For a surjective bounded linear T:X→Y between Banach spaces, some c>0 satisfies cBY(0,1)⊆T(BX(0,1)).

Facts & Assumptions

Given: DC and T as in the statement.

[A1]

Proof

technique · direct
1.1givenA1

Under [A1], Open mapping theorem makes T(BX(0,1)) an open neighbourhood of 0.

2.1step 1.1∎

It therefore contains BY(0,c) for some c>0, which is exactly the claim.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passverified 2026-09-26 (gpt-6-sol)Open item page →

Bounded inverse theorem

Statement

Assume DC. A bounded bijective linear map T:X→Y between Banach spaces has a bounded linear inverse T−1:Y→X.

Facts & Assumptions

Given: DC and a bounded bijective linear T:X→Y between Banach spaces.

[A1]

Proof

technique · direct
1.1givenA1

Under [A1], Open mapping theorem makes T(BX(0,1)) an open neighbourhood of 0; hence BY(0,c)⊆T(BX(0,1)) for some c>0.

2.1step 1.1algebra

If y≠0, the point cy/(2∥y∥) lies in BY(0,c), so its unique preimage has norm <1. Scaling gives ∥T−1y∥<2c−1∥y∥; this also holds at 0.

3.1step 2.1∎

Thus T−1 is bounded, and it is linear because T is a linear bijection.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-09-07Open item page →

The graph of a linear operator with a linear domain

Definition

For normed spaces X,Y, a linear subspace D⊆X (Linear subspace of a vector space) and a linear map A:D→Y, its graph is G(A)={(x,Ax):x∈D}⊆X×Y. Equip X×Y with the maximum product norm ∥(x,y)∥max⁡=max⁡{∥x∥,∥y∥} from The standard product norms on a finite product of normed spaces. The operator is closed when G(A) is closed in this norm.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-07Open item page →

Closed graph theorem

Statement

Assume DC. For Banach spaces X,Y and an everywhere-defined linear T:X→Y, T is bounded if and only if its graph (The graph of a linear operator with a linear domain) is closed.

Facts & Assumptions

Given: DC, Banach spaces X,Y, and an everywhere-defined linear map T.

Proof

technique · direct
1.1given

If T is bounded, xn→x and Txn→y, continuity gives y=Tx, so the graph is closed.

1.2given

Conversely, a closed graph is Banach by A closed subspace of a Banach space is Banach, since X×Y is Banach by Finite products of Banach spaces are Banach.

2.1step 1.2∎

The first projection G(T)→X is a bounded linear bijection; its inverse is bounded by Bounded inverse theorem. Composing that inverse with the second projection makes T bounded.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-09-07Open item page →

A closable densely defined linear operator

Definition

Let X and Y be normed spaces, and let A:D(A)⊆X→Y be linear with dense linear domain. It is closable when the closure of its graph (The graph of a linear operator with a linear domain) in X×Y (Interior, closure, boundary, limit point, isolated point and dense subset of a metric space) is itself the graph of a linear operator. That operator is the closure A‾.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-07Open item page →

Sequential criterion for closability

Statement

Assume DC. A densely defined linear A:D(A)⊆X→Y is closable if and only if every sequence xn∈D(A) with xn→0 and Axn→y has y=0.

Facts & Assumptions

Given: DC and A as in the statement.

Proof

technique · direct
1.1given

If the graph closure is a graph and (0,y) lies in it, it must equal the graph point (0,0); this proves the sequential condition.

1.2givenconstruct

Conversely, if (x,y) and (x,z) lie in the graph closure, sequences of graph points converging to them exist by metric closure (using DC to choose 1/(n+1) approximants). Their differences give a sequence tending to (0,y−z).

2.1step 1.2∎

The sequential condition gives y−z=0, so the graph closure has at most one second coordinate over each first coordinate; as a closed linear subspace it is a graph.

CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-07Open item page →

A separately continuous bilinear map on Banach spaces is jointly continuous

Statement

Assume DC. If X,Y are Banach, Z normed, and b:X×Y→Z is bilinear and separately continuous, then b is jointly continuous.

Facts & Assumptions

Given: DC, Banach X,Y, normed Z, and separately continuous bilinear b.

Proof

technique · direct
1.1given

For each y in the unit ball of Y, x↦b(x,y) is bounded; for fixed x, separate continuity makes their values at x bounded on that unit ball.

2.1step 1.1

Uniform boundedness Uniform boundedness principle gives C with ∥b(x,y)∥≤C∥x∥∥y∥.

3.1step 2.1∎

Thus b is bounded in the sense of A bounded bilinear map between normed spaces, and the boundedness/joint-continuity equivalence For a bilinear map, boundedness is equivalent to joint continuity yields joint continuity.

CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-07Open item page →

A one-sided comparison of two complete norms makes them equivalent

Statement

Assume DC. Let p,q be complete norms on one vector space V. If q(v)≤Cp(v) for all v and some C>0, then p and q are equivalent norms (Equivalent norms, and the dictionary with equivalent metrics).

Facts & Assumptions

Given: DC, complete norms p,q on V, and q≤Cp.

Proof

technique · direct
1.1given

The identity I:(V,p)→(V,q) is a bounded linear bijection by the assumed inequality.

2.1step 1.1

Both spaces are Banach (Banach space), so Bounded inverse theorem makes I−1 bounded: p(v)≤C′q(v) for some C′>0.

3.1step 2.1∎

The two inequalities are precisely equivalence of p and q.

5 · Examples, counterexamples and false statements

None yet.

Sources