:: Basic Properties of Rough Sets and Rough Membership Function :: by Adam Grabowski :: :: Received November 23, 2003 :: Copyright (c) 2003-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 NUMBERS, ORDERS_2, RELAT_1, NATTRA_1, TOLER_1, TARSKI, ZFMISC_1, MATRIX_1, STRUCT_0, RELAT_2, XBOOLE_0, PARTFUN1, SUBSET_1, FINSEQ_1, CARD_3, ORDINAL4, FUNCT_1, PROB_2, FINSEQ_2, NAT_1, FINSET_1, EQREL_1, CARD_1, ARYTM_3, XXREAL_0, XXREAL_1, FUNCT_3, ARYTM_1, ROUGHS_1, FUNCT_7; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, FINSET_1, RELAT_1, RELAT_2, FUNCT_1, FINSEQ_1, RVSUM_1, FINSEQ_2, RELSET_1, PARTFUN1, CARD_3, PROB_2, FUNCT_2, FUNCT_3, DOMAIN_1, STRUCT_0, ORDERS_2, EQREL_1, RCOMP_1, TOLER_1, ORDERS_3; constructors EQREL_1, PROB_2, RCOMP_1, RVSUM_1, FUNCT_6, REALSET2, ORDERS_3, RELSET_1, BINOP_2, NUMBERS; registrations XBOOLE_0, SUBSET_1, RELAT_1, PARTFUN1, FINSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, MEMBERED, FINSEQ_1, EQREL_1, STRUCT_0, ORDERS_2, VALUED_0, CARD_1, RELSET_1; requirements BOOLE, SUBSET, NUMERALS, REAL; begin :: Preliminaries registration let A be set; cluster RelStr (# A, id A #) -> discrete; end; theorem :: ROUGHS_1:1 for X being set st Total X c= id X holds X is trivial; definition let A be RelStr; attr A is diagonal means :: ROUGHS_1:def 1 the InternalRel of A c= id the carrier of A; end; registration let A be non trivial set; cluster RelStr (# A, Total A #) -> non diagonal; end; theorem :: ROUGHS_1:2 for L being reflexive RelStr holds id the carrier of L c= the InternalRel of L; registration cluster non discrete -> non trivial for reflexive RelStr; cluster reflexive trivial -> discrete for RelStr; end; theorem :: ROUGHS_1:3 for X being set, R being Relation of X holds R is total reflexive iff id X c= R; registration cluster discrete -> diagonal for RelStr; cluster non diagonal -> non discrete for RelStr; end; registration cluster non diagonal non empty for RelStr; end; theorem :: ROUGHS_1:4 for A being non diagonal non empty RelStr ex x, y being Element of A st x <> y & [x,y] in the InternalRel of A; theorem :: ROUGHS_1:5 for D being set, p, q being FinSequence of D holds Union (p^q) = Union p \/ Union q; theorem :: ROUGHS_1:6 for p, q being Function st q is disjoint_valued & p c= q holds p is disjoint_valued; registration cluster empty -> disjoint_valued for Function; end; registration let A be set; cluster disjoint_valued for FinSequence of A; end; registration let A be non empty set; cluster non empty disjoint_valued for FinSequence of A; end; definition let A be set; let X be FinSequence of bool A; let n be Nat; redefine func X.n -> Subset of A; end; definition let A be set; let X be FinSequence of bool A; redefine func Union X -> Subset of A; end; registration let A be finite set; let R be Relation of A; cluster RelStr (# A, R #) -> finite; end; theorem :: ROUGHS_1:7 for X being set, x, y being object, T being Tolerance of X st x in Class (T, y) holds y in Class (T, x); begin :: Tolerance and Approximation Spaces definition let P be RelStr; attr P is with_equivalence means :: ROUGHS_1:def 2 the InternalRel of P is Equivalence_Relation of the carrier of P; attr P is with_tolerance means :: ROUGHS_1:def 3 the InternalRel of P is Tolerance of the carrier of P; end; registration cluster with_equivalence -> with_tolerance for RelStr; end; registration let A be set; cluster RelStr (# A, id A #) -> with_equivalence; end; registration cluster discrete finite with_equivalence non empty for RelStr; cluster non diagonal finite with_equivalence non empty for RelStr; end; definition mode Approximation_Space is with_equivalence non empty RelStr; mode Tolerance_Space is with_tolerance non empty RelStr; end; registration let A be Tolerance_Space; cluster the InternalRel of A -> total reflexive symmetric; end; registration let A be Approximation_Space; cluster the InternalRel of A -> transitive; end; definition let A be non empty RelStr; let X be Subset of A; func LAp X -> Subset of A equals :: ROUGHS_1:def 4 { x where x is Element of A : Class (the InternalRel of A, x) c= X }; func UAp X -> Subset of A equals :: ROUGHS_1:def 5 { x where x is Element of A : Class (the InternalRel of A, x) meets X }; end; definition let A be non empty RelStr; let X be Subset of A; func BndAp X -> Subset of A equals :: ROUGHS_1:def 6 UAp X \ LAp X; end; definition let A be non empty RelStr; let X be Subset of A; attr X is rough means :: ROUGHS_1:def 7 BndAp X <> {}; end; notation let A be non empty RelStr; let X be Subset of A; antonym X is exact for X is rough; end; reserve A for Tolerance_Space, X, Y for Subset of A; theorem :: ROUGHS_1:8 for x being object st x in LAp X holds Class (the InternalRel of A, x) c= X; theorem :: ROUGHS_1:9 for x being Element of A st Class (the InternalRel of A, x) c= X holds x in LAp X; theorem :: ROUGHS_1:10 for x being set st x in UAp X holds Class (the InternalRel of A, x) meets X; theorem :: ROUGHS_1:11 for x being Element of A st Class (the InternalRel of A, x) meets X holds x in UAp X; theorem :: ROUGHS_1:12 LAp X c= X; theorem :: ROUGHS_1:13 X c= UAp X; theorem :: ROUGHS_1:14 LAp X c= UAp X; theorem :: ROUGHS_1:15 X is exact iff LAp X = X; theorem :: ROUGHS_1:16 X is exact iff UAp X = X; theorem :: ROUGHS_1:17 X = LAp X iff X = UAp X; theorem :: ROUGHS_1:18 LAp {}A = {}; theorem :: ROUGHS_1:19 UAp {}A = {}; theorem :: ROUGHS_1:20 LAp [#]A = [#]A; theorem :: ROUGHS_1:21 UAp [#]A = [#]A; theorem :: ROUGHS_1:22 LAp (X /\ Y) = LAp X /\ LAp Y; theorem :: ROUGHS_1:23 UAp (X \/ Y) = UAp X \/ UAp Y; theorem :: ROUGHS_1:24 X c= Y implies LAp X c= LAp Y; theorem :: ROUGHS_1:25 X c= Y implies UAp X c= UAp Y; theorem :: ROUGHS_1:26 LAp X \/ LAp Y c= LAp (X \/ Y); theorem :: ROUGHS_1:27 UAp (X /\ Y) c= UAp X /\ UAp Y; theorem :: ROUGHS_1:28 LAp X` = (UAp X)`; theorem :: ROUGHS_1:29 UAp X` = (LAp X)`; theorem :: ROUGHS_1:30 UAp LAp UAp X = UAp X; theorem :: ROUGHS_1:31 LAp UAp LAp X = LAp X; theorem :: ROUGHS_1:32 BndAp X = BndAp X`; reserve A for Approximation_Space, X for Subset of A; theorem :: ROUGHS_1:33 LAp LAp X = LAp X; theorem :: ROUGHS_1:34 LAp LAp X = UAp LAp X; theorem :: ROUGHS_1:35 UAp UAp X = UAp X; theorem :: ROUGHS_1:36 UAp UAp X = LAp UAp X; registration let A be Tolerance_Space; cluster exact for Subset of A; end; registration let A be Approximation_Space; let X be Subset of A; cluster LAp X -> exact; cluster UAp X -> exact; end; theorem :: ROUGHS_1:37 for A being Approximation_Space, X being Subset of A, x, y being set st x in UAp X & [x,y] in the InternalRel of A holds y in UAp X; registration let A be non diagonal Approximation_Space; cluster rough for Subset of A; end; definition let A be Approximation_Space; let X be Subset of A; mode RoughSet of X -> set means :: ROUGHS_1:def 8 it = [LAp X, UAp X]; end; begin :: Membership Function registration let A be finite Tolerance_Space, x be Element of A; cluster card Class (the InternalRel of A, x) -> non empty; end; definition let A be finite Tolerance_Space; let X be Subset of A; func MemberFunc (X, A) -> Function of the carrier of A, REAL means :: ROUGHS_1:def 9 for x being Element of A holds it.x = card (X /\ Class (the InternalRel of A, x)) / (card Class (the InternalRel of A, x)); end; reserve A for finite Tolerance_Space, X for Subset of A, x for Element of A; theorem :: ROUGHS_1:38 0 <= MemberFunc (X, A).x & MemberFunc (X, A).x <= 1; theorem :: ROUGHS_1:39 MemberFunc (X, A).x in [. 0, 1 .]; reserve A for finite Approximation_Space, X, Y for Subset of A, x for Element of A; theorem :: ROUGHS_1:40 MemberFunc (X, A).x = 1 iff x in LAp X; theorem :: ROUGHS_1:41 MemberFunc (X, A).x = 0 iff x in (UAp X)`; theorem :: ROUGHS_1:42 0 < MemberFunc (X, A).x & MemberFunc (X, A).x < 1 iff x in BndAp X; theorem :: ROUGHS_1:43 for A being discrete Approximation_Space, X being Subset of A holds X is exact; registration let A be discrete Approximation_Space; cluster -> exact for Subset of A; end; theorem :: ROUGHS_1:44 for A being discrete finite Approximation_Space, X being Subset of A holds MemberFunc (X, A) = chi (X, the carrier of A); theorem :: ROUGHS_1:45 for A being finite Approximation_Space, X being Subset of A, x, y being set st [x,y] in the InternalRel of A holds MemberFunc (X, A).x = MemberFunc (X, A).y; theorem :: ROUGHS_1:46 MemberFunc (X`,A).x = 1 - (MemberFunc (X,A).x); theorem :: ROUGHS_1:47 X c= Y implies MemberFunc (X, A).x <= MemberFunc (Y, A).x; theorem :: ROUGHS_1:48 MemberFunc (X \/ Y, A).x >= MemberFunc (X, A).x; theorem :: ROUGHS_1:49 MemberFunc (X /\ Y, A).x <= MemberFunc (X, A).x; theorem :: ROUGHS_1:50 MemberFunc (X \/ Y, A).x >= max (MemberFunc (X, A).x, MemberFunc (Y, A ).x); theorem :: ROUGHS_1:51 X misses Y implies MemberFunc (X \/ Y, A).x = MemberFunc (X, A).x + MemberFunc (Y, A).x; theorem :: ROUGHS_1:52 MemberFunc (X /\ Y, A).x <= min (MemberFunc (X, A).x, MemberFunc (Y, A).x); definition let A be finite Tolerance_Space; let X be FinSequence of bool the carrier of A; let x be Element of A; func FinSeqM (x,X) -> FinSequence of REAL means :: ROUGHS_1:def 10 dom it = dom X & for n being Nat st n in dom X holds it.n = MemberFunc (X.n, A).x; end; theorem :: ROUGHS_1:53 for X being FinSequence of bool the carrier of A, x being Element of A, y being Subset of A holds FinSeqM (x, X^<*y*>) = FinSeqM (x, X) ^ <* MemberFunc (y, A).x *>; theorem :: ROUGHS_1:54 MemberFunc ({}A, A).x = 0; theorem :: ROUGHS_1:55 for X being disjoint_valued FinSequence of bool the carrier of A holds MemberFunc (Union X, A).x = Sum FinSeqM (x, X); theorem :: ROUGHS_1:56 LAp X = { x where x is Element of A : MemberFunc (X, A).x = 1 }; theorem :: ROUGHS_1:57 UAp X = { x where x is Element of A : MemberFunc (X, A).x > 0 }; theorem :: ROUGHS_1:58 BndAp X = { x where x is Element of A : 0 < MemberFunc (X, A).x & MemberFunc (X, A).x < 1 }; begin :: Rough Inclusion reserve A for Tolerance_Space, X, Y, Z for Subset of A; definition let A be Tolerance_Space, X, Y be Subset of A; pred X _c= Y means :: ROUGHS_1:def 11 LAp X c= LAp Y; reflexivity; pred X c=^ Y means :: ROUGHS_1:def 12 UAp X c= UAp Y; reflexivity; end; definition let A be Tolerance_Space, X, Y be Subset of A; pred X _c=^ Y means :: ROUGHS_1:def 13 X _c= Y & X c=^ Y; reflexivity; end; theorem :: ROUGHS_1:59 X _c= Y & Y _c= Z implies X _c= Z; theorem :: ROUGHS_1:60 X c=^ Y & Y c=^ Z implies X c=^ Z; theorem :: ROUGHS_1:61 X _c=^ Y & Y _c=^ Z implies X _c=^ Z; begin :: Rough Equality of Sets definition let A be Tolerance_Space, X, Y be Subset of A; pred X _= Y means :: ROUGHS_1:def 14 LAp X = LAp Y; reflexivity; symmetry; pred X =^ Y means :: ROUGHS_1:def 15 UAp X = UAp Y; reflexivity; symmetry; pred X _=^ Y means :: ROUGHS_1:def 16 LAp X = LAp Y & UAp X = UAp Y; reflexivity; symmetry; end; definition let A be Tolerance_Space, X, Y be Subset of A; redefine pred X _= Y means :: ROUGHS_1:def 17 X _c= Y & Y _c= X; redefine pred X =^ Y means :: ROUGHS_1:def 18 X c=^ Y & Y c=^ X; redefine pred X _=^ Y means :: ROUGHS_1:def 19 X _= Y & X =^ Y; end;