References
- [1] Grzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41-46, 1990.
- [2] Grzegorz Bancerek, Czesław Bylinski, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, Karol Pak, 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.
- [3] Leszek Borys. Paracompact and metrizable spaces. Formalized Mathematics, 2(4):481-485, 1991.
- [4] Nicolas Bourbaki. General Topology: Chapters 1-4. Springer Science and Business Media, 2013.
- [5] Nicolas Bourbaki, H.G. Eggleston, and S. Madan. Elements of mathematics: Topological vector spaces. Springer-Verlag, 1987.
- [6] Czesław Bylinski. Functions and their basic properties. Formalized Mathematics, 1(1): 55-65, 1990.
- [7] Czesław Bylinski. Functions from a set to a set. Formalized Mathematics, 1(1):153-164, 1990.
- [8] Czesław Bylinski. Some basic properties of sets. Formalized Mathematics, 1(1):47-53, 1990.
- [9] Agata Darmochwał and Yatsuka Nakamura. Metric spaces as topological spaces - fundamental concepts. Formalized Mathematics, 2(4):605-608, 1991.
- [10] Adam Grabowski. On the subcontinua of a real line. Formalized Mathematics, 11(3): 313-322, 2003.
- [11] Adam Grabowski. On the boundary and derivative of a set. Formalized Mathematics, 13 (1):139-146, 2005.
- [12] Stanisława Kanas, Adam Lecko, and Mariusz Startek. Metric spaces. Formalized Mathematics, 1(3):607-610, 1990.
- [13] Artur Korniłowicz. Recursive definitions. Part II. Formalized Mathematics, 12(2):167-172, 2004.
- [14] Erwin Kreyszig. Introductory Functional Analysis with Applications. Wiley, 1 edition, 1989.
- [15] Gilbert Lee and Piotr Rudnicki. Dickson’s lemma. Formalized Mathematics, 10(1):29-37, 2002.
- [16] Karol Pak. Complete spaces. Formalized Mathematics, 16(1):35-43, 2008. doi:10.2478/v10037-008-0006-2.
- [17] Walter Rudin. Functional Analysis. New York, McGraw-Hill, 2nd edition, 1991.
- [18] Andrzej Trybulec. Function domains and Frænkel operator. Formalized Mathematics, 1 (3):495-500, 1990.
- [19] Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1 (1):73-83, 1990.
- [20] Kosaku Yoshida. Functional Analysis. Springer, 1980.