:: Relational Formal Characterization of Rough Sets :: by Adam Grabowski :: :: Received January 17, 2013 :: Copyright (c) 2013-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies STRUCT_0, ORDERS_2, RELAT_1, TARSKI, ZFMISC_1, PRE_TOPC, RELAT_2, XBOOLE_0, PARTFUN1, SUBSET_1, TOPS_1, FUNCT_1, FINSET_1, EQREL_1, XXREAL_0, ROUGHS_1, RCOMP_1, ROUGHS_2; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FINSET_1, RELAT_1, RELAT_2, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, DOMAIN_1, STRUCT_0, ORDERS_2, EQREL_1, PRE_TOPC, TOPS_1, ROUGHS_1, YELLOW_3; constructors EQREL_1, REALSET2, RELSET_1, ROUGHS_1, YELLOW_3, TOPS_1; registrations XBOOLE_0, SUBSET_1, RELAT_1, FINSET_1, NAT_1, STRUCT_0, ORDERS_2, RELSET_1, FUNCT_1, FUNCT_2, YELLOW_3, TOPS_1, PRE_TOPC; requirements BOOLE, SUBSET, NUMERALS; begin :: Preliminaries registration cluster non empty void for RelStr; end; theorem :: ROUGHS_2:1 for R being total non empty RelStr, x being Element of R holds x in field the InternalRel of R; theorem :: ROUGHS_2:2 for R being non empty 1-sorted, X being Subset of R holds { x where x is Element of R : {} c= X } = [#]R; theorem :: ROUGHS_2:3 for R being 1-sorted, X being Subset of R holds { x where x is Element of R : {} meets X } = {}R; begin :: Missing Ordinary Properties of Binary Relations definition let R be Relation, X be set; pred R is_serial_in X means :: ROUGHS_2:def 1 for x being object st x in X holds ex y being object st y in X & [x,y] in R; end; definition let R be Relation; attr R is serial means :: ROUGHS_2:def 2 R is_serial_in field R; end; definition let R be RelStr; attr R is serial means :: ROUGHS_2:def 3 the InternalRel of R is_serial_in the carrier of R; end; registration cluster reflexive -> serial for RelStr; end; definition let R be non empty RelStr; redefine attr R is serial means :: ROUGHS_2:def 4 for x being Element of R ex y being Element of R st x <= y; end; registration cluster total -> serial for RelStr; cluster serial -> total for RelStr; end; registration let R be non empty serial RelStr, x be Element of R; cluster Class (the InternalRel of R,x) -> non empty; end; :: Reflexive relations theorem :: ROUGHS_2:4 for R being non empty reflexive RelStr, x being Element of R holds x in Class (the InternalRel of R,x); registration let R be non empty reflexive RelStr, x be Element of R; cluster Class (the InternalRel of R,x) -> non empty; end; :: Mediate relations definition let R be Relation, X be set; pred R is_mediate_in X means :: ROUGHS_2:def 5 for x,y being object st x in X & y in X holds [x,y] in R implies ex z being object st z in X & [x,z] in R & [z,y] in R; end; definition let R be Relation; attr R is mediate means :: ROUGHS_2:def 6 R is_mediate_in field R; end; definition let R be RelStr; attr R is mediate means :: ROUGHS_2:def 7 the InternalRel of R is_mediate_in the carrier of R; end; registration cluster reflexive -> mediate for RelStr; end; begin :: Approximations Revisited theorem :: ROUGHS_2:5 for R being non empty RelStr, a, b being Element of R st a in UAp ({b}) holds [a,b] in the InternalRel of R; definition let R be non empty RelStr; let X be Subset of R; func Uap X -> Subset of R equals :: ROUGHS_2:def 8 (LAp X`)`; end; definition let R be non empty RelStr; let X be Subset of R; func Lap X -> Subset of R equals :: ROUGHS_2:def 9 (UAp X`)`; end; theorem :: ROUGHS_2:6 for R being non empty RelStr, X being Subset of R for x being object st x in LAp X holds Class (the InternalRel of R, x) c= X; theorem :: ROUGHS_2:7 for R being non empty RelStr, X being Subset of R for x being set st x in UAp X holds Class (the InternalRel of R, x) meets X; theorem :: ROUGHS_2:8 for R being non empty RelStr, X being Subset of R holds Uap X = UAp X; theorem :: ROUGHS_2:9 for R being non empty RelStr, X being Subset of R holds Lap X = LAp X; theorem :: ROUGHS_2:10 :: Example 2 for R being non empty void RelStr, X being Subset of R holds LAp X = [#]R; theorem :: ROUGHS_2:11 :: Example 2 for R being non empty void RelStr, X being Subset of R holds UAp X = {}R; begin :: General Properties of Approximations registration let R be non empty RelStr; reduce LAp ([#]R) to [#]R; end; registration let R be non empty serial RelStr; reduce UAp ([#]R) to [#]R; end; registration let R be non empty serial RelStr; reduce LAp {}R to {}R; end; registration let R be non empty RelStr; reduce UAp ({}R) to {}R; end; theorem :: ROUGHS_2:12 :: Proposition 2 4L for R being non empty RelStr, X, Y being Subset of R holds LAp (X /\ Y) = LAp (X) /\ LAp (Y); theorem :: ROUGHS_2:13 :: Proposition 2 4H for R being non empty RelStr, X, Y being Subset of R holds UAp (X \/ Y) = UAp X \/ UAp Y; theorem :: ROUGHS_2:14 :: Proposition 2 6L for R being non empty RelStr, X, Y being Subset of R st X c= Y holds LAp X c= LAp Y; theorem :: ROUGHS_2:15 :: Proposition 2 6H for R being non empty RelStr, X, Y being Subset of R st X c= Y holds UAp X c= UAp Y; theorem :: ROUGHS_2:16 :: Proposition 2 8LH for R being non empty RelStr, X being Subset of R holds LAp (X`) = (UAp X)`; theorem :: ROUGHS_2:17 :: Proposition 2 9LH for R being non empty serial RelStr, X being Subset of R holds LAp X c= UAp X; begin :: Auxiliary Operation on Approximation Operators definition let R be non empty RelStr; func LAp R -> Function of bool the carrier of R, bool the carrier of R means :: ROUGHS_2:def 10 for X being Subset of R holds it.X = LAp X; func UAp R -> Function of bool the carrier of R, bool the carrier of R means :: ROUGHS_2:def 11 for X being Subset of R holds it.X = UAp X; end; definition let f be Function; attr f is empty-preserving means :: ROUGHS_2:def 12 f.{} = {}; end; definition let A be set; let f be Function of bool A, bool A; attr f is universe-preserving means :: ROUGHS_2:def 13 f.A = A; end; registration let A be non empty set; cluster id bool A -> empty-preserving universe-preserving for Function of bool A, bool A; end; registration let A be non empty set; cluster empty-preserving universe-preserving for Function of bool A, bool A; end; definition let X be set; let f be Function of bool X, bool X; func Flip f -> Function of bool X, bool X means :: ROUGHS_2:def 14 for x being Subset of X holds it.x = (f.x`)`; end; theorem :: ROUGHS_2:18 for X being set, f being Function of bool X, bool X st f.{} = {} holds (Flip f).X = X; theorem :: ROUGHS_2:19 for X being set, f being Function of bool X, bool X st f.X = X holds (Flip f).{} = {}; theorem :: ROUGHS_2:20 for X being set, f being Function of bool X, bool X st f = id bool X holds Flip f = f; theorem :: ROUGHS_2:21 for X being set, f being Function of bool X, bool X st for A, B being Subset of X holds f.(A \/ B) = f.A \/ f.B holds for A, B being Subset of X holds (Flip f).(A /\ B) = (Flip f).A /\ (Flip f).B; theorem :: ROUGHS_2:22 for X being set, f being Function of bool X, bool X st for A, B being Subset of X holds f.(A /\ B) = f.A /\ f.B holds for A, B being Subset of X holds (Flip f).(A \/ B) = (Flip f).A \/ (Flip f).B; theorem :: ROUGHS_2:23 for X being set, f being Function of bool X, bool X holds Flip Flip f = f; registration let A be non empty set; let f be universe-preserving Function of bool A, bool A; cluster Flip f -> empty-preserving; end; registration let A be non empty set; let f be empty-preserving Function of bool A, bool A; cluster Flip f -> universe-preserving; end; theorem :: ROUGHS_2:24 for A being non empty set, L, U being Function of bool A, bool A st U = Flip L & for X being Subset of A holds L.(L.X) c= L.X holds for X being Subset of A holds U.X c= U.(U.X); begin :: Towards Topological Models of Rough Sets definition let T be TopSpace; func ClMap T -> Function of bool the carrier of T, bool the carrier of T means :: ROUGHS_2:def 15 for X being Subset of T holds it.X = Cl X; func IntMap T -> Function of bool the carrier of T, bool the carrier of T means :: ROUGHS_2:def 16 for X being Subset of T holds it.X = Int X; end; definition let T be TopSpace; let f be Function of bool the carrier of T, bool the carrier of T; attr f is closed-valued means :: ROUGHS_2:def 17 for X being Subset of T holds f.X is closed; attr f is open-valued means :: ROUGHS_2:def 18 for X being Subset of T holds f.X is open; end; registration let T be TopSpace; cluster ClMap T -> closed-valued; cluster IntMap T -> open-valued; end; registration let T be TopSpace; cluster closed-valued for Function of bool the carrier of T, bool the carrier of T; cluster open-valued for Function of bool the carrier of T, bool the carrier of T; end; theorem :: ROUGHS_2:25 for T being TopSpace holds Flip ClMap T = IntMap T; theorem :: ROUGHS_2:26 for T being TopSpace holds Flip IntMap T = ClMap T; registration let T be non empty TopSpace; cluster ClMap T -> empty-preserving universe-preserving; cluster IntMap T -> empty-preserving universe-preserving; end; begin :: Formalization of Zhu's Paper :: General Finite Relations theorem :: ROUGHS_2:27 for R being non empty RelStr holds Flip UAp R = LAp R; theorem :: ROUGHS_2:28 for R being non empty RelStr holds Flip LAp R = UAp R; theorem :: ROUGHS_2:29 :: Proposition 1 2H 4H for A being non empty finite set, U being Function of bool A, bool A st U.{} = {} & (for X, Y being Subset of A holds U.(X \/ Y) = U.X \/ U.Y) holds ex R being non empty finite RelStr st the carrier of R = A & U = UAp R; theorem :: ROUGHS_2:30 :: Proposition 1 1L 4L for A being non empty finite set, L being Function of bool A, bool A st L.A = A & (for X, Y being Subset of A holds L.(X /\ Y) = L.X /\ L.Y) holds ex R being non empty finite RelStr st the carrier of R = A & L = LAp R; :: Serial Relations theorem :: ROUGHS_2:31 :: Proposition 2 1L 4L 2L for A being non empty finite set, L being Function of bool A, bool A st L.A = A & L.{} = {} & (for X, Y being Subset of A holds L.(X /\ Y) = L.X /\ L.Y) holds ex R being non empty serial RelStr st the carrier of R = A & L = LAp R; theorem :: ROUGHS_2:32 :: Proposition 2 1H 4H 2H for A being non empty finite set, U being Function of bool A, bool A st U.A = A & U.{} = {} & (for X, Y being Subset of A holds U.(X \/ Y) = U.X \/ U.Y) holds ex R being non empty finite serial RelStr st the carrier of R = A & U = UAp R; theorem :: ROUGHS_2:33 :: Proposition 3 1L 4L 8LH for A being non empty finite set, L being Function of bool A, bool A st L.A = A & (for X being Subset of A holds L.X c= (L.(X`))`) & (for X, Y being Subset of A holds L.(X /\ Y) = L.X /\ L.Y) holds ex R being non empty finite serial RelStr st the carrier of R = A & L = LAp R; theorem :: ROUGHS_2:34 :: Proposition 4 2H 4H 8LH for A being non empty finite set, U being Function of bool A, bool A st U.{} = {} & (for X being Subset of A holds (U.(X`))` c= U.X) & (for X, Y being Subset of A holds U.(X \/ Y) = U.X \/ U.Y) holds ex R being non empty serial RelStr st the carrier of R = A & U = UAp R; :: Reflexive binary relations theorem :: ROUGHS_2:35 :: Proposition 5 3L for R being non empty reflexive RelStr, X being Subset of R holds LAp X c= X; theorem :: ROUGHS_2:36 :: Proposition 5 3H for R being non empty reflexive RelStr, X being Subset of R holds X c= UAp X; theorem :: ROUGHS_2:37 :: Proposition 5 1H 4H 3H for A being non empty finite set, U being Function of bool A, bool A st U.{} = {} & (for X being Subset of A holds X c= U.X) & (for X,Y being Subset of A holds U.(X \/ Y) = U.X \/ U.Y) holds ex R being non empty finite reflexive RelStr st the carrier of R = A & U = UAp R; theorem :: ROUGHS_2:38 :: Proposition 5 1L 4L 3L for A being non empty finite set, L being Function of bool A, bool A st L.A = A & (for X being Subset of A holds L.X c= X) & (for X,Y being Subset of A holds L.(X /\ Y) = L.X /\ L.Y) holds ex R being non empty finite reflexive RelStr st the carrier of R = A & L = LAp R; :: Mediate Relations theorem :: ROUGHS_2:39 :: Proposition 6 5H' for R being non empty mediate RelStr, X being Subset of R holds UAp X c= UAp (UAp X); theorem :: ROUGHS_2:40 :: Proposition 6 5L' for R being non empty mediate RelStr, X being Subset of R holds LAp (LAp X) c= LAp X; theorem :: ROUGHS_2:41 :: Proposition 7 2H 4H 5H' for A being non empty finite set, U being Function of bool A, bool A st U.{} = {} & (for X being Subset of A holds U.X c= U.(U.X)) & (for X,Y being Subset of A holds U.(X \/ Y) = U.X \/ U.Y) holds ex R being non empty mediate finite RelStr st the carrier of R = A & U = UAp R; theorem :: ROUGHS_2:42 :: Proposition 8 1L 4L 5L' for A being non empty finite set, L being Function of bool A, bool A st L.A = A & (for X being Subset of A holds L.(L.X) c= L.X) & (for X,Y being Subset of A holds L.(X /\ Y) = L.X /\ L.Y) holds ex R being non empty mediate finite RelStr st the carrier of R = A & L = LAp R; :: Corollaries theorem :: ROUGHS_2:43 :: Corollary 1 for A being non empty finite set, L being Function of bool A, bool A st L.A = A & (for X, Y being Subset of A holds L.(X /\ Y) = L.X /\ L.Y) holds (for X being Subset of A holds L.X c= (L.(X`))`) iff L.{} = {}; theorem :: ROUGHS_2:44 :: Corollary 2 for A being non empty finite set, U being Function of bool A, bool A st U.{} = {} & (for X,Y being Subset of A holds U.(X \/ Y) = U.X \/ U.Y) holds (for X being Subset of A holds (U.(X`))` c= U.X) iff U.A = A;