Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-14
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.

Countable compactness closes in the bidual

Statement

Assume the ultrafilter lemma, the Axiom of Dependent Choice (DC), and HB. Let X be a real or complex Banach space and let A⊆X be relatively weakly countably compact: every sequence in A has a weak cluster point in X. Then A is norm bounded and

JX(A)‾ w∗⊆JX(X)⊆X∗∗.

Here the closure uses σ(X∗∗,X∗). The conclusion does not assert that the cluster point or the representing point belongs to A.

Facts & Assumptions

Given: the three stated principles, X, and A as in the statement.

[F1]

Relative weak countable compactness means that every sequence in the set has a cluster point in the ambient weak space, with "cluster" requiring every neighborhood to contain arbitrarily late terms (Relative weak compactness and three sequential notions).

[F2]

The weak and weak-star topologies are the initial topologies of their evaluation maps; basic weak-star neighborhoods impose only finitely many evaluation inequalities (Weak topology on a normed space, The weak-star topology from finite evaluations, Basic weak star neighborhoods).

[F3]

Assuming the ultrafilter lemma, the dual unit ball is weak-star compact (Banach–Alaoglu), and arbitrary products of compact Hausdorff spaces are compact (Assuming the ultrafilter lemma, an arbitrary product of compact Hausdorff spaces is compact).

[F4]

Under HB the canonical map JX:X→X∗∗ is an isometry, for both scalar fields (Relative Hahn–Banach makes the canonical bidual map an isometry). HB is the named relative dominated-extension principle (The real dominated-extension principle as an additional hypothesis over ZF).

[F5]

Assuming DC, a pointwise bounded family of bounded operators on a Banach space is uniformly norm bounded (Uniform boundedness principle). If the target is Banach, the bounded-operator space is Banach (If (Y) is Banach then (\mathcal B(X,Y)) is Banach).

[F6]

DC supplies a sequence following any entire relation from a specified initial state (The axiom of dependent choice: a relation in which every element is related to something admits an N-indexed chain).

[F10]

On the scalar field put ρ(s,t)=min⁡{1,∣s−t∣}. This bounded metric induces the usual scalar topology, since its balls of radius less than 1 are the usual balls. It is complete: a ρ-Cauchy sequence is Cauchy for the usual metric by testing tolerances below 1, and its usual scalar limit is also its ρ-limit. The standard weighted metric on a countable product of complete metrics bounded by 1 therefore applies to copies of (K,ρ) and induces the product topology; metric spaces are Hausdorff (The standard weighted metric on a countable product of bounded complete metric spaces is complete, The reals are complete, The complex plane is complete, and convergence is equivalent to convergence of real and imaginary parts, Distinct points of a metric space have disjoint balls around them, The product set ∏i∈IXi of functions choosing a point in each factor, the projections, the box topology, and the product topology as the initial topology of the projections; the empty product is a one-point space).

[F12]

A nonempty at-most-countable set can be enumerated by a sequence, finite Cartesian products of countable sets are countable, the natural numbers are cofinal in the reals, and 1/n is eventually smaller than every positive real (A nonempty set is at most countable iff it is a surjective image of N, A product of two at most countable sets is at most countable, Every complete ordered field is Archimedean, For every ε>0 in a complete ordered field there is a natural n≥1 with 1/n<ε).

Proof

technique · the Grothendieck pointwise-compactness argument, with each countable selection implemented by DC
1.1given

If A=∅, it is norm bounded and JX(A)=∅ has empty weak-star closure, so both conclusions hold. Hence assume A≠∅.

1.2F2F3F4

Put K=BX∗ with its weak-star topology and define Φ:X→KK by Φ(x)(u)=u(x). Each Φ(x) is continuous on K by [F2], so Φ(X)⊆C(K). The space K is compact by [F3] and Hausdorff because distinct members of X∗ differ at some x∈X, whose evaluation separates them in the Hausdorff scalar field. By [F4], ∥Φ(x)∥∞=∥x∥ and Φ is injective. Since every u∈X∗ is zero or a scalar multiple of a member of K, [F2] shows that the pointwise topology on Φ(X) is exactly the weak topology transported from X.

1.3F1F2F6F12

For each u∈X∗ the scalar set u(A) is bounded. Otherwise every set En={a∈A:∣u(a)∣>n}, n≥1, is nonempty. Apply DC to finite valid histories, starting with the empty history and extending the nth stage by an element of En+1; this gives (an) with ∣u(an)∣>n+1. Let a be a weak cluster. The weak neighborhood ∣u(x−a)∣<1 contains arbitrarily late an, while [F12] lets us take such an n with n+1>∣u(a)∣+1. Then ∣u(an)∣≤∣u(a)∣+1<n+1, a contradiction.

1.4F8

We shall repeatedly use this choice-free consequence of compactness. If (zn) is a sequence in a compact space, then the closed sets CN={zn:n≥N}‾ are nonempty, nested, and have the finite-intersection property. By [F8] some z lies in every CN; by the closure characterization, every neighborhood of z contains terms with arbitrarily large indices. Thus z is a cluster point of the sequence.

