Topological interpretation of rough sets. (English) Zbl 1298.54006

Summary: Rough sets, developed by Pawlak, are an important model of incomplete or partially known information. In this article, which is essentially a continuation of [A. Grabowski, “Basic properties of rough sets and rough membership function”, Formaliz. Math. 12, No. 1, 21–28 (2004)], 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 Y. Isomichi [Pac. J. Math. 38, 657–668 (1971; Zbl 0227.54001)] (formalized in Mizar in [M. Jastrzębska and A. Grabowski, “The properties of supercondensed sets, subcondensed sets and condensed sets”, Formaliz. Math. 13, No. 2, 353–359 (2005)]) and about fourteen sets of C. Kuratowski [Fundam. Math. 3, 182–199 (1922; JFM 48.0210.04)] (encoded with the help of Mizar adjectives and clusters’ registrations in [L. K. Bagińska and A. Grabowski, “On the Kuratowski closure-complement problem”, Formaliz. Math. 11, No. 3, 323–329 (2003)]) 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 [Z. Karno, “The lattice of domains of an extremally disconnected space”, Formaliz. Math. 3, No. 2, 143–149 (1992)], 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 [A. Grabowski, Fundam. Inform. 128, No. 1–2, 65–79 (2013; Zbl 1285.68180)].


54A40 Fuzzy topology
54H10 Topological representations of algebraic systems
68T37 Reasoning under uncertainty in the context of artificial intelligence
03B35 Mechanization of proofs and logical operations


Full Text: DOI


[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.; · 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.; · 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.;
[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.; · Zbl 0725.65053
[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.;
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.