Alphabeta MathHow 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.
Dual unit ball has extreme points
Statement
Assume the Axiom of Choice. The closed unit ball of the dual of every nonzero real or complex normed space has an extreme point.
Facts & Assumptions
Given: AC and a nonzero real or complex normed space .
Under the ultrafilter lemma the closed dual unit ball is weak-star compact (Banach–Alaoglu).
Under AC every nonempty compact convex subset of a locally convex Hausdorff real or complex TVS has an extreme point (Krein–Milman existence of extreme points).
The weak-star topology on is Hausdorff and locally convex without any choice assumption (Basic weak star neighborhoods).
AC is the declared ambient choice principle (The Axiom of Choice).
AC implies the ultrafilter lemma (The ultrafilter lemma, from the Axiom of Choice: every filter extends to an ultrafilter).
AC supplies the Hahn–Banach theorem used inside locally convex separation in the selected Krein–Milman proof (Hahn-Banach dominated extension theorem for real vector spaces).
Proof
By [F5], the assumed AC supplies the ultrafilter lemma. Therefore [F1] makes compact for the weak-star topology.
By [F3], with the weak-star topology is a locally convex Hausdorff real or complex TVS. The set is nonempty because it contains the zero functional, and it is convex by the triangle inequality and homogeneity of the dual norm.
Apply [F2] to the nonempty weak-star compact convex set . Its proof uses Zorn under AC and separation under HB; [F6] records that the same AC hypothesis supplies that HB input. Hence has an extreme point.
This proves the stated nonzero case. In fact the same argument includes , whose dual ball is the singleton and whose unique point is extreme.
Depends on
Used by
Dependency tree · two levels
25 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)