2.1F1step 1.2

Every sequence in M:=Φ(A) has a pointwise cluster in Φ(X). Indeed, injectivity gives its unique lift (an) in A; [F1] gives a weak cluster a∈X, and the topology identification in step 1.2 makes Φ(a) a pointwise cluster.

2.2F5step 1.3

The dual X∗=B(X,K) is Banach: the real and complex scalar fields are Banach and [F5] applies to the bounded-operator space. The family {JX(a):a∈A}⊆B(X∗,K) is pointwise bounded by step 1.3, so UBP under the assumed DC gives R:=sup⁡a∈A∥JX(a)∥<∞.

3.1F4step 1.2step 2.2

The HB isometry [F4] gives ∥a∥=∥JX(a)∥≤R for every a∈A. Thus A, and equivalently M in the supremum norm, is norm bounded.

4.1F3F8F9step 3.1

Let B=M‾ p be the closure in the full product KK. For each t∈K, step 3.1 gives ∣h(t)∣≤R for h∈M. The scalar disk DR={z:∣z∣≤R} is compact Hausdorff by [F9], including R=0; hence DRK is compact by [F3]. It is closed in KK, so B⊆DRK, and B is closed in that product. Therefore B is compact by [F8].

5.1F10step 4.1assume-contra

We prove B⊆C(K). Suppose instead that g∈B is discontinuous at y∈K. Then for some ε>0, every neighborhood of y meets Z={z∈K:∣g(z)−g(y)∣≥ε}. This is exactly the negation of continuity at y into the metric scalar field, written with one failed positive tolerance. Notice y∉Z.

6.1F2F6F7step 5.1construct

Put U0=K and ηn=ε/(n+1) for n≥1. DC on finite valid histories constructs hn∈M, open neighborhoods Un of y, and xn∈K such that ∣hn(y)−g(y)∣<ηn/2 and ∣hn(xm)−g(xm)∣<ηn/2 for m<n, while y∈Un⊆Un‾⊆Un−1∩{z:∣hn(z)−hn(y)∣<ηn} and xn∈Un∩Z. At stage n, the approximation is possible because g is in the pointwise closure of M; the set to be shrunk is an open neighborhood of y because hn is continuous; [F7] supplies Un; and step 5.1 makes Un∩Z nonempty. Thus the relation extending a finite valid history is entire, exactly the hypothesis of DC.

7.1F8step 1.4step 2.1step 6.1

By step 2.1, (hn) has a pointwise cluster h=Φ(a)∈Φ(X). By step 1.4, (xn) has a cluster x∈K. The nesting in step 6.1 gives xm∈Un whenever m≥n, so the closure characterization gives x∈Un‾ for every n.

8.1F10F12step 6.1step 7.1

Hence ∣hn(x)−hn(y)∣<ηn and ∣hn(y)−g(y)∣<ηn/2. Since ηn→0 by [F12], hn(x)→g(y). But h is a pointwise cluster of (hn), so h(x) is a cluster of the convergent scalar sequence (hn(x)); scalar Hausdorffness forces h(x)=g(y).

9.1F10F12step 5.1step 6.1step 7.1step 8.1

For fixed m, step 6.1 gives hn(xm)→g(xm) as n→∞. The same cluster-and-uniqueness argument gives h(xm)=g(xm). Since xm∈Z, we therefore have ∣h(xm)−h(x)∣=∣g(xm)−g(y)∣≥ε for every m.

10.1F1F2step 1.2step 7.1step 9.1discharge-contradiction: step 5.1

The function h=Φ(a) is continuous on K. Thus {z:∣h(z)−h(x)∣<ε/2} is a neighborhood of the cluster x and must contain arbitrarily late xm, contradicting step 9.1. Therefore every g∈B is continuous and B⊆C(K).

11.1F2F3step 4.1step 10.1

Fix g∈B. For positive integers r,s and h∈M, define Vhr,s={(t1,…,tr)∈Kr:∣h(tj)−g(tj)∣<1/s for 1≤j≤r}. These sets are open because g,h∈C(K) by step 10.1, and they cover Kr because g lies in the pointwise closure of M. The finite power Kr is compact by [F3], so some nonempty finite list of members of M has the corresponding Vhr,s covering Kr.

12.1F6F12step 11.1

Pair the positive integer indices (r,s) using [F12]. Apply DC to finite histories of choices of the finite subcovers from step 11.1; the extension relation is entire. Thus obtain one finite list Fr,s⊆M for every pair. Their union M0 is at most countable: retain the finite-list order, pad each nonempty list by its first term, and enumerate the pairs of natural indices using [F12]. No member of an uncountable family has been selected.

13.1F8F12step 4.1step 12.1

The point g lies in the pointwise closure of M0: for finitely many points and tolerance δ>0, repeat points if needed to form a positive-length tuple and choose s with 1/s<δ; a member of Fr,s gives all the inequalities. Let P=M0‾ p. Then g∈P⊆B; P is closed in compact B, hence compact by [F8], and it is separable because the at-most-countable M0 is dense in it.

