Complete Spaces

Karol Pąk

Formalized Mathematics (2008)

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

Abstract

top
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

How to cite

top

Karol 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. [1] Grzegorz Bancerek. The ordinal numbers. Formalized Mathematics, 1(1):91-96, 1990. 
  2. [2] Grzegorz Bancerek. Countable sets and Hessenberg's theorem. Formalized Mathematics, 2(1):65-69, 1991. 
  3. [3] Józef Białas and Yatsuka Nakamura. Dyadic numbers and T4 topological spaces. Formalized Mathematics, 5(3):361-366, 1996. 
  4. [4] Leszek Borys. Paracompact and metrizable spaces. Formalized Mathematics, 2(4):481-485, 1991. 
  5. [5] Czesław Byliński. Functions and their basic properties. Formalized Mathematics, 1(1):55-65, 1990. 
  6. [6] Czesław Byliński. Functions from a set to a set. Formalized Mathematics, 1(1):153-164, 1990. 
  7. [7] Czesław Byliński. Some basic properties of sets. Formalized Mathematics, 1(1):47-53, 1990. 
  8. [8] Agata Darmochwał. Compact spaces. Formalized Mathematics, 1(2):383-386, 1990. 
  9. [9] Agata Darmochwał. Families of subsets, subspaces and mappings in topological spaces. Formalized Mathematics, 1(2):257-261, 1990. 
  10. [10] Agata Darmochwał. Finite sets. Formalized Mathematics, 1(1):165-167, 1990. 
  11. [11] Agata Darmochwał and Yatsuka Nakamura. Metric spaces as topological spaces - fundamental concepts. Formalized Mathematics, 2(4):605-608, 1991. 
  12. [12] Alicia de la Cruz. Totally bounded metric spaces. Formalized Mathematics, 2(4):559-562, 1991. 
  13. [13] Ryszard Engelking. General Topology, volume 60 of Monografie Matematyczne. PWN - Polish Scientific Publishers, Warsaw, 1977. Zbl0373.54002
  14. [14] Adam Grabowski. On the Kuratowski limit operators. Formalized Mathematics, 11(4):399-409, 2003. 
  15. [15] Adam Grabowski. On the boundary and derivative of a set. Formalized Mathematics, 13(1):139-146, 2005. 
  16. [16] Krzysztof Hryniewiecki. Basic properties of real numbers. Formalized Mathematics, 1(1):35-40, 1990. 
  17. [17] Stanisława Kanas, Adam Lecko, and Mariusz Startek. Metric spaces. Formalized Mathematics, 1(3):607-610, 1990. 
  18. [18] Jarosław Kotowicz. Convergent sequences and the limit of sequences. Formalized Mathematics, 1(2):273-275, 1990. 
  19. [19] Jarosław Kotowicz. Monotone real sequences. Subsequences. Formalized Mathematics, 1(3):471-475, 1990. 
  20. [20] Jarosław Kotowicz. Real sequences and basic operations on them. Formalized Mathematics, 1(2):269-272, 1990. 
  21. [21] Robert Milewski. Bases of continuous lattices. Formalized Mathematics, 7(2):285-294, 1998. 
  22. [22] Beata Padlewska. Families of sets. Formalized Mathematics, 1(1):147-152, 1990. 
  23. [23] Beata Padlewska and Agata Darmochwał. Topological spaces and continuous functions. Formalized Mathematics, 1(1):223-230, 1990. 
  24. [24] Andrzej Trybulec. Domains and their Cartesian products. Formalized Mathematics, 1(1):115-122, 1990. 
  25. [25] Michał Trybulec. Formal languages - concatenation and closure. Formalized Mathematics, 15(1):11-15, 2007. 
  26. [26] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67-71, 1990. 
  27. [27] Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1(1):73-83, 1990. 
  28. [28] Edmund Woronowicz. Relations defined on sets. Formalized Mathematics, 1(1):181-186, 1990. 
  29. [29] Edmund Woronowicz and Anna Zalewska. Properties of binary relations. Formalized Mathematics, 1(1):85-89, 1990. 

NotesEmbed ?

top

You must be logged in to post comments.

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

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

                
Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.