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.
Under choice, weight , density , local character , and character as raw cardinal minima and a supremum
Definition
Assume the Axiom of Choice (The Axiom of Choice) and let be a topological space. The weight is the least cardinality of a basis for , and the density is the least cardinality of a dense subset of (Basis and subbasis for a topology, and the topology generated by a family of sets, Dense, nowhere dense and codense subsets of a topological space, and the criterion by basic open sets, Cardinal (initial ordinal) and cardinality).
For , the local character is the least cardinality of a neighbourhood base at (Neighbourhood of a point and neighbourhood base, with this library's convention that a neighbourhood need not be open). The character is the raw cardinal supremum
No normalization is imposed. In particular a one-member local base has cardinality , not . The forward lemmas named in justified_by establish the asserted minima and supremum.
Depends on
- Basis and subbasis for a topology, and the topology generated by a family of sets
- Dense, nowhere dense and codense subsets of a topological space, and the criterion by basic open sets
- Neighbourhood of a point and neighbourhood base, with this library's convention that a neighbourhood need not be open
- Cardinal (initial ordinal) and cardinality
- Cardinal sum $\kappa \oplus \lambda$, product $\kappa \otimes \lambda$ and exponentiation $\kappa^{\lambda}$, and why they are written apart from the ordinal operations
- The Axiom of Choice
Used by
- For the lower-limit line, χ=d=L=c=ℵ₀ and w=2^ℵ₀ under choice Example
- Under choice, for an infinite discrete space of cardinality κ, w=d=L=c=κ while χ=1 Example
- Under choice, for the usual real line, w=d=χ=L=c=ℵ₀ under the raw convention Example
- Under choice, d(X) is a well-defined cardinal Lemma
- Under choice, w(X) is a well-defined cardinal Lemma
- Under choice, χ(x,X) and χ(X) are well-defined cardinals Lemma
- Under choice, a continuous surjection does not increase density or Lindelöf degree Proposition
- Under choice, for Y⊆ X, w(Y)≤ w(X) and χ(y,Y)≤χ(y,X) Proposition
- Under choice, c(X)≤ d(X)≤ w(X) and χ(X),L(X)≤ w(X) Theorem
- Weight and character of the Kojman-Shelah scale subspace Theorem
Dependency tree · two levels
27 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
- D. H. Fremlin, Measure Theory, Chapter 5A (standard reference, not scraped)
- Cardinal function (Wikipedia) (standard reference, not scraped)