{"id":"palomar/PALOMAR-2026-10-18-000027","url":"https://github.com/Arthur742Ramos/Math-Formalization/tree/5ad14f00d92275a9e782fb9491dbfd8d8d8f9faf/topology/collectionwise-normal","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-18-000027-v1.json","repo":"https://github.com/Arthur742Ramos/Math-Formalization","tags":["math.GN","msc:54D15","msc:54D20","general-topology","paracompactness","lean"],"score":0,"title":"Paracompact expansion and collectionwise separation","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":"Every locally finite indexed family of arbitrary subsets of a paracompact topological space admits a locally finite open expansion with the same index type, without separation assumptions. In a paracompact normal space, a discrete closed family admits a discrete locally finite open expansion whose closures are pairwise disjoint and lie in prescribed open neighborhoods. Consequently every paracompact Hausdorff space is collectionwise normal. Index and ambient types may be empty and have independent universes; the family has unrestricted cardinality. These are classical results; no novelty is…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-18","reactions":{},"formalized":true,"formalizes":[{"title":"On expanding locally finite collections, Canadian Journal of Mathematics 23(1) (1971), 58–68","identifier":"https://www.cambridge.org/core/services/aop-cambridge-core/content/view/778ABD4D951A8DAA9B1F88F887604533/S0008414X00052974a.pdf/div-class-title-on-expanding-locally-finite-collections-div.pdf","relationship":"formalizes"}]}