On Nowhere and Everywhere Dense Subspaces of Topological Spaces

Journal of Formalized Mathematics
Volume 5, 1993
University of Bialystok
Copyright (c) 1993 Association of Mizar Users

On Nowhere and Everywhere Dense Subspaces of Topological Spaces

Zbigniew Karno: Warsaw University, Bialystok

Summary.

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.