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.
Basic weak star neighborhoods
Statement
For a real or complex normed space , the sets
form a weak-star neighborhood base at . The empty list gives . This topology is Hausdorff and locally convex, and addition and joint scalar multiplication are continuous, without HB or any choice assumption.
Facts & Assumptions
The weak-star topology is the initial topology of evaluations, with the displayed finite-evaluation basis (The weak-star topology from finite evaluations).
Proof
Given: a real or complex normed space .
Each displayed set is a finite intersection of inverse scalar disks. Conversely, every finite intersection of subbasic sets containing contains such a set by shrinking each scalar open set to a disk and taking the smallest of the finitely many positive radii. The empty intersection needs no shrinking.
For a finite list set , with for an empty list. Linearity gives and . Hence its open balls are balanced and real-convex; the bounds imply , proving addition is continuous.
To control scalar multiplication at , use . The requirements and make this less than . Thus the topology is a locally convex vector topology.
If as functions, some has . Put . The evaluation disks of radius about these two values have disjoint inverse images containing and , since a common member would give . This proves Hausdorffness; on a singleton dual it is vacuous. No norming principle is involved.
Depends on
Used by
Dependency tree · two levels
3 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 (2017); exact harvest in batch coverage (standard reference, not scraped)
- Teschl, Topics in Real and Functional Analysis (2017); exact harvest in batch coverage (standard reference, not scraped)