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 real line with its Borel sigma-algebra is standard Borel
Statement
The measurable space with its usual topology is standard Borel.
Facts & Assumptions
Given: The real line with its usual metric and Borel sigma-algebra.
A topological space is Polish if and only if it is separable and has a compatible complete metric. Polish spaces are separable completely metrizable spaces
A space is separable when it has a countable dense subset. Separability: the existence of an at most countable dense subset
The real line with its usual metric is complete. and for with the Euclidean metric are complete, componentwise from the Cauchy criterion in
The rationals form a countable set. is countably infinite
The rational numbers are dense in the real line. The rationals embed densely in the reals
A measurable space is standard Borel when it is measurably isomorphic to the Borel space of a Polish topology. Standard Borel spaces
Proof
Given: with its usual metric.
By [F4] and [F5], is a countable dense subset of , so [F2] makes the usual real line separable. Its usual metric is complete by [F3]. Thus the usual topology is Polish by [F1].
The identity map from to the usual Polish real line is a bijection and preserves exactly the Borel sets. The standard-Borel definition [F6] therefore applies.
Source notes
Biskup, Chapter 2, Definition 2.3 and the immediately following examples, identifies the real line with its Euclidean Borel sigma-algebra as a standard Borel space. The proof above supplies the separability and completeness argument from the named local interfaces.
Depends on
- Polish spaces are separable completely metrizable spaces
- Separability: the existence of an at most countable dense subset
- Standard Borel spaces
- The rationals embed densely in the reals
- $\mathbb{R}$ and $\mathbb{R}^n$ for $n \ge 1$ with the Euclidean metric are complete, componentwise from the Cauchy criterion in $\mathbb{R}$
- $\mathbb{Q}$ is countably infinite
Used by
Dependency tree · two levels
51 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
- O. Biskup, MATH 275D notes, Chapter 2: Kolmogorov Extension Theorem (standard reference, not scraped)