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.
For the lower-limit line, and under choice
Example
Assume Choice and let be the lower-limit line. At , the intervals form a countable local base. No finite family is a local base: the intersection of finitely many neighbourhoods is still a neighbourhood and contains some , whereas cannot contain any member of a finite local base contained in that intersection. Hence .
The rationals are countable and meet every nonempty half-open interval, so ; no finite set is dense, since a short half-open interval can avoid it. The published lower-limit-line lemma gives Lindelöfness, while the cover has no finite subcover, so . Density bounds cellularity above, and the disjoint family bounds it below, giving .
All half-open intervals form a basis of cardinality at most . Conversely, well order any basis and assign to each its first member with ; if , then cannot contain , so . Thus .
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, $c(X)\le d(X)\le w(X)$ and $\chi(X),L(X)\le w(X)$
- The lower-limit line has a clopen basis, is regular, and is Lindelöf under countable choice
- Intervals of $\mathbb{R}$: the nine order-convex forms, nondegeneracy, and length
- A family is a basis for a unique topology iff it covers the set and every point of an intersection of two members lies in a member inside that intersection; finite intersections of any subbasis form a basis
- $\mathbb{Q}$ is countably infinite
- The rationals embed densely in the reals
- $\mathbb{R}$ is uncountable (Cantor's nested intervals, 1874)
- $\mathbb{R} \approx \mathcal{P}(\mathbb{N})$ in ZF, by the Cantor set for one injection and by the cuts $\{q \in \mathbb{Q} : q < x\}$ for the other; so $\lvert \mathbb{R} \rvert = 2^{\aleph_0}$ under the Axiom of Choice
- Absorption: for cardinals $\kappa, \lambda$ with $\kappa$ infinite and $\lambda \le \kappa$, $\kappa \oplus \lambda = \kappa$, and $\kappa \otimes \lambda = \kappa$ when $\lambda \ne 0$
- The Axiom of Choice
Used by
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 190 results over 32 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
- UCR General Topology Notes (standard reference, not scraped)
- Lower limit topology (Wikipedia) (standard reference, not scraped)
- D. H. Fremlin, Measure Theory, Chapter 5A (standard reference, not scraped)