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.
The Borel sigma-algebra of a subspace is the trace of the ambient Borel sigma-algebra
Statement
Let be a subspace of a topological space . Then
Facts & Assumptions
Given: A topological space and a subset with its subspace topology.
The subspace topology on consists exactly of the traces of open sets of (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).
Generating a sigma-algebra commutes with taking traces (Generating a sigma-algebra commutes with taking traces).
The Borel sigma-algebra of a topological space is generated by its open sets (The Borel sigma-algebra of a topological space).
Proof
By [L1], the family generating is precisely the trace on of the family generating .
Applying [L2] to the family of open subsets of gives .
Depends on
Used by
- Polar integration may discard the cut locus Corollary
- There is a Lebesgue measurable subset of ℝ that is not Borel Corollary
- The polar surface set function on the unit sphere Definition
- Matching C¹ pieces across a hyperplane have no jump derivative Example
- Sharp Sobolev threshold for a radial power Example
- The Borel sigma-algebra of the Cantor set is the trace of the real Borel sigma-algebra Example
- FALSE: every Riemann integrable function on a closed bounded interval is Borel measurable False statement
- A bounded Riemann integrable function admits Borel Darboux envelopes with the same Lebesgue integral Lemma
- Agreement of Borel overlap integrals Lemma
- Lebesgue-Stieltjes measures on ℝ are outer regular and inner regular by compact sets Theorem
Dependency tree · two levels
11 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
- T. Tao, An Introduction to Measure Theory, Exercise 1.4.12 (standard reference, not scraped)