{"id":"palomar/PALOMAR-2026-10-28-000011","url":"https://github.com/Arthur742Ramos/Math-Formalization/tree/537b3000679eb402ce37fda0866e715412e04a12/topology/mycielski-cantor-independent","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-28-000011-v1.json","repo":"https://github.com/Arthur742Ramos/Math-Formalization","tags":["math.GN","math.LO","msc:54H05","msc:03E15","msc:54E52"],"score":0,"title":"Mycielski Cantor independent set for dense-open binary relations","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 nonempty open subset U of a perfect Polish space X contains a closed topological embedding e of Cantor space Nat -> Bool such that every ordered pair of distinct image points lies in each member of a countable family of dense-open subsets R_n of X × X. Coordinated finite refinements enforce all ordered pairs, have closure nesting and vanishing diameter; ambient completeness yields the Cantor limit map. Single-Cantor binary-relation scope only; no novelty claim.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-28","reactions":{},"formalized":true,"formalizes":[{"title":"Independent sets in topological algebras","identifier":"https://eudml.org/doc/213780","relationship":"formalizes"},{"title":"A dynamical version of Kuratowski–Mycielski theorem and invariant chaotic sets","identifier":"https://arxiv.org/abs/1801.10266v1","relationship":"formalizes"}]}