Alphabeta MathHow 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 rationals are Borel and F-sigma but neither open nor closed nor G-delta
Example
The canonical copy of the rationals in is and Borel, but it is neither open nor closed nor .
Facts & Assumptions
Given: The canonical subset .
The set is and is not ( is , meager and not , while the irrationals are , residual and not ).
Both and its complement are dense in (Both and are dense in , and every nonempty open subset of is uncountable).
means a countable union of closed sets ( and subsets of ), and the Borel sigma-algebra contains every closed set and is closed under countable unions (The Borel sigma-algebra of a topological space).
Verification
By [L1] and [L3], is a countable union of closed Borel sets and is therefore Borel and .
Density of the complement in [L2] prevents from containing a nonempty open interval, so it is not open; density of and its being a proper subset prevent it from being closed.
The final claim, that is not , is exactly the third conclusion of [L1].
Depends on
- $F_\sigma$ and $G_\delta$ subsets of $\mathbb{R}$
- $\mathbb{Q}$ is $F_\sigma$, meager and not $G_\delta$, while the irrationals are $G_\delta$, residual and not $F_\sigma$
- The Borel sigma-algebra of a topological space
- Both $\mathbb{Q}$ and $\mathbb{R} \setminus \mathbb{Q}$ are dense in $\mathbb{R}$, and every nonempty open subset of $\mathbb{R}$ is uncountable
Used by
Nothing in the library uses this result yet.
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 90 results over 17 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
- T. Tao, An Introduction to Measure Theory, Definition 1.4.16 (standard reference, not scraped)