Standard Borel Spaces

Michikazu Hirata 📧

August 8, 2023

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


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}$.


BSD License


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


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.

Session Standard_Borel_Spaces