Volume 6, 1994

University of Bialystok

Copyright (c) 1994 Association of Mizar Users

**Zbigniew Karno**- Warsaw University, Bialystok

- 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 [8].\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., [5]), 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$.

- Properties of the Closure and the Interior Operations
- Anti-Discrete Subsets of Topological Structures
- Maximal Anti-Discrete Subsets of Topological Structures
- Anti-Discrete and Maximal Anti-discrete Subsets of Topological Spaces
- Maximal Anti-Discrete Subspaces

- [1]
Czeslaw Bylinski.
Some basic properties of sets.
*Journal of Formalized Mathematics*, 1, 1989. - [2]
Zbigniew Karno.
The lattice of domains of an extremally disconnected space.
*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] Kazimierz Kuratowski. \em Topology, volume I. PWN - Polish Scientific Publishers, Academic Press, Warsaw, New York and London, 1966.
- [6]
Beata Padlewska.
Families of sets.
*Journal of Formalized Mathematics*, 1, 1989. - [7]
Beata Padlewska and Agata Darmochwal.
Topological spaces and continuous functions.
*Journal of Formalized Mathematics*, 1, 1989. - [8] M. H. Stone. Application of Boolean algebras to topology. \em Math. Sb., 1:765--771, 1936.
- [9]
Andrzej Trybulec.
Tarski Grothendieck set theory.
*Journal of Formalized Mathematics*, Axiomatics, 1989. - [10]
Andrzej Trybulec.
A Borsuk theorem on homotopy types.
*Journal of Formalized Mathematics*, 3, 1991. - [11]
Zinaida Trybulec.
Properties of subsets.
*Journal of Formalized Mathematics*, 1, 1989. - [12]
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]