Compactness in Metric Spaces

Kazuhisa Nakasho, Keiko Narita, and Yasunari Shidama. "Compactness in Metric Spaces." Formalized Mathematics 24.3 (2016): 167-172. <http://eudml.org/doc/287988>.

@article{KazuhisaNakasho2016,
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].},
author = {Kazuhisa Nakasho, Keiko Narita, Yasunari Shidama},
journal = {Formalized Mathematics},
keywords = {metric spaces; normed linear spaces; compactness},
language = {eng},
number = {3},
pages = {167-172},
title = {Compactness in Metric Spaces},
url = {http://eudml.org/doc/287988},
volume = {24},
year = {2016},
}

TY - JOUR
AU - Kazuhisa Nakasho
AU - Keiko Narita
AU - Yasunari Shidama
TI - Compactness in Metric Spaces
JO - Formalized Mathematics
PY - 2016
VL - 24
IS - 3
SP - 167
EP - 172
AB - 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].
LA - eng
KW - metric spaces; normed linear spaces; compactness
UR - http://eudml.org/doc/287988
ER -