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.
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]
-
Fourteen Kuratowski Sets
-
Seven Kuratowski Sets
-
The Set Generating Exactly Fourteen Kuratowski Sets
-
The Set Generating Exactly Seven Kuratowski Sets
-
The Difference Between Chosen Kuratowski Sets
-
Final Proofs For Seven Sets
-
Final Proofs For Fourteen Sets
-
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]