This paper is a continuation of [12]. First some definitions needed to formulate Cantor's theorem on complete spaces and show several facts about them are introduced. Next section contains the proof of Cantor's theorem and some properties of complete spaces resulting from this theorem. Moreover, countable compact spaces and proofs of auxiliary facts about them is defined. I also show the important condition that every metric space is compact if and only if it is countably compact. Then I prove that every metric space is compact if and only if it is a complete and totally bounded space. I also introduce the definition of the metric space with the well metric. This article is based on [13].MML identifier: COMPL SP, version: 7.8.05 4.89.993
@article{bwmeta1.element.doi-10_2478_v10037-008-0006-2,
author = {Karol P\k ak},
title = {Complete Spaces},
journal = {Formalized Mathematics},
volume = {16},
year = {2008},
pages = {35-43},
language = {en},
url = {http://dml.mathdoc.fr/item/bwmeta1.element.doi-10_2478_v10037-008-0006-2}
}
Karol Pąk. Complete Spaces. Formalized Mathematics, Tome 16 (2008) pp. 35-43. http://gdmltest.u-ga.fr/item/bwmeta1.element.doi-10_2478_v10037-008-0006-2/
[1] Grzegorz Bancerek. The ordinal numbers. Formalized Mathematics, 1(1):91-96, 1990.
[2] Grzegorz Bancerek. Countable sets and Hessenberg's theorem. Formalized Mathematics, 2(1):65-69, 1991.
[3] Józef Białas and Yatsuka Nakamura. Dyadic numbers and T4 topological spaces. Formalized Mathematics, 5(3):361-366, 1996.
[4] Leszek Borys. Paracompact and metrizable spaces. Formalized Mathematics, 2(4):481-485, 1991.
[5] Czesław Byliński. Functions and their basic properties. Formalized Mathematics, 1(1):55-65, 1990.
[6] Czesław Byliński. Functions from a set to a set. Formalized Mathematics, 1(1):153-164, 1990.
[7] Czesław Byliński. Some basic properties of sets. Formalized Mathematics, 1(1):47-53, 1990.
[8] Agata Darmochwał. Compact spaces. Formalized Mathematics, 1(2):383-386, 1990.
[9] Agata Darmochwał. Families of subsets, subspaces and mappings in topological spaces. Formalized Mathematics, 1(2):257-261, 1990.
[10] Agata Darmochwał. Finite sets. Formalized Mathematics, 1(1):165-167, 1990.
[11] Agata Darmochwał and Yatsuka Nakamura. Metric spaces as topological spaces - fundamental concepts. Formalized Mathematics, 2(4):605-608, 1991.
[12] Alicia de la Cruz. Totally bounded metric spaces. Formalized Mathematics, 2(4):559-562, 1991.
[13] Ryszard Engelking. General Topology, volume 60 of Monografie Matematyczne. PWN - Polish Scientific Publishers, Warsaw, 1977. | Zbl 0373.54002
[14] Adam Grabowski. On the Kuratowski limit operators. Formalized Mathematics, 11(4):399-409, 2003.
[15] Adam Grabowski. On the boundary and derivative of a set. Formalized Mathematics, 13(1):139-146, 2005.
[16] Krzysztof Hryniewiecki. Basic properties of real numbers. Formalized Mathematics, 1(1):35-40, 1990.
[17] Stanisława Kanas, Adam Lecko, and Mariusz Startek. Metric spaces. Formalized Mathematics, 1(3):607-610, 1990.
[18] Jarosław Kotowicz. Convergent sequences and the limit of sequences. Formalized Mathematics, 1(2):273-275, 1990.
[19] Jarosław Kotowicz. Monotone real sequences. Subsequences. Formalized Mathematics, 1(3):471-475, 1990.
[20] Jarosław Kotowicz. Real sequences and basic operations on them. Formalized Mathematics, 1(2):269-272, 1990.
[21] Robert Milewski. Bases of continuous lattices. Formalized Mathematics, 7(2):285-294, 1998.
[22] Beata Padlewska. Families of sets. Formalized Mathematics, 1(1):147-152, 1990.
[23] Beata Padlewska and Agata Darmochwał. Topological spaces and continuous functions. Formalized Mathematics, 1(1):223-230, 1990.
[24] Andrzej Trybulec. Domains and their Cartesian products. Formalized Mathematics, 1(1):115-122, 1990.
[25] Michał Trybulec. Formal languages - concatenation and closure. Formalized Mathematics, 15(1):11-15, 2007.
[26] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67-71, 1990.
[27] Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1(1):73-83, 1990.
[28] Edmund Woronowicz. Relations defined on sets. Formalized Mathematics, 1(1):181-186, 1990.
[29] Edmund Woronowicz and Anna Zalewska. Properties of binary relations. Formalized Mathematics, 1(1):85-89, 1990.