Rough sets, developed by Pawlak, are an important model of incomplete or partially known information. In this article, which is essentially a continuation of [11], we characterize rough sets in terms of topological closure and interior, as the approximations have the properties of the Kuratowski operators. We decided to merge topological spaces with tolerance approximation spaces. As a testbed for our developed approach, we restated the results of Isomichi [13] (formalized in Mizar in [14]) and about fourteen sets of Kuratowski [17] (encoded with the help of Mizar adjectives and clusters’ registrations in [1]) in terms of rough approximations. The upper bounds which were 14 and 7 in the original paper of Kuratowski, in our case are six and three, respectively. It turns out that within the classification given by Isomichi, 1st class subsets are precisely crisp sets, 2nd class subsets are proper rough sets, and there are no 3rd class subsets in topological spaces generated by approximations. Also the important results about these spaces is that they are extremally disconnected [15], hence lattices of their domains are Boolean. Furthermore, we develop the theory of abstract spaces equipped with maps possessing characteristic properties of rough approximations which enables us to freely use the notions from the theory of rough sets and topological spaces formalized in the Mizar Mathematical Library [10].
@article{bwmeta1.element.doi-10_2478_forma-2014-0010,
author = {Adam Grabowski},
title = {Topological Interpretation of Rough Sets},
journal = {Formalized Mathematics},
volume = {22},
year = {2014},
pages = {89-97},
zbl = {1298.54006},
language = {en},
url = {http://dml.mathdoc.fr/item/bwmeta1.element.doi-10_2478_forma-2014-0010}
}
Adam Grabowski. Topological Interpretation of Rough Sets. Formalized Mathematics, Tome 22 (2014) pp. 89-97. http://gdmltest.u-ga.fr/item/bwmeta1.element.doi-10_2478_forma-2014-0010/
[1] Lilla Krystyna Baginska and Adam Grabowski. On the Kuratowski closure-complement problem. Formalized Mathematics, 11(3):323-329, 2003.
[2] Grzegorz Bancerek. Cardinal numbers. Formalized Mathematics, 1(2):377-382, 1990.
[3] Grzegorz Bancerek. The ordinal numbers. Formalized Mathematics, 1(1):91-96, 1990.
[4] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Formalized Mathematics, 1(1):107-114, 1990.
[5] Czesław Bylinski. Functions and their basic properties. Formalized Mathematics, 1(1): 55-65, 1990.
[6] Czesław Bylinski. Functions from a set to a set. Formalized Mathematics, 1(1):153-164, 1990.
[7] Czesław Bylinski. Partial functions. Formalized Mathematics, 1(2):357-367, 1990.
[8] Czesław Bylinski. Some basic properties of sets. Formalized Mathematics, 1(1):47-53, 1990.
[9] Agata Darmochwał. Finite sets. Formalized Mathematics, 1(1):165-167, 1990.
[10] Adam Grabowski. Automated discovery of properties of rough sets. Fundamenta Informaticae, 128:65-79, 2013. doi:10.3233/FI-2013-933.[Crossref][WoS] | Zbl 1285.68180
[11] Adam Grabowski. Basic properties of rough sets and rough membership function. Formalized Mathematics, 12(1):21-28, 2004.
[12] Adam Grabowski. Relational formal characterization of rough sets. Formalized Mathematics, 21(1):55-64, 2013. doi:10.2478/forma-2013-0006.[Crossref] | Zbl 1286.68428
[13] Yoshinori Isomichi. New concepts in the theory of topological space - supercondensed set, subcondensed set, and condensed set. Pacific Journal of Mathematics, 38(3):657-668, 1971. | Zbl 0227.54001
[14] Magdalena Jastrz¸ebska and Adam Grabowski. The properties of supercondensed sets, subcondensed sets and condensed sets. Formalized Mathematics, 13(2):353-359, 2005.
[15] Zbigniew Karno. The lattice of domains of an extremally disconnected space. Formalized Mathematics, 3(2):143-149, 1992.
[16] Artur Korniłowicz. On the topological properties of meet-continuous lattices. Formalized Mathematics, 6(2):269-277, 1997.
[17] Kazimierz Kuratowski. Sur l’opération A de l’analysis situs. Fundamenta Mathematicae, 3:182-199, 1922. | Zbl 48.0210.04
[18] Beata Padlewska. Families of sets. Formalized Mathematics, 1(1):147-152, 1990.
[19] Beata Padlewska and Agata Darmochwał. Topological spaces and continuous functions. Formalized Mathematics, 1(1):223-230, 1990.
[20] Bartłomiej Skorulski. First-countable, sequential, and Frechet spaces. Formalized Mathematics, 7(1):81-86, 1998.
[21] Bartłomiej Skorulski. The sequential closure operator in sequential and Frechet spaces. Formalized Mathematics, 8(1):47-54, 1999.
[22] Andrzej Trybulec. Enumerated sets. Formalized Mathematics, 1(1):25-34, 1990.
[23] Andrzej Trybulec. Function domains and Frænkel operator. Formalized Mathematics, 1 (3):495-500, 1990.
[24] Andrzej Trybulec and Agata Darmochwał. Boolean domains. Formalized Mathematics, 1 (1):187-190, 1990.
[25] Wojciech A. Trybulec and Grzegorz Bancerek. Kuratowski - Zorn lemma. Formalized Mathematics, 1(2):387-393, 1990.
[26] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67-71, 1990.
[27] Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1 (1):73-83, 1990.
[28] Mirosław Wysocki and Agata Darmochwał. Subsets of topological spaces. Formalized Mathematics, 1(1):231-237, 1990.