{"id":"palomar/PALOMAR-2026-10-12-000003","url":"https://github.com/Arthur742Ramos/Math-Formalization/tree/ccc3ca43dc26c6774f2afd7f2b2223066451c362/topology/dowker-characterization","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-12-000003-v1.json","repo":"https://github.com/Arthur742Ramos/Math-Formalization","tags":["math.GN","msc:54D15","msc:54D20","msc:54B10","msc:54C30","general-topology","paracompactness","lean-formalization"],"score":0,"title":"Dowker's countable paracompactness, product normality and strict insertion characterization","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":"Formalization of Dowker (1951), Theorem 4: normality plus ordinary countable paracompactness of an arbitrary topological space X is equivalent to normality of X times the closed unit interval, and to strict continuous insertion between arbitrary real upper and lower semicontinuous functions h<g. No T1 or Hausdorff assumption on X, boundedness or uniform gap is added. Companion compact metrizable product theorem (Lemma 3) and countable-cover/decreasing-closed-sequence equivalences (Theorem 2) are included.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-12","reactions":{},"formalized":true,"formalizes":[{"title":"On countably paracompact spaces","identifier":"https://doi.org/10.4153/CJM-1951-026-2","relationship":"formalizes"}]}