{"id":"palomar/PALOMAR-2026-10-14-000001","url":"https://github.com/Arthur742Ramos/Math-Formalization/tree/6aa68b2cb67719a187e64de29567443575eb560e/topology/nagata-smirnov","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-14-000001-v1.json","repo":"https://github.com/Arthur742Ramos/Math-Formalization","tags":["math.GN","msc:54E35","msc:54D20","msc:54D15","general-topology","metrization","lean"],"score":0,"title":"The full Nagata–Smirnov 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 regular Hausdorff space is metrizable if and only if it has an open basis expressed as a countable union of locally finite families. Every layer can have arbitrary cardinality. The development proves the necessity using metric paracompactness, perfect normality from the basis, continuity of arbitrary locally finite bounded coordinates, and a compatible metric via a countable product of metric function spaces. It assumes neither second countability nor separability and includes empty spaces. This formalizes classical mathematics, without claiming new mathematics or first formalization…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-14","reactions":{},"formalized":true,"formalizes":[{"title":"Geometric Aspects of General Topology, second-edition author manuscript (November 2, 2023), chapter 2: Metrizability, Paracompactness, and Related Properties","identifier":"https://www.researchgate.net/publication/299698540_Metrization_and_Paracompact_Spaces","relationship":"formalizes"}]}