# Complete Spaces

Formalized Mathematics (2008)

- Volume: 16, Issue: 1, page 35-43
- ISSN: 1426-2630

## Access Full Article

top## Abstract

top## How to cite

topKarol Pąk. "Complete Spaces." Formalized Mathematics 16.1 (2008): 35-43. <http://eudml.org/doc/267316>.

@article{KarolPąk2008,

abstract = {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},

author = {Karol Pąk},

journal = {Formalized Mathematics},

language = {eng},

number = {1},

pages = {35-43},

title = {Complete Spaces},

url = {http://eudml.org/doc/267316},

volume = {16},

year = {2008},

}

TY - JOUR

AU - Karol Pąk

TI - Complete Spaces

JO - Formalized Mathematics

PY - 2008

VL - 16

IS - 1

SP - 35

EP - 43

AB - 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

LA - eng

UR - http://eudml.org/doc/267316

ER -

## References

top- [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. Zbl0373.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.

## NotesEmbed ?

topTo embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.