This is an unofficial reimagining of the Archive of Formal Proofs
Quasi-Borel Spacesby Michikazu Hirata, Yasuhiko Minamide and Tetsuya Sato