REPOZYTORIUM UNIWERSYTETU
W BIAŁYMSTOKU
UwB

Proszę używać tego identyfikatora do cytowań lub wstaw link do tej pozycji: http://hdl.handle.net/11320/5551
Tytuł: Compactness in Metric Spaces
Autorzy: Nakasho, Kazuhisa
Narita, Keiko
Shidama, Yasunari
Słowa kluczowe: metric spaces
normed linear spaces
compactness
Data wydania: 2016
Data dodania: 2-cze-2017
Wydawca: De Gruyter Open
Źródło: Formalized Mathematics, Volume 24, Issue 3, pp. 167-172
Abstrakt: 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].
Afiliacja: Nakasho Kazuhisa - Shinshu University Nagano, Japan
Narita Keiko - Hirosaki-city Aomori, Japan
Shidama Yasunari - Shinshu University Nagano, Japan
URI: http://hdl.handle.net/11320/5551
DOI: 10.1515/forma-2016-0013
ISSN: 1426-2630
1898-9934
Typ Dokumentu: Article
Występuje w kolekcji(ach):Formalized Mathematics, 2016, Volume 24, Issue 3

Pliki w tej pozycji:
Plik Opis RozmiarFormat 
forma-2016-0013.pdf228,56 kBAdobe PDFOtwórz
Pokaż pełny widok rekordu Zobacz statystyki


Pozycja ta dostępna jest na podstawie licencji Licencja Creative Commons CCL Creative Commons