{"id":"palomar/PALOMAR-2026-10-16-000021","url":"https://github.com/Arthur742Ramos/Math-Formalization/tree/8ff5eedba962cb74050fe6d5f0acd934ba830fc5/topology/alexandroff-urysohn","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-16-000021-v1.json","repo":"https://github.com/Arthur742Ramos/Math-Formalization","tags":["math.GN","msc:54E35","msc:54E15","topology","metrization","lean-formalization","uniform-spaces"],"score":0,"title":"Alexandroff–Urysohn cover metrization","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 T0 space is metrizable if and only if it admits a sequence of open covers such that every intersecting pair of members at the next level has union contained in one member at the current level, and the point-stars form a neighborhood basis. Without separation the same criterion characterizes pseudometrizability. The proof constructs a countably generated co-membership uniformity with exactly the supplied topology. Covers have unrestricted cardinality; empty spaces are included. Classical mathematics, with no novelty or priority claim.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-16","reactions":{},"formalized":true,"formalizes":[{"title":"Geometric Aspects of General Topology, second-edition author manuscript (November 2, 2023)","identifier":"https://www.researchgate.net/profile/Katsuro-Sakai/publication/299698540_Metrization_and_Paracompact_Spaces/links/6589f0136f6e450f19a3d3b8/Metrization-and-Paracompact-Spaces.pdf","relationship":"formalizes"}]}