Volume 5, 1993

University of Bialystok

Copyright (c) 1993 Association of Mizar Users

**Zbigniew Karno**- Warsaw University, Bialystok

- Let $X$ be a topological space and let $X_{0}$ be a subspace of $X$ with the carrier $A$. $X_{0}$ is called {\em boundary}\/ ({\em dense}) in $X$ if $A$ is boundary (dense), i.e., ${\rm Int}\,A = \emptyset$ ($\overline{A} =$ the carrier of $X$); $X_{0}$ is called {\em nowhere dense}\/ ({\em everywhere dense}) in $X$ if $A$ is nowhere dense (everywhere dense), i.e., ${\rm Int}\,\overline{A} = \emptyset$ ($\overline{{\rm Int}\,A} =$ the carrier of $X$) (see [6] and comp. [7]).\par Our purpose is to list, using Mizar formalism, a number of properties of such subspaces, mostly in non-discrete (non-almost-discrete) spaces (comp. [6]). Recall that $X$ is called {\em discrete}\/ if every subset of $X$ is open (closed); $X$ is called {\em almost discrete}\/ if every open subset of $X$ is closed; equivalently, if every closed subset of $X$ is open (see [1], [5] and comp. [7],[8]). We have the following characterization of non-discrete spaces: {\em $X$ is non-discrete iff there exists a boundary subspace in $X$}. Hence, {\em $X$ is non-discrete iff there exists a dense proper subspace in $X$}. We have the following analogous characterization of non-almost-discrete spaces: {\em $X$ is non-almost-discrete iff there exists a nowhere dense subspace in $X$}. Hence, {\em $X$ is non-almost-discrete iff there exists an everywhere dense proper subspace in $X$}.\par Note that some interdependencies between boundary, dense, nowhere and everywhere dense subspaces are also indicated. These have the form of observations in the text and they correspond to the existential and to the conditional clusters in the Mizar System. These clusters guarantee the existence and ensure the extension of types supported automatically by the Mizar System.

- Some Properties of Subsets of a Topological Space
- Dense and Everywhere Dense Subspaces
- Boundary and Nowhere Dense Subspaces
- Dense and Boundary Subspaces of Non-discrete Spaces
- Everywhere and Nowhere Dense Subspaces of Non-almost-discrete Spaces

- [1]
Zbigniew Karno.
The lattice of domains of an extremally disconnected space.
*Journal of Formalized Mathematics*, 4, 1992. - [2]
Zbigniew Karno.
On a duality between weakly separated subspaces of topological spaces.
*Journal of Formalized Mathematics*, 4, 1992. - [3]
Zbigniew Karno.
Separated and weakly separated subspaces of topological spaces.
*Journal of Formalized Mathematics*, 4, 1992. - [4]
Zbigniew Karno.
Maximal discrete subspaces of almost discrete topological spaces.
*Journal of Formalized Mathematics*, 5, 1993. - [5]
Zbigniew Karno.
On discrete and almost discrete topological spaces.
*Journal of Formalized Mathematics*, 5, 1993. - [6]
Zbigniew Karno.
Remarks on special subsets of topological spaces.
*Journal of Formalized Mathematics*, 5, 1993. - [7] Kazimierz Kuratowski. \em Topology, volume I. PWN - Polish Scientific Publishers, Academic Press, Warsaw, New York and London, 1966.
- [8] Kazimierz Kuratowski. \em Topology, volume II. PWN - Polish Scientific Publishers, Academic Press, Warsaw, New York and London, 1968.
- [9]
Beata Padlewska and Agata Darmochwal.
Topological spaces and continuous functions.
*Journal of Formalized Mathematics*, 1, 1989. - [10]
Andrzej Trybulec.
Tarski Grothendieck set theory.
*Journal of Formalized Mathematics*, Axiomatics, 1989. - [11]
Andrzej Trybulec.
A Borsuk theorem on homotopy types.
*Journal of Formalized Mathematics*, 3, 1991. - [12]
Zinaida Trybulec.
Properties of subsets.
*Journal of Formalized Mathematics*, 1, 1989. - [13]
Miroslaw Wysocki and Agata Darmochwal.
Subsets of topological spaces.
*Journal of Formalized Mathematics*, 1, 1989.

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