{"id":"palomar/PALOMAR-2026-10-11-000013","url":"https://github.com/Arthur742Ramos/Math-Formalization/tree/dac5d2d127d25d61e972fc5d9fc442146c67440d/topology/michael-biquotient","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-11-000013-v1.json","repo":"https://github.com/Arthur742Ramos/Math-Formalization","tags":["math.GN","msc:54C10","msc:54B10","msc:54A20","msc:54D20","general-topology","biquotient-maps","lean-formalization"],"score":0,"title":"Michael's biquotient-map product and characterization theorems","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 Michael (1968), Theorems 1.2 and 1.3: arbitrary indexed products of biquotient continuous surjections are biquotient, without separation assumptions; for a Hausdorff target, biquotience is equivalent to quotientness of the product with every identity map and to the same property for paracompact test spaces. The cover definition, filter and ultrafilter bridges, and an actual Hausdorff paracompact counterexample topology on the underlying target set are proved. Reverse tests use the target universe; the forward implication is separately universe-polymorphic.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-11","reactions":{},"formalized":true,"formalizes":[{"title":"Bi-quotient maps and cartesian products of quotient maps","identifier":"https://www.numdam.org/article/AIF_1968__18_2_287_0.pdf","relationship":"formalizes"}]}