PL EN


Preferencje help
Widoczny [Schowaj] Abstrakt
Liczba wyników
2016 | 24 | 3 | 167-172
Tytuł artykułu

Compactness in Metric Spaces

Treść / Zawartość
Warianty tytułu
Języki publikacji
EN
Abstrakty
EN
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].
Słowa kluczowe
Wydawca
Rocznik
Tom
24
Numer
3
Strony
167-172
Opis fizyczny
Daty
wydano
2016-09-01
otrzymano
2016-06-30
online
2017-02-08
Twórcy
  • Shinshu University Nagano,
autor
  • Hirosaki-city Aomori,
  • Shinshu University Nagano,
Bibliografia
Typ dokumentu
Bibliografia
Identyfikatory
Identyfikator YADDA
bwmeta1.element.doi-10_1515_forma-2016-0013
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.