CorollaryStatement: AI-adaptedProof: 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.

A separable predual has weak-star sequentially compact dual ball

Statement

Assume the ultrafilter lemma. If $X$ is a separable real or complex normed space, then every sequence in $B_{X^{*}}$ has a subsequence converging in the weak-star topology. Completeness of $X$ is not required.

Facts & Assumptions

Given: The ultrafilter lemma and a separable real or complex normed space $X$ .

[F1]

A separable space has an at most countable dense subset (Separability: the existence of an at most countable dense subset).

[F2]

A fixed dense sequence metrizes the weak-star topology on every norm-bounded subset of the dual (Dual ball weak-star metrizable for a separable predual).

[F3]

Under the ultrafilter lemma, $B_{X^{*}}$ is weak-star compact, without completeness of $X$ (Banach–Alaoglu).

[F4]

Every compact metric space is countably compact (In any metric space compactness implies countable compactness and limit point compactness, and each of countable compactness and limit point compactness implies sequential compactness; every implication here is proved without a choice principle).

[F5]

Every countably compact metric space is sequentially compact, and this implication uses no choice principle (In any metric space compactness implies countable compactness and limit point compactness, and each of countable compactness and limit point compactness implies sequential compactness; every implication here is proved without a choice principle).

Proof

technique · direct

1.1

Fix an at most countable dense set $D \subseteq X$ . It is nonempty because $0 \in X$ and the empty set is not dense in a nonempty space. If $D$ is countably infinite, a witnessing bijection $N \to D$ is a dense sequence. If $D$ is finite, a witnessing finite list can be repeated periodically (and its first entry repeated after the list ends) to give a sequence with range $D$ . Thus $X$ has a fixed dense sequence; no countable family of choices was made.

F1given

1.2

The same ball is weak-star compact by Banach–Alaoglu; the ultrafilter lemma is used at this step through [F3].

2.1

Applying [F2] to the norm-bounded set $B_{X^{*}}$ gives a metric inducing precisely its relative weak-star topology.

F2step 1.1

3.1

By steps 2.1 and 1.2 the ball is a compact metric space, hence countably compact by [F4] and sequentially compact by [F5]. Equivalently, every sequence in it has a weak-star convergent subsequence.

F4F5step 2.1step 1.2∎

Depends on

Used by

Banach–Alaoglu versus sequential Alaoglu Remark

Dependency tree · two levels

36 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Bühler–Salamon, Functional Analysis (standard reference, not scraped)
Gerald Teschl, Topics in Real and Functional Analysis (standard reference, not scraped)