### 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

### 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