<abstract xmlns="http://www.w3.org/1999/xhtml"><p> 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.</p><p>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].</p></abstract>

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].

Compactness in Metric Spaces

Formalized Mathematics

This work is licensed under version 3.0 of the Creative Commons Attribution–ShareAlike License

{"article-title":"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...

Compactness in Metric Spaces

Published Online: Feb 21, 2017

Page range: 167 - 172

Received: Jun 30, 2016

DOI: https://doi.org/10.1515/forma-2016-0013

Keywords
metric spaces, normed linear spaces, compactness

© by Kazuhisa Nakasho

This work is licensed under version 3.0 of the Creative Commons Attribution–ShareAlike License

Compactness in Metric Spaces

Published Online: Feb 21, 2017

Page range: 167 - 172

Received: Jun 30, 2016

DOI: https://doi.org/10.1515/forma-2016-0013

Keywordsmetric spaces, normed linear spaces, compactness

© by Kazuhisa Nakasho

This work is licensed under version 3.0 of the Creative Commons Attribution–ShareAlike License

Keywords
metric spaces, normed linear spaces, compactness