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.
Borel hierarchy exhaustion and preservation by continuous pullback
Statement
In ZFC, for every topological space ,
Continuous inverse images preserve , and at every positive countable rank. If has the subspace topology, its and sets are exactly the traces of the corresponding classes on . No trace assertion for is made. The inverse-image proof uses no choice beyond the supplied representations.
Facts & Assumptions
The countable Borel hierarchy and its limit convention defines the positive ranks and the least Borel sigma-algebra.
Under countable choice, countable subsets of have countable suprema: Assuming countable choice: every at most countable subset of is bounded below , so no at most countable subset of is cofinal in it, and a supremum of at most countably many at most countable ordinals is at most countable.
Continuity of a map of topological spaces at a point and globally gives the open-neighbourhood criterion.
Transfinite induction permits induction over the positive countable ordinals.
Assume The Axiom of Choice, including its restriction to countable families.
Proof
Given: The indicated spaces, ranks and axiom assumptions.
By F5, every rank lies in : rank one consists of opens; the progressive step takes complements and countable unions of earlier Borel sets. Write for the union in the statement. If , then , the latter inclusion using a constant sequence. Thus is closed under complements.
Let be continuous. For open , every point of has an open neighbourhood inside that preimage by F3; their union proves it open. Induct on the rank by F5. For a represented union , , and the induction hypotheses place each preimage in its original lower rank. Also . These identities prove both classes at the next rank. Membership in both gives the assertion, without selecting any representations simultaneously.
Given , let be its least positive rank. The preceding complement argument applied twice gives . By F2 and A1, , and each . Hence . The empty union is . Thus is a sigma-algebra containing the opens and so contains by its leastness; step 1.1 gives equality.
For the inclusion , is open by F4, so is continuous and step 1.2 gives one trace inclusion. Conversely induct by F5. Opens lift by F4. If with lower- constituents, each has an ambient lift in its own rank by induction. Their sets of lifts are nonempty subsets of ; A1 chooses lifts . Then has trace . If is , lift to and use , whose trace is . This proves the reverse inclusion in both classes. For the same identities apply, with an available lift throughout. QED.
Depends on
- The countable Borel hierarchy and its limit convention
- Assuming countable choice: every at most countable subset of $\omega_1$ is bounded below $\omega_1$, so no at most countable subset of $\omega_1$ is cofinal in it, and a supremum of at most countably many at most countable ordinals is at most countable
- The Axiom of Choice
- Transfinite induction
- Continuity of a map of topological spaces at a point and globally
- Subspace topology: the traces of the open sets, its closed sets and its bases, the continuity of the inclusion, and the characteristic property of a map into a subspace
Used by
- Every set of reals is Borel False statement
- Borel payoffs admit unraveling covers Theorem
- Universal Borel sets and strictness on Cantor space 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
- Lemma 2.5(i–ii), Lemma 2.6(iv), Exercise 2.8(a), printed pp14–15; local exhaustion argument fills the abbreviated sigma-algebra step (standard reference, not scraped)