{"id":"palomar/PALOMAR-2026-10-23-000003","url":"https://github.com/Arthur742Ramos/Math-Formalization/tree/d33817461fadbe8d7498a237b0c5bc27dc044afb/topology/sierpinski-rationals","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-23-000003-v1.json","repo":"https://github.com/Arthur742Ramos/Math-Formalization","tags":["math.GN","msc:54F65","msc:54E35","msc:06A05","general-topology","rational-numbers","formalization"],"score":0,"title":"Sierpiński's characterization of the rationals","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 countable metrizable topological space without isolated points is homeomorphic to the rational numbers with their usual topology. Conversely, these four properties characterize spaces homeomorphic to the rationals. A clopen basis is derived from the hypotheses. Scheduled binary clopen splits give each point an address with both bits arbitrarily far out; the induced lexicographic order is proved dense, without endpoints, and to generate exactly the original topology. The countable dense-order isomorphism theorem then gives the homeomorphism. This formalizes classical…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-23","reactions":{},"formalized":true,"formalizes":[{"title":"Two Topological Uniqueness Theorems for Spaces of Real Numbers, arXiv:1210.1008v1","identifier":"https://arxiv.org/pdf/1210.1008v1","relationship":"formalizes"}]}