Journal of Formalized Mathematics
Volume 15, 2003
University of Bialystok
Copyright (c) 2003 Association of Mizar Users

On the Kuratowski Closure-Complement Problem


Lilla Krystyna Baginska
University of Bialystok
Adam Grabowski
University of Bialystok
This work has been partially supported by CALCULEMUS grant HPRN-CT-2000-00102.

Summary.

In this article we formalize the Kuratowski closure-complement result: there is at most 14 distinct sets that one can produce from a given subset $A$ of a topological space $T$ by applying closure and complement operators and that all 14 can be obtained from a suitable subset of $\Bbb R,$ namely KuratExSet $=\{1\} \cup {\Bbb Q} (2,3) \cup (3, 4)\cup (4,\infty)$.\par The second part of the article deals with the maximal number of distinct sets which may be obtained from a given subset $A$ of $T$ by applying closure and interior operators. The subset KuratExSet of $\Bbb R$ is also enough to show that 7 can be achieved.

MML Identifier: KURATO_1

The terminology and notation used in this paper have been introduced in the following articles [13] [15] [14] [10] [16] [12] [1] [3] [11] [7] [6] [8] [2] [4] [9] [5]

Contents (PDF format)

  1. Fourteen Kuratowski Sets
  2. Seven Kuratowski Sets
  3. The Set Generating Exactly Fourteen Kuratowski Sets
  4. The Set Generating Exactly Seven Kuratowski Sets
  5. The Difference Between Chosen Kuratowski Sets
  6. Final Proofs For Seven Sets
  7. Final Proofs For Fourteen Sets
  8. Properties of Kuratowski Sets

Bibliography

[1] Grzegorz Bancerek. Cardinal numbers. Journal of Formalized Mathematics, 1, 1989.
[2] Leszek Borys. Paracompact and metrizable spaces. Journal of Formalized Mathematics, 3, 1991.
[3] Agata Darmochwal. Finite sets. Journal of Formalized Mathematics, 1, 1989.
[4] Agata Darmochwal and Yatsuka Nakamura. Metric spaces as topological spaces --- fundamental concepts. Journal of Formalized Mathematics, 3, 1991.
[5] Adam Grabowski. On the subcontinua of a real line. Journal of Formalized Mathematics, 15, 2003.
[6] Jaroslaw Kotowicz. Convergent real sequences. Upper and lower bound of sets of real numbers. Journal of Formalized Mathematics, 1, 1989.
[7] Wojciech Leonczuk and Krzysztof Prazmowski. Incidence projective spaces. Journal of Formalized Mathematics, 2, 1990.
[8] Yatsuka Nakamura. Half open intervals in real numbers. Journal of Formalized Mathematics, 14, 2002.
[9] Yatsuka Nakamura and Andrzej Trybulec. A mathematical model of CPU. Journal of Formalized Mathematics, 4, 1992.
[10] Beata Padlewska and Agata Darmochwal. Topological spaces and continuous functions. Journal of Formalized Mathematics, 1, 1989.
[11] Konrad Raczkowski and Pawel Sadowski. Topological properties of subsets in real numbers. Journal of Formalized Mathematics, 2, 1990.
[12] Andrzej Trybulec. Enumerated sets. Journal of Formalized Mathematics, 1, 1989.
[13] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.
[14] Andrzej Trybulec. Subsets of real numbers. Journal of Formalized Mathematics, Addenda, 2003.
[15] Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.
[16] Miroslaw Wysocki and Agata Darmochwal. Subsets of topological spaces. Journal of Formalized Mathematics, 1, 1989.

Received June 12, 2003


[ Download a postscript version, MML identifier index, Mizar home page]