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.
Dense domains and directed unions of specializing conditions
Statement
For an Aronszajn tree and each , the set is dense: every has some in . If a nonempty downward-directed family meets every , then is a total specializing function . Downward directed means that for every there is with . These assertions require no choice axiom and assert no existence of such a .
Facts & Assumptions
Given: , , and as above. In the union assertion, a family with the stated properties is supplied.
Conditions are finite partial maps separating comparable distinct nodes, with stronger conditions extending weaker ones. Finite specializing conditions
A natural-valued map separating comparable distinct nodes specializes the tree. Aronszajn, Suslin and special trees
Proof
Fix and . If take . Otherwise choose the explicit natural when and when the finite range is nonempty. Put . It is a finite function extending , and differs from every old label. Pairs in the old domain satisfy F1 already; any new comparable pair involves and has unequal labels. Thus and , proving density.
Put as a union of graphs. If , take containing the respective pairs. Directedness gives extending both; as is a function, . Thus is a function with domain contained in and values in . For each , meeting supplies a condition in with in its domain, so . Hence . No simultaneous selection of the conditions is needed for this pointwise conclusion.
If , totality gives whose domains contain respectively. A common stronger contains both nodes, so F1 gives . Since by its membership in , these are and . Therefore specializes by F2. This uses only the supplied directed family; density alone does not provide that family.
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
7 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.