{"id":"palomar/PALOMAR-2026-10-15-000002","url":"https://github.com/Arthur742Ramos/Math-Formalization/tree/20375446decf52134cb2788640fe19b580002c05/topology/smirnov-local-metrization","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-15-000002-v1.json","repo":"https://github.com/Arthur742Ramos/Math-Formalization","tags":["math.GN","msc:54E35","msc:54D20","general-topology","metrization","paracompact-spaces"],"score":0,"title":"Smirnov's local-to-global metrization theorem","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":"A space is metrizable if and only if it is Hausdorff, paracompact and locally metrizable. A reusable construction gives a sigma locally finite basis from any point-finite open cover of metrizable patches in a paracompact space, without a separation hypothesis. Local neighborhoods, the cover index and each basis layer may have arbitrary cardinality. The proof assumes no second countability, separability, local compactness or nonemptiness. Classical mathematics; no novelty or priority claim.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-15","reactions":{},"formalized":true,"formalizes":[{"title":"Topology, second edition (2000), Section 42","identifier":"ISBN:9780131816299","relationship":"formalizes"},{"title":"Geometric Aspects of General Topology, second-edition author manuscript (November 2, 2023)","identifier":"https://www.researchgate.net/publication/299698540_Metrization_and_Paracompact_Spaces","relationship":"formalizes"}]}