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.
Under choice, and
Statement
Assuming choice, and .
Facts & Assumptions
Given: A topological space , the Axiom of Choice, a basis of cardinality , and a dense subset of cardinality .
The raw definitions make and the least cardinalities of a basis and a dense subset, make the supremum of the local characters, make the least cardinal bounding subcovers, and make the supremum of sizes of pairwise-disjoint nonempty open families (Under choice, weight , density , local character , and character as raw cardinal minima and a supremum, Under choice, Lindelöf degree and cellularity as raw cardinal functions).
The Axiom of Choice chooses one member from each nonempty set in a family (The Axiom of Choice).
Proof
Choose one point from each nonempty ; the chosen set meets every nonempty open set because is a basis, so it is dense and has cardinality at most .
For each , the subfamily is a local base at and has cardinality at most , so every local character, and therefore its supremum , is at most .
Given an open cover, choose for each that lies in a cover member one such member; these at most chosen sets still cover , so .
For a pairwise-disjoint family of nonempty open sets, choose a point of for each ; disjointness makes this assignment injective into , so and .
Steps 1.1, 1.2, 1.3 and 1.4 give and .
Depends on
- Under choice, weight $w(X)$, density $d(X)$, local character $\chi(x,X)$, and character $\chi(X)$ as raw cardinal minima and a supremum
- Under choice, Lindelöf degree $L(X)$ and cellularity $c(X)$ as raw cardinal functions
- Under choice, $w(X)$ is a well-defined cardinal
- Under choice, $d(X)$ is a well-defined cardinal
- Under choice, $\chi(x,X)$ and $\chi(X)$ are well-defined cardinals
- Under choice, $L(X)$ is a well-defined cardinal
- Under choice, $c(X)$ is a well-defined cardinal
- The Axiom of Choice
Used by
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 57 results over 14 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.
Sources
- D. H. Fremlin, Measure Theory, Chapter 5A (standard reference, not scraped)