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, Lindelöf degree and cellularity as raw cardinal functions
Definition
Assume the Axiom of Choice (The Axiom of Choice). The Lindelöf degree is the least cardinal such that every open cover of has a subcover of cardinality at most . The cellularity is the cardinal supremum of the cardinalities of pairwise-disjoint families of nonempty open subsets of .
These are raw cardinal functions. Thus finite covers and finite cellular families retain their finite cardinalities. Their well-definedness is supplied by the forward lemmas named in justified_by.
Depends on
- Open cover, subcover, and compact topological space; a compact subset is a subspace that is compact in its own right
- Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison
- 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, c(X) is a well-defined cardinal Lemma
- Under choice, L(X) is a well-defined cardinal Lemma
- Under choice, a continuous surjection does not increase density or Lindelöf degree Proposition
- Under choice, c(X)≤ d(X)≤ w(X) and χ(X),L(X)≤ w(X) Theorem
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 74 results over 20 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)
- Cardinal function (Wikipedia) (standard reference, not scraped)