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 subspaces admit polish presentations
Statement
Assume AC. If is a Borel subset of a Polish space , then has a finer Polish topology with exactly the trace sigma-algebra . In fact there is a finer Polish topology on with the same Borel sets which makes clopen. Thus is standard Borel.
Facts & Assumptions
Given: AC, a Polish space , and a Borel subset .
Polish means separable and completely metrizable. (Polish spaces are separable completely metrizable spaces)
Under countable choice, a subspace of a complete metric space has a compatible complete metric. (Under the Axiom of Countable Choice, every subspace of a complete metric space is completely metrizable)
Countably many complete metrics bounded by one have a complete product metric. (The standard weighted metric on a countable product of bounded complete metric spaces is complete)
Under countable choice, complete metrizability plus a countable basis is equivalent to being Polish. (For completely metrizable spaces, the separable and second-countable definitions of Polish space agree under countable choice)
AC selects the countable family of topology, metric and basis witnesses and supplies countable choice. (The Axiom of Choice)
A Polish presentation with exactly the given Borel sigma-algebra makes a space standard Borel. (Standard Borel spaces)
Under countable choice, a countable union of countable sets is countable. (Countable unions of at most countable sets, assuming )
A finite product of countable sets is countable, by iteration of the binary product statement. (A product of two at most countable sets is at most countable)
Proof
If is empty there is only the empty subset and the assertion holds. On nonempty , fix a compatible complete metric and a countable basis using [F1], [F4] and [F5]. An open is (repeat ), so [F2] completely metrizes it; its closed complement is complete in the restricted original metric since a limit of a sequence in a closed set stays there. Both subspaces have countable trace bases and hence are Polish by [F4].
Bound each component metric by replacing with ; this preserves its topology and Cauchy sequences, hence completeness. On the disjoint union of and , retain those metrics within components and set cross-component distance equal to two. The triangle inequality holds within a component and across components (any cross-component path includes an edge of length two). A Cauchy sequence is eventually in one component and converges there. A union of the two countable bases is countable. This Polish topology is finer than , makes clopen, and has the same Borel sets: each new open is the union of two old trace-open sets, hence old Borel. Empty components simply contribute no points.
Let be the old Borel subsets that can be made clopen by such a refinement. Step 2.1 puts every open set in ; closure under complements uses the same topology. Given , [F5] selects a witnessing Polish topology , complete bounded metric and countable basis for each . Include . In let .
The diagonal is closed. If two coordinates differ, disjoint neighbourhoods in the original metric topology pull back to open neighbourhoods in both refined coordinates; their product cylinder misses . The product is completely metrized by [F3], so its closed subspace is complete. It has a countable basis of finite cylinders restricted to ; For each finite length the coordinate-index and basis-index lists form a countable set by [F8]; [F7] makes the union over lengths countable, with its countable-choice hypothesis supplied by [F5]. By [F4] it is Polish. Pull its topology back to along . This refines every . Each basic open is a finite intersection of old Borel sets, and every open is a union of a subfamily of the countable basis. Thus every new open is old Borel; the two Borel sigma-algebras coincide.
Each is clopen in the common refinement, so is open. Apply the splitting construction of step 2.1 to that Polish topology, making the union clopen while preserving its Borel sets, hence the original Borel sets. Consequently is a sigma-algebra containing , and contains every old Borel set. For the specified , restrict the resulting complete metric and countable basis to the closed set . This is a Polish topology on , finer than its original subspace topology; its Borel sets are precisely the old traces, since relative opens generate traces of Borel sets in either topology. The identity is the Polish presentation required by [F6].
Source notes
Marker, Descriptive Set Theory, Lemmas 2.22–2.23 and Theorem 2.24, printed pp.20–21 (PDF indices 19–20), full statements and proofs read. The closed-diagonal argument is expanded using continuity to the original Hausdorff topology. Rao–Srivastava, An Elementary Proof of the Borel Isomorphism Theorem, pp.347–349, is retained as the scaffold’s independent background treatment, not a load-bearing citation in this proof.
Depends on
- Standard Borel spaces
- Polish spaces are separable completely metrizable spaces
- Under the Axiom of Countable Choice, every $G_\delta$ subspace of a complete metric space is completely metrizable
- The standard weighted metric on a countable product of bounded complete metric spaces is complete
- For completely metrizable spaces, the separable and second-countable definitions of Polish space agree under countable choice
- The Axiom of Choice
- Countable unions of at most countable sets, assuming $\mathrm{AC}_\omega$
- A product of two at most countable sets is at most countable
Used by
Dependency tree · two levels
28 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
- Rao and Srivastava, An Elementary Proof of the Borel Isomorphism Theorem (standard reference, not scraped)
- Marker, Descriptive Set Theory, Lemmas 2.22-2.23 and Theorem 2.24 (standard reference, not scraped)