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

BSD License

### Topics

- Mathematics/Analysis
- Mathematics/Topology

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

### Session Standard_Borel_Spaces

- Lemmas_StandardBorel
- Set_Based_Metric_Space
- Set_Based_Metric_Product
- Abstract_Metrizable_Topology
- StandardBorel
- Space_of_Continuous_Maps

### Used by

- Disintegration Theorem
- S-Finite Measure Monad on Quasi-Borel Spaces

## Cite

×

Standard_Borel_Spaces-AFP

    @article{Standard_Borel_Spaces-AFP,
      author  = {Michikazu Hirata},
      title   = {Standard Borel Spaces},
      journal = {Archive of Formal Proofs},
      month   = {August},
      year    = {2023},
      note    = {\url{https://isa-afp.org/entries/Standard_Borel_Spaces.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest