Journal of Formalized Mathematics
Volume 1, 1989
University of Bialystok
Copyright (c) 1989 Association of Mizar Users

Subsets of Topological Spaces

Miroslaw Wysocki
Warsaw University, Bialystok
Agata Darmochwal
Warsaw University, Bialystok


The article contains some theorems about open and closed sets. The following topological operations on sets are defined: closure, interior and frontier. The following notions are introduced: dense set, boundary set, nowheredense set and set being domain (closed domain and open domain), and some basic facts concerning them are proved.

Supported by RPBP.III-24.C1.

MML Identifier: TOPS_1

The terminology and notation used in this paper have been introduced in the following articles [2] [3] [1]

Contents (PDF format)


[1] Beata Padlewska and Agata Darmochwal. Topological spaces and continuous functions. Journal of Formalized Mathematics, 1, 1989.
[2] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.
[3] Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.

Received April 28, 1989

[ Download a postscript version, MML identifier index, Mizar home page]