Journal of Formalized Mathematics
Volume 6, 1994
University of Bialystok
Copyright (c) 1994 Association of Mizar Users

Maximal Anti-Discrete Subspaces of Topological Spaces

Zbigniew Karno
Warsaw University, Bialystok

Summary.

Let $X$ be a topological space and let $A$ be a subset of $X$. $A$ is said to be {\em anti-discrete}\/ provided for every open subset $G$ of $X$ either $A \cap G = \emptyset$ or $A \subseteq G$; equivalently, for every closed subset $F$ of $X$ either $A \cap F = \emptyset$ or $A \subseteq F$. An anti-discrete subset $M$ of $X$ is said to be {\em maximal anti-discrete}\/ provided for every anti-discrete subset $A$ of $X$ if $M \subseteq A$ then $M = A$. A subspace of $X$ is {\em maximal anti-discrete}\/ iff its carrier is maximal anti-discrete in $X$. The purpose is to list a few properties of maximal anti-discrete sets and subspaces in Mizar formalism.\par It is shown that every $x \in X$ is contained in a unique maximal anti-discrete subset M$(x)$ of $X$, denoted in the text by MaxADSet($x$). Such subset can be defined by $${\rm M}(x) = \bigcap\ \{ S \subseteq X : x \in S,\ {\rm and}\ S \ {\rm is}\ {\rm open}\ {\rm or}\ {\rm closed}\ {\rm in}\ X\}.$$ It has the following remarkable properties: (1) $y \in {\rm M}(x)$ iff ${\rm M}(y) = {\rm M}(x)$, (2) either ${\rm M}(x) \cap {\rm M}(y) = \emptyset$ or ${\rm M}(x) = {\rm M}(y)$, (3) ${\rm M}(x) = {\rm M}(y)$ iff $\overline{\{x\}} = \overline{\{y\}}$, and (4) ${\rm M}(x) \cap {\rm M}(y) = \emptyset$ iff $\overline{\{x\}} \neq \overline{\{y\}}$. It follows from these properties that $\{{\rm M}(x) : x \in X\}$ is the $T_{0}$-partition of $X$ defined by M.H.~Stone in .\par Moreover, it is shown that the operation M defined on all subsets of $X$ by $${\rm M}(A) = \bigcup\ \{{\rm M}(x) : x \in A\},$$ denoted in the text by MaxADSet($A$), satisfies the Kuratowski closure axioms (see e.g., ), i.e., (1) ${\rm M}(A \cup B) = {\rm M}(A) \cup {\rm M}(B)$, (2) ${\rm M}(A) = {\rm M}({\rm M}(A))$, (3) $A \subseteq {\rm M}(A)$,and (4) ${\rm M}(\emptyset) = \emptyset$. Note that this operation commutes with the usual closure operation of $X$, and if $A$ is an open (or a closed) subset of $X$, then ${\rm M}(A) = A$.

MML Identifier: TEX_4

The terminology and notation used in this paper have been introduced in the following articles          

Contents (PDF format)

1. Properties of the Closure and the Interior Operations
2. Anti-Discrete Subsets of Topological Structures
3. Maximal Anti-Discrete Subsets of Topological Structures
4. Anti-Discrete and Maximal Anti-discrete Subsets of Topological Spaces
5. Maximal Anti-Discrete Subspaces

Bibliography

 Czeslaw Bylinski. Some basic properties of sets. Journal of Formalized Mathematics, 1, 1989.
 Zbigniew Karno. The lattice of domains of an extremally disconnected space. Journal of Formalized Mathematics, 4, 1992.
 Zbigniew Karno. Separated and weakly separated subspaces of topological spaces. Journal of Formalized Mathematics, 4, 1992.
 Zbigniew Karno. Maximal discrete subspaces of almost discrete topological spaces. Journal of Formalized Mathematics, 5, 1993.
 Kazimierz Kuratowski. \em Topology, volume I. PWN - Polish Scientific Publishers, Academic Press, Warsaw, New York and London, 1966.
 Beata Padlewska. Families of sets. Journal of Formalized Mathematics, 1, 1989.
 Beata Padlewska and Agata Darmochwal. Topological spaces and continuous functions. Journal of Formalized Mathematics, 1, 1989.
 M. H. Stone. Application of Boolean algebras to topology. \em Math. Sb., 1:765--771, 1936.
 Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.
 Andrzej Trybulec. A Borsuk theorem on homotopy types. Journal of Formalized Mathematics, 3, 1991.
 Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.
 Miroslaw Wysocki and Agata Darmochwal. Subsets of topological spaces. Journal of Formalized Mathematics, 1, 1989.