Compactness in Metric Spaces

In this article, we mainly formalize in Mizar [2] the equivalence among a few compactness definitions of metric spaces, norm spaces, and the real line. In the first section, we formalized general topological properties of metric spaces. We discussed openness and closedness of subsets in metric spaces in terms of convergence of element sequences. In the second section, we firstly formalize the definition of sequentially compact, and then discuss the equivalence of compactness, countable compactness, sequential compactness, and totally boundedness with completeness in metric spaces.In the third section, we discuss compactness in norm spaces. We formalize the equivalence of compactness and sequential compactness in norm space. In the fourth section, we formalize topological properties of the real line in terms of convergence of real number sequences. In the last section, we formalize the equivalence of compactness and sequential compactness in the real line. These formalizations are based on [20], [5], [17], [14], and [4].Nakasho Kazuhisa - Shinshu University Nagano, JapanNarita Keiko - Hirosaki-city Aomori, JapanShidama Yasunari - Shinshu University Nagano, JapanGrzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41-46, 1990.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.Leszek Borys. Paracompact and metrizable spaces. Formalized Mathematics, 2(4):481-485, 1991.Nicolas Bourbaki. General Topology: Chapters 1-4. Springer Science and Business Media, 2013.Nicolas Bourbaki, H.G. Eggleston, and S. Madan. Elements of mathematics: Topological vector spaces. Springer-Verlag, 1987.Czesław Bylinski. Functions and their basic properties. Formalized Mathematics, 1(1): 55-65, 1990.Czesław Bylinski. Functions from a set to a set. Formalized Mathematics, 1(1):153-164, 1990.Czesław Bylinski. Some basic properties of sets. Formalized Mathematics, 1(1):47-53, 1990.Agata Darmochwał and Yatsuka Nakamura. Metric spaces as topological spaces - fundamental concepts. Formalized Mathematics, 2(4):605-608, 1991.Adam Grabowski. On the subcontinua of a real line. Formalized Mathematics, 11(3): 313-322, 2003.Adam Grabowski. On the boundary and derivative of a set. Formalized Mathematics, 13 (1):139-146, 2005.Stanisława Kanas, Adam Lecko, and Mariusz Startek. Metric spaces. Formalized Mathematics, 1(3):607-610, 1990.Artur Korniłowicz. Recursive definitions. Part II. Formalized Mathematics, 12(2):167-172, 2004.Erwin Kreyszig. Introductory Functional Analysis with Applications. Wiley, 1 edition, 1989.Gilbert Lee and Piotr Rudnicki. Dickson’s lemma. Formalized Mathematics, 10(1):29-37, 2002.Karol Pak. Complete spaces. Formalized Mathematics, 16(1):35-43, 2008.Walter Rudin. Functional Analysis. New York, McGraw-Hill, 2nd edition, 1991.Andrzej Trybulec. Function domains and Frænkel operator. Formalized Mathematics, 1 (3):495-500, 1990.Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1 (1):73-83, 1990.Kosaku Yoshida. Functional Analysis. Springer, 1980