ROUGHS_2: Relational Formal Characterization of Rough Sets

proof end;

end;

theorem Th1: :: ROUGHS_2:1

for R being non empty total RelStr
for x being Element of R holds x in field the InternalRel of R

proof end;

theorem Th2: :: ROUGHS_2:2

for R being non empty 1-sorted
for X being Subset of R holds { x where x is Element of R : {} c= X } = [#] R

proof end;

theorem Th3: :: ROUGHS_2:3

for R being 1-sorted
for X being Subset of R holds { x where x is Element of R : {} meets X } = {} R

proof end;

definition

let R be Relation;
let X be set ;

pred R is_serial_in X means :Def1: :: 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;

:: deftheorem Def1 defines is_serial_in ROUGHS_2:def 1 :

definition

let R be Relation;

attr R is serial means :: ROUGHS_2:def 2
R is_serial_in field R;

end;

:: deftheorem defines serial ROUGHS_2:def 2 :

definition

let R be RelStr ;

attr R is serial means :Def3: :: ROUGHS_2:def 3
the InternalRel of R is_serial_in the carrier of R;

end;

:: deftheorem Def3 defines serial ROUGHS_2:def 3 :

Lm1: for R being RelStr st the InternalRel of R is_reflexive_in the carrier of R holds
R is serial

proof end;

registration

cluster reflexive -> serial for RelStr ;

coherence by Lm1, ORDERS_2:def 2;

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;

compatibility

proof end;

end;

:: deftheorem defines serial ROUGHS_2:def 4 :

registration

cluster total -> serial for RelStr ;

proof end;

cluster serial -> total for RelStr ;

proof end;

end;

Lm2: for R being non empty serial RelStr
for x being Element of R holds Class ( the InternalRel of R,x) <> {}

proof end;

registration

let R be non empty serial RelStr ;
let x be Element of R;

cluster Im ( the InternalRel of R,x) -> non empty ;

coherence by Lm2;

end;

:: Reflexive relations

theorem Th4: :: ROUGHS_2:4

for R being non empty reflexive RelStr
for x being Element of R holds x in Class ( the InternalRel of R,x)

proof end;

registration

let R be non empty reflexive RelStr ;
let x be Element of R;

cluster Im ( the InternalRel of R,x) -> non empty ;

coherence ;

end;

:: Mediate relations

definition

let R be Relation;
let X be set ;

:: Mediate relations

pred R is_mediate_in X means :Def5: :: ROUGHS_2:def 5
for x, y being object st x in X & y in X & [x,y] in R holds
ex z being object st
( z in X & [x,z] in R & [z,y] in R );

end;

:: deftheorem Def5 defines is_mediate_in ROUGHS_2:def 5 :

definition

let R be Relation;

attr R is mediate means :: ROUGHS_2:def 6
R is_mediate_in field R;

end;

:: deftheorem defines mediate ROUGHS_2:def 6 :

definition

let R be RelStr ;

attr R is mediate means :Def7: :: ROUGHS_2:def 7
the InternalRel of R is_mediate_in the carrier of R;

end;

:: deftheorem Def7 defines mediate ROUGHS_2:def 7 :

registration

cluster reflexive -> mediate for RelStr ;

proof end;

end;

theorem Th5: :: ROUGHS_2:5

for R being non empty RelStr
for a, b being Element of R st a in UAp {b} holds
[a,b] in the InternalRel of R

proof end;

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 `)) ` ;

coherence ;

end;

:: deftheorem defines Uap ROUGHS_2:def 8 :

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 `)) ` ;

coherence ;

end;

:: deftheorem defines Lap ROUGHS_2:def 9 :

theorem Th6: :: ROUGHS_2:6

for R being non empty RelStr
for X being Subset of R
for x being object st x in LAp X holds
Class ( the InternalRel of R,x) c= X

proof end;

theorem Th7: :: ROUGHS_2:7

for R being non empty RelStr
for X being Subset of R
for x being set st x in UAp X holds
Class ( the InternalRel of R,x) meets X

proof end;

theorem Th8: :: ROUGHS_2:8

for R being non empty RelStr
for X being Subset of R holds Uap X = UAp X

proof end;

theorem Th9: :: ROUGHS_2:9

for R being non empty RelStr
for X being Subset of R holds Lap X = LAp X

proof end;

theorem :: ROUGHS_2:10

for R being non empty void RelStr
for X being Subset of R holds LAp X = [#] R

proof end;

theorem :: ROUGHS_2:11

for R being non empty void RelStr
for X being Subset of R holds UAp X = {} R

proof end;

registration

let R be non empty RelStr ;

reduce LAp ([#] R) to [#] R;

proof end;

end;

registration

let R be non empty serial RelStr ;

reduce UAp ([#] R) to [#] R;

proof end;

end;

registration

let R be non empty serial RelStr ;

reduce LAp ({} R) to {} R;

proof end;

end;

registration

let R be non empty RelStr ;

reduce UAp ({} R) to {} R;

proof end;

end;

theorem :: ROUGHS_2:12

for R being non empty RelStr
for X, Y being Subset of R holds LAp (X /\ Y) = (LAp X) /\ (LAp Y)

proof end;

theorem Th13: :: ROUGHS_2:13

for R being non empty RelStr
for X, Y being Subset of R holds UAp (X \/ Y) = (UAp X) \/ (UAp Y)

proof end;

theorem :: ROUGHS_2:14

for R being non empty RelStr
for X, Y being Subset of R st X c= Y holds
LAp X c= LAp Y

proof end;

theorem Th15: :: ROUGHS_2:15

for R being non empty RelStr
for X, Y being Subset of R st X c= Y holds
UAp X c= UAp Y

proof end;

theorem Th16: :: ROUGHS_2:16

for R being non empty RelStr
for X being Subset of R holds LAp (X `) = (UAp X) `

proof end;

theorem Th17: :: ROUGHS_2:17

for R being non empty serial RelStr
for X being Subset of R holds LAp X c= UAp X

proof end;

definition

let R be non empty RelStr ;

func LAp R -> Function of (bool the carrier of R),(bool the carrier of R) means :Def10: :: ROUGHS_2:def 10
for X being Subset of R holds it . X = LAp X;

proof end;

proof end;

func UAp R -> Function of (bool the carrier of R),(bool the carrier of R) means :Def11: :: ROUGHS_2:def 11
for X being Subset of R holds it . X = UAp X;

proof end;

proof end;

end;

:: deftheorem Def10 defines LAp ROUGHS_2:def 10 :

:: deftheorem Def11 defines UAp ROUGHS_2:def 11 :

definition

let f be Function;

attr f is empty-preserving means :Def12: :: ROUGHS_2:def 12
f . {} = {} ;

end;

:: deftheorem Def12 defines empty-preserving ROUGHS_2:def 12 :

definition

let A be set ;
let f be Function of (bool A),(bool A);

attr f is universe-preserving means :Def13: :: ROUGHS_2:def 13
f . A = A;

end;

:: deftheorem Def13 defines universe-preserving ROUGHS_2:def 13 :

registration

let A be non empty set ;

cluster id (bool A) -> empty-preserving universe-preserving for Function of (bool A),(bool A);

proof end;

end;

registration

let A be non empty set ;

cluster non empty Relation-like bool A -defined bool A -valued Function-like total V29( bool A, bool A) empty-preserving universe-preserving for Element of bool [:(bool A),(bool A):];

proof end;

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 :Def14: :: ROUGHS_2:def 14
for x being Subset of X holds it . x = (f . (x `)) ` ;

proof end;

proof end;

end;

:: deftheorem Def14 defines Flip ROUGHS_2:def 14 :

theorem Th18: :: ROUGHS_2:18

for X being set
for f being Function of (bool X),(bool X) st f . {} = {} holds
(Flip f) . X = X

proof end;

theorem Th19: :: ROUGHS_2:19

for X being set
for f being Function of (bool X),(bool X) st f . X = X holds
(Flip f) . {} = {}

proof end;

theorem :: ROUGHS_2:20

for X being set
for f being Function of (bool X),(bool X) st f = id (bool X) holds
Flip f = f

proof end;

theorem :: ROUGHS_2:21

for X being set
for 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)

proof end;

theorem Th22: :: ROUGHS_2:22

for X being set
for 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)

proof end;

theorem Th23: :: ROUGHS_2:23

for X being set
for f being Function of (bool X),(bool X) holds Flip (Flip f) = f

proof end;

registration

let A be non empty set ;
let f be universe-preserving Function of (bool A),(bool A);

cluster Flip f -> empty-preserving ;

proof end;

end;

registration

let A be non empty set ;
let f be empty-preserving Function of (bool A),(bool A);

cluster Flip f -> universe-preserving ;

proof end;

end;

theorem Th24: :: ROUGHS_2:24

for A being non empty set
for 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)

proof end;

definition

let T be TopSpace;

func ClMap T -> Function of (bool the carrier of T),(bool the carrier of T) means :Def15: :: ROUGHS_2:def 15
for X being Subset of T holds it . X = Cl X;

proof end;

proof end;

func IntMap T -> Function of (bool the carrier of T),(bool the carrier of T) means :Def16: :: ROUGHS_2:def 16
for X being Subset of T holds it . X = Int X;

proof end;

proof end;

end;

:: deftheorem Def15 defines ClMap ROUGHS_2:def 15 :

:: deftheorem Def16 defines IntMap ROUGHS_2:def 16 :

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;

:: deftheorem defines closed-valued ROUGHS_2:def 17 :

:: deftheorem defines open-valued ROUGHS_2:def 18 :

registration

let T be TopSpace;

cluster ClMap T -> closed-valued ;

proof end;

cluster IntMap T -> open-valued ;

proof end;

end;

registration

let T be TopSpace;

cluster non empty Relation-like bool the carrier of T -defined bool the carrier of T -valued Function-like total V29( bool the carrier of T, bool the carrier of T) closed-valued for Element of bool [:(bool the carrier of T),(bool the carrier of T):];

proof end;

cluster non empty Relation-like bool the carrier of T -defined bool the carrier of T -valued Function-like total V29( bool the carrier of T, bool the carrier of T) open-valued for Element of bool [:(bool the carrier of T),(bool the carrier of T):];

proof end;

end;

theorem Th25: :: ROUGHS_2:25

for T being TopSpace holds Flip (ClMap T) = IntMap T

proof end;

theorem :: ROUGHS_2:26

for T being TopSpace holds Flip (IntMap T) = ClMap T

proof end;

registration

let T be non empty TopSpace;

cluster ClMap T -> empty-preserving universe-preserving ;

proof end;

cluster IntMap T -> empty-preserving universe-preserving ;