References
- [1] Higher-Order Tarski Grothendieck as a Foundation for Formal Proof, Sep. 2019. Zenodo. doi:10.4230/lipics.itp.2019.9.
- [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_17
- [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-6604425130069070
- [4] Józef Białas and Yatsuka Nakamura. The Urysohn lemma. Formalized Mathematics, 9 (3):631–636, 2001.
- [5] Nicolas Bourbaki. General Topology: Chapters 1–4. Springer Science and Business Media, 2013.
- [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_1
- [7] Roland Coghetto. Topology from neighbourhoods. Formalized Mathematics, 23(4):289–296, 2015. doi:10.1515/forma-2015-0023.10.1515/forma-2015-0023
- [8] Thierry Coquand. Théorie des types dépendants et axiome d’univalence. Séminaire Bourbaki, 66:1085, 2014.
- [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_2
- [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_2
- [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_9
- [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_12
- [13] Artur Korniłowicz. How to define terms in Mizar effectively. Studies in Logic, Grammar and Rhetoric, 18:67–77, 2009.
- [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_6
- [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-1
- [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_25
- [17] Library Committee of the Association of Mizar Users. Preliminaries to structures. Mizar Mathematical Library, 1995.
- [18] Beata Padlewska and Agata Darmochwał. Topological spaces and continuous functions. Formalized Mathematics, 1(1):223–230, 1990.
- [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/3236787
- [20] Claude Wagschal. Topologie et analyse fonctionnelle. Hermann, 1995.
- [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.