{"id":"palomar/PALOMAR-2026-10-17-000019","url":"https://github.com/Arthur742Ramos/Math-Formalization/tree/cd7ae6bc5f4a1e5569cbbe1a883b83e92eb07a0e/topology/hewitt-marczewski-pondiczery","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-17-000019-v1.json","repo":"https://github.com/Arthur742Ramos/Math-Formalization","tags":["math.GN","msc:54B10","msc:54D65","msc:54A25","general-topology","separability","product-spaces"],"score":0,"title":"Countable-density Hewitt–Marczewski–Pondiczery theorem","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 product of at most continuum many separable topological spaces is separable. The proof constructs a countable family of finite binary tables that realizes every finite assignment of natural-number labels, then applies dense sequences in the factors. No separation, metrizability, compactness or countable-base assumption on the factors is needed. Empty factors and empty index sets are allowed. A companion theorem proves the sharp criterion for discrete Boolean cubes: Bool^I is separable exactly when the index cardinality is at most continuum. This is the classical countable-density case; no…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-17","reactions":{},"formalized":true,"formalizes":[{"title":"Hewitt-Marczewski-Pondiczery type theorem for abelian groups and Markov’s potential density, arXiv:0912.0497v1","identifier":"https://arxiv.org/pdf/0912.0497v1","relationship":"formalizes"}]}