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 $D$ be a subset of $X$. $D$ is said to be {\em discrete}\/ provided for every subset $A$ of $X$ such that $A \subseteq D$ there is an open subset $G$ of $X$ such that $A = D \cap G$\/ (comp. e.g., [9]). A discrete subset $M$ of $X$ is said to be {\em maximal discrete}\/ provided for every discrete subset $D$ of $X$ if $M \subseteq D$ then $M = D$. A subspace of $X$ is {\em discrete}\/ ({\em maximal discrete}) iff its carrier is discrete (maximal discrete) in $X$.\par Our purpose is to list a number of properties of discrete and maximal discrete sets in Mizar formalism. In particular, we show here that {\em if $D$ is dense and discrete then $D$ is maximal discrete}; moreover, {\em if $D$ is open and maximal discrete then $D$ is dense}. We discuss also the problem of the existence of maximal discrete subsets in a topological space.\par To present the main results we first recall a definition of a class of topological spaces considered herein. A topological space $X$ is called {\em almost discrete}\/ if every open subset of $X$ is closed; equivalently, if every closed subset of $X$ is open. Such spaces were investigated in Mizar formalism in [6] and [7]. We show here that {\em every almost discrete space contains a maximal discrete subspace and every such subspace is a retract of the enveloping space}. Moreover, {\em if $X_{0}$ is a maximal discrete subspace of an almost discrete space $X$ and $r : X \rightarrow X_{0}$ is a continuous retraction, then $r^{-1}(x) = \overline{\{x\}}$ for every point $x$ of $X$ belonging to $X_{0}$}. This fact is a specialization, in the case of almost discrete spaces, of the theorem of M.H. Stone that every topological space can be made into a $T_{0}$-space by suitable identification of points (see [11]).

- Proper Subsets of 1-sorted Structures
- Proper Subspaces of Topological Spaces
- Maximal Discrete Subsets and Subspaces
- Maximal Discrete Subspaces of Almost Discrete Spaces
- Continuous Mappings and Almost Discrete Spaces

- [1]
Jozef Bialas.
Group and field definitions.
*Journal of Formalized Mathematics*, 1, 1989. - [2]
Leszek Borys.
Paracompact and metrizable spaces.
*Journal of Formalized Mathematics*, 3, 1991. - [3]
Czeslaw Bylinski.
Functions and their basic properties.
*Journal of Formalized Mathematics*, 1, 1989. - [4]
Czeslaw Bylinski.
Functions from a set to a set.
*Journal of Formalized Mathematics*, 1, 1989. - [5]
Czeslaw Bylinski.
Partial functions.
*Journal of Formalized Mathematics*, 1, 1989. - [6]
Zbigniew Karno.
The lattice of domains of an extremally disconnected space.
*Journal of Formalized Mathematics*, 4, 1992. - [7]
Zbigniew Karno.
On discrete and almost discrete topological spaces.
*Journal of Formalized Mathematics*, 5, 1993. - [8]
Zbigniew Karno.
Remarks on special subsets of topological spaces.
*Journal of Formalized Mathematics*, 5, 1993. - [9] Kazimierz Kuratowski. \em Topology, volume I. PWN - Polish Scientific Publishers, Academic Press, Warsaw, New York and London, 1966.
- [10]
Beata Padlewska and Agata Darmochwal.
Topological spaces and continuous functions.
*Journal of Formalized Mathematics*, 1, 1989. - [11] M. H. Stone. Application of Boolean algebras to topology. \em Math. Sb., 1:765--771, 1936.
- [12]
Andrzej Trybulec.
Domains and their Cartesian products.
*Journal of Formalized Mathematics*, 1, 1989. - [13]
Andrzej Trybulec.
Tarski Grothendieck set theory.
*Journal of Formalized Mathematics*, Axiomatics, 1989. - [14]
Andrzej Trybulec.
A Borsuk theorem on homotopy types.
*Journal of Formalized Mathematics*, 3, 1991. - [15]
Zinaida Trybulec.
Properties of subsets.
*Journal of Formalized Mathematics*, 1, 1989. - [16]
Edmund Woronowicz.
Relations and their basic properties.
*Journal of Formalized Mathematics*, 1, 1989. - [17]
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]