{"id":"palomar/PALOMAR-2026-10-17-000011","url":"https://github.com/Arthur742Ramos/Math-Formalization/tree/47aaba112beb17b7c0ca68f56356c5c829ee154d/topology/compact-countable-network","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-17-000011-v1.json","repo":"https://github.com/Arthur742Ramos/Math-Formalization","tags":["math.GN","msc:54E35","msc:54D30","general-topology","metrization","lean-formalization","compact-spaces"],"score":0,"title":"Compact Hausdorff countable-network 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":"For an arbitrary compact Hausdorff space, metrizability and second countability are each equivalent to the existence of a countable network of arbitrary subsets. A genuine Urysohn-function construction from pairs of network elements supplies continuous separation, and a compatible metric induces exactly the original topology. Supporting results give bounded-real-coordinate closed embeddings, preservation under continuous surjections, arbitrary-subspace heredity and compact-subspace metrization. Empty spaces and arbitrary universes are allowed. This is classical mathematics; no novelty or…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-17","reactions":{},"formalized":true,"formalizes":[{"title":"Countable Tightness and the Grothendieck Property in Cp-Theory, arXiv:2007.08579v1","identifier":"https://arxiv.org/pdf/2007.08579v1","relationship":"formalizes"}]}