14.1F2F8step 1.4step 10.1step 13.1

We record the compact-cluster argument of Haase's Lemma E.1. Let (qn)⊆K, q∈K, and let (vj) be pointwise dense in P. If vj(qn)→vj(q) for every j, then v(qn)→v(q) for every v∈P. Indeed, let C be the intersection of the closures of all tails of (qn); it is nonempty by step 1.4. For z∈C, continuity and the assumed scalar convergence give vj(z)=vj(q) for every j. Pointwise density then gives v(z)=v(q) for every v∈P: otherwise the two-coordinate neighborhood of v at z,q with radius ∣v(z)−v(q)∣/3 would contain no vj. If v(qn) failed to converge to v(q), least-index recursion would give a subsequence staying some fixed positive distance away. Its closed tail closures have a common point z∈C by [F8], while continuity of v at z contradicts both v(z)=v(q) and that fixed separation.

14.2F10F12step 13.1

The compact separable pointwise space P is nonempty because it contains g. Enumerate a nonempty pointwise-dense subset as (vj) using [F12]. On the countable product of the bounded scalar metrics ρ use the standard weighted product metric D from [F10], and pull it back along q↦(vj(q))j to a continuous pseudometric d on K.

15.1F3F6F10F12step 14.2

For each positive integer n, the open d-balls of radius 1/n cover K, so compactness gives a nonempty finite list of centers. DC, applied to finite histories of such lists, chooses one list for each n. Pad every list by its first center and use the countable pairing in [F12] to enumerate the union as (qm). For each q∈K and each n, take the first center in the nth list whose ball contains q; the resulting sequence qmn satisfies d(qmn,q)<1/n, hence vj(qmn)→vj(q) for every j.

16.1F10step 14.1step 15.1

The evaluations at (qm) separate P. If v,w∈P agree at every qm, then for arbitrary q∈K use the sequence from step 15.1. Step 14.1 gives v(qmn)→v(q) and w(qmn)→w(q); equality term by term and scalar Hausdorffness give v(q)=w(q). Thus v=w.

17.1F2F10F11step 13.1step 16.1

The evaluation map E:P→KN, E(v)=(v(qm))m, is continuous for the pointwise and product topologies by [F2] and injective by step 16.1. Its corestriction to E(P) is a continuous bijection from compact P to a metric, hence Hausdorff, space. By [F11] it is a homeomorphism. Pulling back the restriction of the weighted metric built from ρ therefore metrizes the pointwise topology of P.

18.1F12step 13.1step 17.1

Enumerate M0 as (wk), with repetitions allowed. Since it is dense in the metric space P, for each n≥1 there is a k with dP(wk,g)<1/n; take the least such k. This defines, without choice, a sequence (wkn) in M0 converging to g pointwise.

19.1F1F2F10step 1.2step 18.1

Lift this sequence uniquely to (an) in A. By [F1] it has a weak cluster a∈X, so Φ(a) is a pointwise cluster of (wkn) by step 1.2. Every scalar coordinate of that sequence converges to the corresponding coordinate of g by step 18.1; uniqueness of scalar cluster points gives g=Φ(a). Since g∈B was arbitrary, B⊆Φ(X).

20.1F2step 1.2step 4.1step 19.1

Let x∗∗∈JX(A)‾ w∗ and restrict it to K: g(t)=x∗∗(t). Every finite pointwise neighborhood of g on K is the restriction of a basic weak-star neighborhood of x∗∗ in X∗∗, so it meets JX(A) by [F2]. Hence g∈B, and step 19.1 gives a∈X with g(t)=t(a) for every t∈K.

21.1F3F4F5F6step 1.1step 3.1step 20.1∎

For arbitrary u∈X∗, the equality is immediate if u=0; otherwise u/∥u∥∈K, and linearity gives x∗∗(u)=∥u∥g(u/∥u∥)=u(a)=JX(a)(u). Thus x∗∗=JX(a)∈JX(X). Together with step 3.1 and the empty case of step 1.1 this proves both assertions. The ultrafilter lemma is spent in steps 1.2, 4.1 and 11.1 through compactness; HB is spent only in the isometry in steps 1.2 and 3.1; DC is spent in UBP at step 2.2 and in the explicit finite-history constructions of steps 1.3, 6.1, 12.1 and 15.1.

Source notes

Haase's Lemma E.1 and Theorems E.2, E.3 and E.14, printed pp. 345–347 and 354–355, supply the complete compact-cluster, metrization, countable-reduction, and pointwise-closure arguments. The proof above changes Haase's phrase "take gx" to a cover indexed by every available function and uses DC only to choose countably many finite subcovers; this avoids an unrecorded choice over all tuples. It also supplies the dual-completeness premise needed by UBP and uses closed tail closures, rather than a metric compactness theorem, to obtain cluster points in the possibly nonmetrizable space K.

Depends on

Dependency tree · 2 levels

Sources