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