Email Gateway (Oct 11 2023 at 23:59): Email Gateway (Oct 11 2023 at 23:59):From: Gerwin Klein <cl-isabelle-users@lists.cam.ac.uk>
Standard Borel Spaces
by Michikazu Hirata
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 R.
https://www.isa-afp.org/entries/Standard_Borel_Spaces.html
Enjoy!
Gerwin
Last updated: Apr 29 2024 at 01:08 UTC