{"id":"palomar/PALOMAR-2026-10-23-000018","url":"https://github.com/Arthur742Ramos/Math-Formalization/tree/a8c08adf51ec122bff60955a260a3b2f772ea0ac/topology/lavrentieff-extension","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-23-000018-v1.json","repo":"https://github.com/Arthur742Ramos/Math-Formalization","tags":["math.GN","msc:54C20","msc:54E50","msc:54H05","general-topology","homeomorphism-extension","formalization"],"score":0,"title":"Lavrentieff's Gδ homeomorphism extension 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":"Every homeomorphism between arbitrary subsets of completely metrizable spaces extends to a homeomorphism between Gδ supersets contained in the respective closures. Empty subsets and ambient spaces are included. A zero-oscillation construction first gives a Gδ continuous extension domain for maps to complete metric spaces. Restricting the two continuous extensions gives mutually inverse maps. The arbitrary supplied topologies are preserved by compatible complete metrics. Classical mathematics, with no mathematical novelty or priority claim.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-23","reactions":{},"formalized":true,"formalizes":[{"title":"Contribution à la théorie des ensembles homéomorphes","identifier":"https://eudml.org/doc/214269","relationship":"formalizes"},{"title":"Topology for the working mathematician","identifier":"https://www.math.ru.nl/~mueger/topology.pdf","relationship":"formalizes"}]}