A Case Study of Transporting Urysohn’s Lemma from Topology via Open Sets into Topology via Neighborhoods

[1] Higher-Order Tarski Grothendieck as a Foundation for Formal Proof, Sep. 2019. Zenodo. doi:10.4230/lipics.itp.2019.9.Search in Google Scholar

[2] Grzegorz Bancerek, Czesław Byliński, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, Karol Pąk, and Josef Urban. Mizar: State-of-the-art and beyond. In Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, and Volker Sorge, editors, Intelligent Computer Mathematics, volume 9150 of Lecture Notes in Computer Science, pages 261–279. Springer International Publishing, 2015. ISBN 978-3-319-20614-1. doi:10.1007/978-3-319-20615-8_17.10.1007/978-3-319-20615-8_17Search in Google Scholar

[3] Grzegorz Bancerek, Czesław Byliński, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, and Karol Pąk. The role of the Mizar Mathematical Library for interactive proof development in Mizar. Journal of Automated Reasoning, 61(1):9–32, 2018. doi:10.1007/s10817-017-9440-6.10.1007/s10817-017-9440-6604425130069070Search in Google Scholar

[4] Józef Białas and Yatsuka Nakamura. The Urysohn lemma. Formalized Mathematics, 9 (3):631–636, 2001.Search in Google Scholar

[5] Nicolas Bourbaki. General Topology: Chapters 1–4. Springer Science and Business Media, 2013.Search in Google Scholar

[6] Nicolas Bourbaki. Topologie générale: Chapitres 1à 4. Eléments de mathématique. Springer Science & Business Media, 2007.10.1007/978-3-540-34486-5_1Search in Google Scholar

[7] Roland Coghetto. Topology from neighbourhoods. Formalized Mathematics, 23(4):289–296, 2015. doi:10.1515/forma-2015-0023.10.1515/forma-2015-0023Search in Google Scholar

[8] Thierry Coquand. Théorie des types dépendants et axiome d’univalence. Séminaire Bourbaki, 66:1085, 2014.Search in Google Scholar

[9] Adam Grabowski and Roland Coghetto. Extending Formal Topology in Mizar by Uniform Spaces, pages 77–105. Springer, Cham, 2020. ISBN 978-3-030-41425-2. doi:10.1007/978-3-030-41425-2_2.10.1007/978-3-030-41425-2_2Search in Google Scholar

[10] Adam Grabowski, Artur Korniłowicz, and Christoph Schwarzweller. Refining Algebraic Hierarchy in Mathematical Repository of Mizar, pages 49–75. Springer, Cham, 2020. ISBN 978-3-030-41425-2. doi:10.1007/978-3-030-41425-2_2.10.1007/978-3-030-41425-2_2Search in Google Scholar

[11] Brian Huffman and Ondřej Kunčar. Lifting and transfer: A modular design for quotients in Isabelle/HOL. In International Conference on Certified Programs and Proofs, pages 131–146. Springer, 2013.10.1007/978-3-319-03545-1_9Search in Google Scholar

[12] Einar Broch Johnsen and Christoph Lüth. Theorem reuse by proof term transformation. In International Conference on Theorem Proving in Higher Order Logics, pages 152–167. Springer, 2004.10.1007/978-3-540-30142-4_12Search in Google Scholar

[13] Artur Korniłowicz. How to define terms in Mizar effectively. Studies in Logic, Grammar and Rhetoric, 18:67–77, 2009.Search in Google Scholar

[14] Nicolas Magaud. Changing data representation within the Coq system. In International Conference on Theorem Proving in Higher Order Logics, pages 87–102. Springer, 2003.10.1007/10930755_6Search in Google Scholar

[15] Yatsuka Nakamura, Nobuyuki Tamura, and Wenpai Chang. A theory of matrices of real elements. Formalized Mathematics, 14(1):21–28, 2006. doi:10.2478/v10037-006-0004-1.10.2478/v10037-006-0004-1Search in Google Scholar

[16] Kazuhisa Nakasho and Yasunari Shidama. Documentation generator focusing on symbols for the HTML-ized Mizar library. In Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, and Volker Sorge, editors, Intelligent Computer Mathematics, CICM 2015, volume 9150 of Lecture Notes in Computer Science, pages 343–347. Springer, Cham, 2015. doi:10.1007/978-3-319-20615-8_25.10.1007/978-3-319-20615-8_25Search in Google Scholar

[17] Library Committee of the Association of Mizar Users. Preliminaries to structures. Mizar Mathematical Library, 1995.Search in Google Scholar

[18] Beata Padlewska and Agata Darmochwał. Topological spaces and continuous functions. Formalized Mathematics, 1(1):223–230, 1990.Search in Google Scholar

[19] Nicolas Tabareau, Éric Tanter, and Matthieu Sozeau. Equivalences for free: univalent parametricity for effective transport. Proceedings of the ACM on Programming Languages, 2(ICFP):1–29, 2018.10.1145/3236787Search in Google Scholar

[20] Claude Wagschal. Topologie et analyse fonctionnelle. Hermann, 1995.Search in Google Scholar

[21] Theo Zimmermann and Hugo Herbelin. Automatic and transparent transfer of theorems along isomorphisms in the Coq proof assistant. arXiv preprint arXiv:1505.05028, 2015.Search in Google Scholar