{"id":"palomar/PALOMAR-2026-10-13-000004","url":"https://github.com/Arthur742Ramos/Math-Formalization/tree/984a610395e195b8d3ca0cd88282ef343e74d33d/topology/perfect-paracompact","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-13-000004-v1.json","repo":"https://github.com/Arthur742Ramos/Math-Formalization","tags":["math.GN","msc:54D20","msc:54C10","topology","paracompactness","lean"],"score":0,"title":"Perfect surjections and paracompactness","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 continuous closed surjection from a Hausdorff space, with compact fibres, preserves and reflects ordinary open-cover paracompactness. The paracompact image is proved Hausdorff without assuming target separation. Supporting selected results give inverse transfer without separation or surjectivity, forward transfer to a regular target, local finiteness of images of arbitrary indexed families, and the regular-space criterion using arbitrary locally finite refinements. No metrizability, countability, local compactness or uniform fibre-size assumption is imposed. The source is based on Munkres…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-13","reactions":{},"formalized":true,"formalizes":[{"title":"Topology, second edition (2000), section 41 exercise 8(a),(b)","identifier":"ISBN 978-0-13-181629-9","relationship":"formalizes"},{"title":"Geometric Aspects of General Topology, second-edition manuscript, chapter 2 (November 2, 2023)","identifier":"https://www.researchgate.net/publication/299698540_Metrization_and_Paracompact_Spaces","relationship":"formalizes"}]}