{"id":"palomar/PALOMAR-2026-10-22-000041","url":"https://github.com/Arthur742Ramos/Math-Formalization/tree/87652c909a92afded15aad86a901d8c11dd75ed8/topology/open-baire-representation","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-22-000041-v1.json","repo":"https://github.com/Arthur742Ramos/Math-Formalization","tags":["math.GN","msc:54C10","msc:54E50","msc:54E52","msc:03E15","general-topology","baire-space","polish-spaces","descriptive-set-theory"],"score":0,"title":"Open Baire-space representation of Polish spaces","trust":"high","domain":"math.GN","source":"palomar","authors":["Arthur Freitas Ramos","David Barros Hulak","Ruy Jose Guerra Barretto de Queiroz"],"reviews":0,"subject":"math.GN","summary":"Every nonempty Polish space is the image of Baire space, the product of countably many discrete natural-number spaces, under a continuous open surjection. The proof constructs a countably branching nonempty open scheme with nested closures, covering children and geometrically shrinking diameters. The image of each basic cylinder is proved exactly equal to its scheme open set. This yields openness and surjectivity of the limit map; existence is also characterized by nonemptiness. These are classical results, with no novelty or priority claim.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-22","reactions":{},"formalized":true,"formalizes":[{"title":"Descriptive Set Theory, Fall 2002 lecture notes","identifier":"https://homepages.math.uic.edu/~marker/math512/dst.pdf","relationship":"formalizes"}]}