ROUGHS_1: Basic Properties of Rough Sets and Rough Membership Function

:: Basic Properties of Rough Sets and Rough Membership Function
:: by Adam Grabowski
::
:: Received November 23, 2003
:: Copyright (c) 2003-2021 Association of Mizar Users

registration

let A be set ;

cluster RelStr(# A,(id A) #) -> discrete ;

coherence by ORDERS_3:def 1;

end;

theorem Th1: :: ROUGHS_1:1

for X being set st Total X c= id X holds
X is trivial

proof end;

definition

let A be RelStr ;

attr A is diagonal means :Def1: :: ROUGHS_1:def 1
the InternalRel of A c= id the carrier of A;

end;

:: deftheorem Def1 defines diagonal ROUGHS_1:def 1 :

registration

let A be non trivial set ;

cluster RelStr(# A,(Total A) #) -> non diagonal ;

coherence by Th1;

end;

theorem :: ROUGHS_1:2

for L being reflexive RelStr holds id the carrier of L c= the InternalRel of L

proof end;

Lm1: for A being RelStr st A is reflexive & A is trivial holds
A is discrete

proof end;

registration

cluster reflexive non discrete -> non trivial reflexive for RelStr ;

coherence by Lm1;

cluster trivial reflexive -> discrete for RelStr ;

end;

theorem :: ROUGHS_1:3

for X being set
for R being Relation of X holds
( ( R is total & R is reflexive ) iff id X c= R )

proof end;

Lm2: for A being RelStr st A is discrete holds
A is diagonal
by ORDERS_3:def 1;

registration

cluster discrete -> diagonal for RelStr ;

coherence by Lm2;

cluster non diagonal -> non discrete for RelStr ;

end;

registration

cluster non empty non diagonal for RelStr ;

proof end;

end;

theorem Th4: :: ROUGHS_1:4

for A being non empty non diagonal RelStr ex x, y being Element of A st
( x <> y & [x,y] in the InternalRel of A )

proof end;

theorem Th5: :: ROUGHS_1:5

for D being set
for p, q being FinSequence of D holds Union (p ^ q) = (Union p) \/ (Union q)

proof end;

theorem Th6: :: ROUGHS_1:6

for p, q being Function st q is disjoint_valued & p c= q holds
p is disjoint_valued

proof end;

registration

cluster empty Relation-like Function-like -> disjoint_valued for set ;

proof end;

end;

registration

let A be set ;

cluster Relation-like NAT -defined A -valued Function-like finite disjoint_valued FinSequence-like FinSubsequence-like for FinSequence of A;

proof end;

end;

registration

let A be non empty set ;

cluster non empty Relation-like NAT -defined A -valued Function-like finite disjoint_valued FinSequence-like FinSubsequence-like for FinSequence of A;

proof end;

end;

definition

let A be set ;
let X be FinSequence of bool A;
let n be Nat;
:: original: .
redefine func X . n -> Subset of A;
coherence

proof end;

end;

definition

let A be set ;
let X be FinSequence of bool A;
:: original: Union
redefine func Union X -> Subset of A;
coherence

proof end;

end;

registration

let A be finite set ;
let R be Relation of A;

cluster RelStr(# A,R #) -> finite ;

end;

theorem Th7: :: ROUGHS_1:7

for X being set
for x, y being object
for T being Tolerance of X st x in Class (T,y) holds
y in Class (T,x)

proof end;

definition

let P be RelStr ;

attr P is with_equivalence means :Def2: :: ROUGHS_1:def 2
the InternalRel of P is Equivalence_Relation of the carrier of P;

attr P is with_tolerance means :Def3: :: ROUGHS_1:def 3
the InternalRel of P is Tolerance of the carrier of P;

end;

:: deftheorem Def2 defines with_equivalence ROUGHS_1:def 2 :

:: deftheorem Def3 defines with_tolerance ROUGHS_1:def 3 :

registration

cluster with_equivalence -> with_tolerance for RelStr ;

end;

registration

let A be set ;

cluster RelStr(# A,(id A) #) -> with_equivalence ;

end;

registration

cluster non empty finite discrete with_equivalence for RelStr ;

proof end;

cluster non empty finite non diagonal with_equivalence for RelStr ;

proof end;

end;

definition

mode Approximation_Space is non empty with_equivalence RelStr ;
mode Tolerance_Space is non empty with_tolerance RelStr ;

end;

registration

let A be Tolerance_Space;

cluster the InternalRel of A -> reflexive symmetric total ;

coherence by Def3;

end;

registration

let A be Approximation_Space;

cluster the InternalRel of A -> transitive ;

coherence by Def2;

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 } ;

proof end;

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 } ;

proof end;

end;

:: deftheorem defines LAp ROUGHS_1:def 4 :

:: deftheorem defines UAp ROUGHS_1:def 5 :

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;

:: deftheorem defines BndAp ROUGHS_1:def 6 :

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;

:: deftheorem defines rough ROUGHS_1:def 7 :

notation

let A be non empty RelStr ;
let X be Subset of A;
antonym exact X for rough ;

end;

theorem Th8: :: ROUGHS_1:8

for A being Tolerance_Space
for X being Subset of A
for x being object st x in LAp X holds
Class ( the InternalRel of A,x) c= X

proof end;

theorem :: ROUGHS_1:9

for A being Tolerance_Space
for X being Subset of A
for x being Element of A st Class ( the InternalRel of A,x) c= X holds
x in LAp X ;

theorem Th10: :: ROUGHS_1:10

for A being Tolerance_Space
for X being Subset of A
for x being set st x in UAp X holds
Class ( the InternalRel of A,x) meets X

proof end;

theorem :: ROUGHS_1:11

for A being Tolerance_Space
for X being Subset of A
for x being Element of A st Class ( the InternalRel of A,x) meets X holds
x in UAp X ;

theorem Th12: :: ROUGHS_1:12

for A being Tolerance_Space
for X being Subset of A holds LAp X c= X

proof end;

theorem Th13: :: ROUGHS_1:13

for A being Tolerance_Space
for X being Subset of A holds X c= UAp X

proof end;

theorem Th14: :: ROUGHS_1:14

for A being Tolerance_Space
for X being Subset of A holds LAp X c= UAp X

proof end;

theorem Th15: :: ROUGHS_1:15

for A being Tolerance_Space
for X being Subset of A holds
( X is exact iff LAp X = X )

proof end;

theorem Th16: :: ROUGHS_1:16

for A being Tolerance_Space
for X being Subset of A holds
( X is exact iff UAp X = X )

proof end;

theorem :: ROUGHS_1:17

for A being Tolerance_Space
for X being Subset of A holds
( X = LAp X iff X = UAp X ) by Th15, Th16;

theorem Th18: :: ROUGHS_1:18

for A being Tolerance_Space holds LAp ({} A) = {}

proof end;

theorem Th19: :: ROUGHS_1:19

for A being Tolerance_Space holds UAp ({} A) = {}

proof end;

theorem Th20: :: ROUGHS_1:20

for A being Tolerance_Space holds LAp ([#] A) = [#] A

proof end;

theorem :: ROUGHS_1:21

for A being Tolerance_Space holds UAp ([#] A) = [#] A

proof end;

theorem :: ROUGHS_1:22

for A being Tolerance_Space
for X, Y being Subset of A holds LAp (X /\ Y) = (LAp X) /\ (LAp Y)

proof end;

theorem :: ROUGHS_1:23

for A being Tolerance_Space
for X, Y being Subset of A holds UAp (X \/ Y) = (UAp X) \/ (UAp Y)

proof end;

theorem Th24: :: ROUGHS_1:24

for A being Tolerance_Space
for X, Y being Subset of A st X c= Y holds
LAp X c= LAp Y

proof end;

theorem Th25: :: ROUGHS_1:25

for A being Tolerance_Space
for X, Y being Subset of A st X c= Y holds
UAp X c= UAp Y

proof end;

theorem :: ROUGHS_1:26

for A being Tolerance_Space
for X, Y being Subset of A holds (LAp X) \/ (LAp Y) c= LAp (X \/ Y)

proof end;

theorem :: ROUGHS_1:27

for A being Tolerance_Space
for X, Y being Subset of A holds UAp (X /\ Y) c= (UAp X) /\ (UAp Y)

proof end;

theorem Th28: :: ROUGHS_1:28

for A being Tolerance_Space
for X being Subset of A holds LAp (X `) = (UAp X) `

proof end;

theorem Th29: :: ROUGHS_1:29

for A being Tolerance_Space
for X being Subset of A holds UAp (X `) = (LAp X) `

proof end;

theorem :: ROUGHS_1:30

for A being Tolerance_Space
for X being Subset of A holds UAp (LAp (UAp X)) = UAp X

proof end;

theorem :: ROUGHS_1:31

for A being Tolerance_Space
for X being Subset of A holds LAp (UAp (LAp X)) = LAp X

proof end;

theorem :: ROUGHS_1:32

for A being Tolerance_Space
for X being Subset of A holds BndAp X = BndAp (X `)

proof end;

theorem :: ROUGHS_1:33

for A being Approximation_Space
for X being Subset of A holds LAp (LAp X) = LAp X

proof end;

theorem Th34: :: ROUGHS_1:34

for A being Approximation_Space
for X being Subset of A holds LAp (LAp X) = UAp (LAp X)

proof end;

theorem :: ROUGHS_1:35

for A being Approximation_Space
for X being Subset of A holds UAp (UAp X) = UAp X

proof end;

theorem Th36: :: ROUGHS_1:36

for A being Approximation_Space
for X being Subset of A holds UAp (UAp X) = LAp (UAp X)

proof end;

registration

let A be Tolerance_Space;

cluster exact for Element of bool the carrier of A;

proof end;

end;

registration

let A be Approximation_Space;
let X be Subset of A;

cluster LAp X -> exact ;

proof end;

cluster UAp X -> exact ;

proof end;

end;

theorem Th37: :: ROUGHS_1:37

for A being Approximation_Space
for X being Subset of A
for x, y being set st x in UAp X & [x,y] in the InternalRel of A holds
y in UAp X

proof end;

registration

let A be non diagonal Approximation_Space;

cluster rough for Element of bool the carrier of A;

proof end;

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;

:: deftheorem defines RoughSet ROUGHS_1:def 8 :

registration

let A be finite Tolerance_Space;
let x be Element of A;

cluster card (Class ( the InternalRel of A,x)) -> non empty ;

proof end;

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 :Def9: :: 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)));

proof end;

proof end;

end;

:: deftheorem Def9 defines MemberFunc ROUGHS_1:def 9 :

theorem Th38: :: ROUGHS_1:38

for A being finite Tolerance_Space
for X being Subset of A
for x being Element of A holds
( 0 <= (MemberFunc (X,A)) . x & (MemberFunc (X,A)) . x <= 1 )

proof end;

theorem :: ROUGHS_1:39

for A being finite Tolerance_Space
for X being Subset of A
for x being Element of A holds (MemberFunc (X,A)) . x in [.0,1.]

proof end;

theorem Th40: :: ROUGHS_1:40

for A being finite Approximation_Space
for X being Subset of A
for x being Element of A holds
( (MemberFunc (X,A)) . x = 1 iff x in LAp X )

proof end;

theorem Th41: :: ROUGHS_1:41

for A being finite Approximation_Space
for X being Subset of A
for x being Element of A holds
( (MemberFunc (X,A)) . x = 0 iff x in (UAp X) ` )

proof end;

theorem Th42: :: ROUGHS_1:42

for A being finite Approximation_Space
for X being Subset of A
for x being Element of A holds
( ( 0 < (MemberFunc (X,A)) . x & (MemberFunc (X,A)) . x < 1 ) iff x in BndAp X )

proof end;

theorem Th43: :: ROUGHS_1:43

for A being discrete Approximation_Space
for X being Subset of A holds X is exact

proof end;

registration

let A be discrete Approximation_Space;

cluster -> exact for Element of bool the carrier of A;

coherence by Th43;

end;

theorem :: ROUGHS_1:44

for A being finite discrete Approximation_Space
for X being Subset of A holds MemberFunc (X,A) = chi (X, the carrier of A)

proof end;

theorem :: ROUGHS_1:45

for A being finite Approximation_Space
for X being Subset of A
for x, y being set st [x,y] in the InternalRel of A holds
(MemberFunc (X,A)) . x = (MemberFunc (X,A)) . y

proof end;

theorem :: ROUGHS_1:46

for A being finite Approximation_Space
for X being Subset of A
for x being Element of A holds (MemberFunc ((X `),A)) . x = 1 - ((MemberFunc (X,A)) . x)

proof end;

theorem Th47: :: ROUGHS_1:47

for A being finite Approximation_Space
for X, Y being Subset of A
for x being Element of A st X c= Y holds
(MemberFunc (X,A)) . x <= (MemberFunc (Y,A)) . x

proof end;

theorem :: ROUGHS_1:48

for A being finite Approximation_Space
for X, Y being Subset of A
for x being Element of A holds (MemberFunc ((X \/ Y),A)) . x >= (MemberFunc (X,A)) . x by Th47, XBOOLE_1:7;

theorem :: ROUGHS_1:49

for A being finite Approximation_Space
for X, Y being Subset of A
for x being Element of A holds (MemberFunc ((X /\ Y),A)) . x <= (MemberFunc (X,A)) . x by Th47, XBOOLE_1:17;

theorem :: ROUGHS_1:50

for A being finite Approximation_Space
for X, Y being Subset of A
for x being Element of A holds (MemberFunc ((X \/ Y),A)) . x >= max (((MemberFunc (X,A)) . x),((MemberFunc (Y,A)) . x))

proof end;

theorem Th51: :: ROUGHS_1:51

for A being finite Approximation_Space
for X, Y being Subset of A
for x being Element of A st X misses Y holds
(MemberFunc ((X \/ Y),A)) . x = ((MemberFunc (X,A)) . x) + ((MemberFunc (Y,A)) . x)

proof end;

theorem :: ROUGHS_1:52

for A being finite Approximation_Space
for X, Y being Subset of A
for x being Element of A holds (MemberFunc ((X /\ Y),A)) . x <= min (((MemberFunc (X,A)) . x),((MemberFunc (Y,A)) . x))

proof end;

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 :Def10: :: 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 ) );

proof end;

proof end;

end;

:: deftheorem Def10 defines FinSeqM ROUGHS_1:def 10 :

theorem Th53: :: ROUGHS_1:53

for A being finite Approximation_Space
for X being FinSequence of bool the carrier of A
for x being Element of A
for y being Subset of A holds FinSeqM (x,(X ^ <*y*>)) = (FinSeqM (x,X)) ^ <*((MemberFunc (y,A)) . x)*>

proof end;

theorem Th54: :: ROUGHS_1:54

for A being finite Approximation_Space
for x being Element of A holds (MemberFunc (({} A),A)) . x = 0

proof end;

theorem :: ROUGHS_1:55

for A being finite Approximation_Space
for x being Element of A
for X being disjoint_valued FinSequence of bool the carrier of A holds (MemberFunc ((Union X),A)) . x = Sum (FinSeqM (x,X))

proof end;

theorem :: ROUGHS_1:56

for A being finite Approximation_Space
for X being Subset of A holds LAp X = { x where x is Element of A : (MemberFunc (X,A)) . x = 1 }

proof end;

theorem :: ROUGHS_1:57

for A being finite Approximation_Space
for X being Subset of A holds UAp X = { x where x is Element of A : (MemberFunc (X,A)) . x > 0 }

proof end;

theorem :: ROUGHS_1:58

for A being finite Approximation_Space
for X being Subset of A holds BndAp X = { x where x is Element of A : ( 0 < (MemberFunc (X,A)) . x & (MemberFunc (X,A)) . x < 1 ) }

proof end;

definition

let A be Tolerance_Space;
let X, Y be Subset of A;

pred X _c= Y means :: ROUGHS_1:def 11
LAp X c= LAp Y;

pred X c=^ Y means :: ROUGHS_1:def 12
UAp X c= UAp Y;

end;

:: deftheorem defines _c= ROUGHS_1:def 11 :

:: deftheorem defines c=^ ROUGHS_1:def 12 :

definition

let A be Tolerance_Space;
let X, Y be Subset of A;

pred X _c=^ Y means :: ROUGHS_1:def 13
( X _c= Y & X c=^ Y );

end;

:: deftheorem defines _c=^ ROUGHS_1:def 13 :

theorem Th59: :: ROUGHS_1:59

for A being Tolerance_Space
for X, Y, Z being Subset of A st X _c= Y & Y _c= Z holds
X _c= Z

proof end;

theorem Th60: :: ROUGHS_1:60

for A being Tolerance_Space
for X, Y, Z being Subset of A st X c=^ Y & Y c=^ Z holds
X c=^ Z

proof end;

theorem :: ROUGHS_1:61

for A being Tolerance_Space
for X, Y, Z being Subset of A st X _c=^ Y & Y _c=^ Z holds
X _c=^ Z by Th60, Th59;

definition

let A be Tolerance_Space;
let 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;

:: deftheorem defines _= ROUGHS_1:def 14 :

:: deftheorem defines =^ ROUGHS_1:def 15 :

:: deftheorem defines _=^ ROUGHS_1:def 16 :

definition

let A be Tolerance_Space;
let X, Y be Subset of A;

redefine pred X _= Y means :: ROUGHS_1:def 17
( X _c= Y & Y _c= X );

proof end;

redefine pred X =^ Y means :: ROUGHS_1:def 18
( X c=^ Y & Y c=^ X );

proof end;

redefine pred X _=^ Y means :: ROUGHS_1:def 19
( X _= Y & X =^ Y );

compatibility ;

end;

:: deftheorem defines _= ROUGHS_1:def 17 :

:: deftheorem defines =^ ROUGHS_1:def 18 :

:: deftheorem defines _=^ ROUGHS_1:def 19 :