Bing’s shrinking method is a key technique for constructing homeomorphisms between topological manifolds in geometric topology. Applications of this method include the generalized Schoenflies theorem, the double suspension theorem for homology spheres, and the 4-dimensional Poincaré conjecture. Homeomorphisms obtained in this method are sometimes counter-intuitive and may even be pathological. This makes Bing’s shrinking method a good target of formalization by proof assistants. We report our formalization of this method in Coq/Ssreflect.
CITATION STYLE
Kuga, K., Hagiwara, M., & Yamamoto, M. (2016). Formalization of Bing’s shrinking method in geometric topology. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9791, pp. 18–27). Springer Verlag. https://doi.org/10.1007/978-3-319-42547-4_2
Mendeley helps you to discover research relevant for your work.