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.
Baire property sigma-algebra and Borel regularity
Statement
In ZFC, in every topological space X the sets with the Baire property form a sigma-algebra containing all Borel sets. Every meagre subset has the Baire property. Every Baire-property set differs from both an set and a set by a meagre set.
Facts & Assumptions
The property of Baire defines Baire-property sets by meagre error from an open set.
The countable Borel hierarchy and its limit convention defines the least sigma-algebra containing the opens.
Assume The Axiom of Choice.
Proof
Given: An arbitrary topological X. Here means a countable union of closed sets, and a countable intersection of open sets.
A subset of a nowhere dense set is nowhere dense since closure is monotone. A finite union of nowhere dense sets is nowhere dense: inside any nonempty open, successively refine to a nonempty open avoiding each of the finitely many closures; the final refinement avoids their union. Subsets of meagre sets retain the same covering witnesses. For a sequence of meagre sets, A1 chooses a nowhere dense covering sequence for each; the diagonal pairing of their two natural indices yields a covering sequence for the union. Thus meagre sets form an ideal closed under countable unions. The empty set has the all-empty witness sequence.
For closed F, is closed with empty interior: a nonempty open contained in it would be contained in F and hence in its interior, a contradiction. Thus F differs from its open interior by a nowhere dense set and has the Baire property. If U is open, its boundary is closed nowhere dense: any nonempty open inside must meet U, precluding containment in that difference. These statements use only the closure and interior definitions, so hold without separation axioms.
Suppose is meagre with U open. Its complementary set differs from closed by the same error; step 1.2 replaces that closed set by its open interior at a further nowhere dense error. Step 1.1 therefore makes the complement Baire-property. For a sequence of Baire-property , A1 selects witnessing opens U_n. The error is contained in , meagre by step 1.1. Thus this class is a sigma-algebra, containing opens and all meagre sets by F1. F2's leastness puts every Borel set in it.
Enclose in a meagre set by closing its specified nowhere dense witnesses. Put and . Then G is , since , and H is . We have . Moreover and , both meagre by steps 1.1–1.2. These give the two required meagre symmetric differences, also when X, U or M is empty. QED.
Depends on
Used by
Dependency tree · two levels
8 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
- Definitions 2.46/2.53/2.55, Exercises 2.48–2.50/2.54 and Lemmas 2.51/2.56, Corollary 2.57 and Exercise 2.58, printed pp26–27 (standard reference, not scraped)