### Abstract

This entry includes a formalization of standard Borel spaces and (a variant of) the Borel isomorphism theorem. A separable complete metrizable topological space is called a polish space and a measurable space generated from a polish space is called a standard Borel space. We formalize the notion of standard Borel spaces by establishing set-based metric spaces, and then prove (a variant of) the Borel isomorphism theorem. The theorem states that a standard Borel spaces is either a countable discrete space or isomorphic to $\mathbb{R}$.

### License

### History

- October 26, 2023
- adjust theories to the set-based metric space library in Isabelle2023

### Topics

### Related publications

- Hirata, M., Minamide, Y., & Sato, T. (2023).
*Semantic Foundations of Higher-Order Probabilistic Programs in Isabelle/HOL*. Schloss Dagstuhl â€“ Leibniz-Zentrum fÃ¼r Informatik. https://doi.org/10.4230/LIPICS.ITP.2023.18