<abstract xml:lang="en" xmlns="http://www.w3.org/1999/xhtml"><p>We continue Mizar formalization of general topology according to the book [11] by Engelking. In the article, we present the final theorem of Section 4.1. Namely, the paper includes the formalization of theorems on the correspondence between the cardinalities of the basis and of some open subcover, and a discreet (closed) subspaces, and the weight of that metrizable topological space. We also define Lindelöf spaces and state the above theorem in this special case. We also introduce the concept of separation among two subsets (see [12]).</p></abstract>

We continue Mizar formalization of general topology according to the book [11] by Engelking. In the article, we present the final theorem of Section 4.1. Namely, the paper includes the formalization of theorems on the correspondence between the cardinalities of the basis and of some open subcover, and a discreet (closed) subspaces, and the weight of that metrizable topological space. We also define Lindelöf spaces and state the above theorem in this special case. We also introduce the concept of separation among two subsets (see [12]).

Basic Properties of Metrizable Topological Spaces

Institute of Computer Science, University of Białystok, Poland

Formalized Mathematics

{"article-title":"Basic Properties of Metrizable Topological Spaces"}

We continue Mizar formalization of general topology according to the book [11] by Engelking. In the article, we present the final theorem of Section 4.1....

Basic Properties of Metrizable Topological Spaces

Publié en ligne: 08 juil. 2010

Pages: 201 - 205

DOI: https://doi.org/10.2478/v10037-009-0024-8

This content is open access.