Journal of Formalized Mathematics
Volume 4, 1992
University of Bialystok
Copyright (c) 1992 Association of Mizar Users

## The Lattice of Domains of an Extremally Disconnected Space

Zbigniew Karno
Warsaw University, Bialystok

### Summary.

Let $X$ be a topological space and let $A$ be a subset of $X$. Recall that $A$ is said to be a {\em domain}\/ in $X$ provided ${\rm Int}\, \overline{A} \subseteq A \subseteq \overline{{\rm Int}\,A}$ (see , ). Recall also that $A$ is said to be a(n) {\em closed}\/ ({\em open})\/ {\em domain}\/ in $X$ if $A = \overline{{\rm Int}\,A}$ ($A = {\rm Int}\,\overline{A}$, resp.) (see e.g. , ). It is well-known that for a given topological space all its closed domains form a Boolean lattice, and similarly all its open domains form a Boolean lattice, too (see e.g., , ). In  it is proved that all domains of a given topological space form a complemented lattice. One may ask whether the lattice of all domains is Boolean. The aim is to give an answer to this question.\par To present the main results we first recall the definition of a class of topological spaces which is important here. $X$ is called {\em extremally disconnected}\/ if for every open subset $A$ of $X$ the closure $\overline {A}$ is open in $X$  (comp. ). It is shown here, using Mizar System, that {\em the lattice of all domains of a topological space $X$ is modular iff $X$ is extremally disconnected.} Moreover, for every extremally disconnected space the lattice of all its domains coincides with both the lattice of all its closed domains and the lattice of all its open domains. From these facts it follows that {\em the lattice of all domains of a topological space $X$ is Boolean iff $X$ is extremally disconnected.}\par Note that we also review some of the standard facts on discrete, anti-discrete, almost discrete, extremally disconnected and hereditarily extremally disconnected topological spaces (comp. , ).

{\it Editor's Note:} This work has won the 1992 \'Sleszy\'nski's Award of the Mizar Society.

#### MML Identifier: TDLAT_3

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

#### Contents (PDF format)

1. Selected Properties of Subsets of a Topological Space
2. Discrete Topological Structures
3. Discrete Topological Spaces
4. Extremally Disconnected Topological Spaces
5. The Lattice of Domains of Extremally Disconnected Spaces

#### Acknowledgments

The author wishes to thank to Professor A.~Trybulec for many helpful conversations during the preparation of this paper. The author is also very grateful to Cz.~Byli\'nski for acquainting him with new PC Mizar utilities programs.

#### Bibliography

 Grzegorz Bancerek. Complete lattices. Journal of Formalized Mathematics, 4, 1992.
 Garrett Birkhoff. \em Lattice Theory. Providence, Rhode Island, New York, 1967.
 Leszek Borys. Paracompact and metrizable spaces. Journal of Formalized Mathematics, 3, 1991.
 Czeslaw Bylinski. Binary operations. Journal of Formalized Mathematics, 1, 1989.
 Czeslaw Bylinski. Some basic properties of sets. Journal of Formalized Mathematics, 1, 1989.
 Ryszard Engelking. \em General Topology, volume 60 of \em Monografie Matematyczne. PWN - Polish Scientific Publishers, Warsaw, 1977.
 Yoshinori Isomichi. New concepts in the theory of topological space -- supercondensed set, subcondensed set, and condensed set. \em Pacific Journal of Mathematics, 38(3):657--668, 1971.
 Zbigniew Karno and Toshihiko Watanabe. Completeness of the lattices of domains of a topological space. Journal of Formalized Mathematics, 4, 1992.
 Kazimierz Kuratowski. \em Topology, volume I. PWN - Polish Scientific Publishers, Academic Press, Warsaw, New York and London, 1966.
 Kazimierz Kuratowski and Andrzej Mostowski. \em Set Theory (with an introduction to descriptive set theory), volume 86 of \em Studies in Logic and The Foundations of Mathematics. PWN - Polish Scientific Publishers and North-Holland Publishing Company, Warsaw-Amsterdam, 1976.
 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. Algebraic characterizations of special Boolean rings. \em Fundamenta Mathematicae, 29:223--303, 1937.
 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.
 Toshihiko Watanabe. The lattice of domains of a topological space. Journal of Formalized Mathematics, 4, 1992.
 Edmund Woronowicz. Relations and their basic properties. Journal of Formalized Mathematics, 1, 1989.
 Miroslaw Wysocki and Agata Darmochwal. Subsets of topological spaces. Journal of Formalized Mathematics, 1, 1989.
 Stanislaw Zukowski. Introduction to lattice theory. Journal of Formalized Mathematics, 1, 1989.