:: Relational Formal Characterization of Rough Sets
::
:: Copyright (c) 2013-2018 Association of Mizar Users

registration
cluster non empty void for RelStr ;
existence
ex b1 being RelStr st
( not b1 is empty & b1 is void )
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 :
for R being Relation
for X being set holds
( R is_serial_in X iff for x being object st x in X holds
ex y being object st
( y in X & [x,y] in R ) );

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 :
for R being Relation holds
( R is serial iff R is_serial_in field R );

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 :
for R being RelStr holds
( R is serial iff the InternalRel of R is_serial_in the carrier of R );

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

proof end;

registration
coherence
for b1 being RelStr st b1 is reflexive holds
b1 is serial
by ;
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
( R is serial iff for x being Element of R ex y being Element of R st x <= y )
proof end;
end;

:: deftheorem defines serial ROUGHS_2:def 4 :
for R being non empty RelStr holds
( R is serial iff for x being Element of R ex y being Element of R st x <= y );

registration
cluster total -> serial for RelStr ;
coherence
for b1 being RelStr st b1 is total holds
b1 is serial
proof end;
cluster serial -> total for RelStr ;
coherence
for b1 being RelStr st b1 is serial holds
b1 is total
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 K41( the InternalRel of R,x) -> non empty ;
coherence
not Class ( the InternalRel of R,x) is empty
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 K41( the InternalRel of R,x) -> non empty ;
coherence
not Class ( the InternalRel of R,x) is empty
;
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 :
for R being Relation
for X being set holds
( R is_mediate_in X iff 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 ) );

definition
let R be Relation;
end;

:: deftheorem defines mediate ROUGHS_2:def 6 :
for R being Relation holds
( R is mediate iff R is_mediate_in field R );

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 :
for R being RelStr holds
( R is mediate iff the InternalRel of R is_mediate_in the carrier of R );

registration
coherence
for b1 being RelStr st b1 is reflexive holds
b1 is mediate
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
(LAp (X ))  is Subset of R
;
end;

:: deftheorem defines Uap ROUGHS_2:def 8 :
for R being non empty RelStr
for X being Subset of R holds Uap X = (LAp (X ))  ;

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
(UAp (X ))  is Subset of R
;
end;

:: deftheorem defines Lap ROUGHS_2:def 9 :
for R being non empty RelStr
for X being Subset of R holds Lap X = (UAp (X ))  ;

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;
reducibility
LAp ([#] R) = [#] R
proof end;
end;

registration
let R be non empty serial RelStr ;
reduce UAp ([#] R) to [#] R;
reducibility
UAp ([#] R) = [#] R
proof end;
end;

registration
let R be non empty serial RelStr ;
reduce LAp ({} R) to {} R;
reducibility
LAp ({} R) = {} R
proof end;
end;

registration
let R be non empty RelStr ;
reduce UAp ({} R) to {} R;
reducibility
UAp ({} R) = {} 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;
existence
ex b1 being Function of (bool the carrier of R),(bool the carrier of R) st
for X being Subset of R holds b1 . X = LAp X
proof end;
uniqueness
for b1, b2 being Function of (bool the carrier of R),(bool the carrier of R) st ( for X being Subset of R holds b1 . X = LAp X ) & ( for X being Subset of R holds b2 . X = LAp X ) holds
b1 = b2
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;
existence
ex b1 being Function of (bool the carrier of R),(bool the carrier of R) st
for X being Subset of R holds b1 . X = UAp X
proof end;
uniqueness
for b1, b2 being Function of (bool the carrier of R),(bool the carrier of R) st ( for X being Subset of R holds b1 . X = UAp X ) & ( for X being Subset of R holds b2 . X = UAp X ) holds
b1 = b2
proof end;
end;

:: deftheorem Def10 defines LAp ROUGHS_2:def 10 :
for R being non empty RelStr
for b2 being Function of (bool the carrier of R),(bool the carrier of R) holds
( b2 = LAp R iff for X being Subset of R holds b2 . X = LAp X );

:: deftheorem Def11 defines UAp ROUGHS_2:def 11 :
for R being non empty RelStr
for b2 being Function of (bool the carrier of R),(bool the carrier of R) holds
( b2 = UAp R iff for X being Subset of R holds b2 . X = UAp X );

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 :
for f being Function holds
( f is empty-preserving iff f . {} = {} );

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 :
for A being set
for f being Function of (bool A),(bool A) holds
( f is universe-preserving iff f . A = A );

registration
let A be non empty set ;
cluster K36((bool A)) -> empty-preserving universe-preserving for Function of (bool A),(bool A);
coherence
for b1 being Function of (bool A),(bool A) st b1 = id (bool A) holds
( b1 is empty-preserving & b1 is universe-preserving )
proof end;
end;

registration
let A be non empty set ;
existence
ex b1 being Function of (bool A),(bool A) st
( b1 is empty-preserving & b1 is universe-preserving )
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 ))  ;
existence
ex b1 being Function of (bool X),(bool X) st
for x being Subset of X holds b1 . x = (f . (x ))
proof end;
uniqueness
for b1, b2 being Function of (bool X),(bool X) st ( for x being Subset of X holds b1 . x = (f . (x ))  ) & ( for x being Subset of X holds b2 . x = (f . (x ))  ) holds
b1 = b2
proof end;
end;

:: deftheorem Def14 defines Flip ROUGHS_2:def 14 :
for X being set
for f, b3 being Function of (bool X),(bool X) holds
( b3 = Flip f iff for x being Subset of X holds b3 . x = (f . (x ))  );

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);
coherence
proof end;
end;

registration
let A be non empty set ;
let f be empty-preserving Function of (bool A),(bool A);
coherence
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;
existence
ex b1 being Function of (bool the carrier of T),(bool the carrier of T) st
for X being Subset of T holds b1 . X = Cl X
proof end;
uniqueness
for b1, b2 being Function of (bool the carrier of T),(bool the carrier of T) st ( for X being Subset of T holds b1 . X = Cl X ) & ( for X being Subset of T holds b2 . X = Cl X ) holds
b1 = b2
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;
existence
ex b1 being Function of (bool the carrier of T),(bool the carrier of T) st
for X being Subset of T holds b1 . X = Int X
proof end;
uniqueness
for b1, b2 being Function of (bool the carrier of T),(bool the carrier of T) st ( for X being Subset of T holds b1 . X = Int X ) & ( for X being Subset of T holds b2 . X = Int X ) holds
b1 = b2
proof end;
end;

:: deftheorem Def15 defines ClMap ROUGHS_2:def 15 :
for T being TopSpace
for b2 being Function of (bool the carrier of T),(bool the carrier of T) holds
( b2 = ClMap T iff for X being Subset of T holds b2 . X = Cl X );

:: deftheorem Def16 defines IntMap ROUGHS_2:def 16 :
for T being TopSpace
for b2 being Function of (bool the carrier of T),(bool the carrier of T) holds
( b2 = IntMap T iff for X being Subset of T holds b2 . X = Int X );

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 :
for T being TopSpace
for f being Function of (bool the carrier of T),(bool the carrier of T) holds
( f is closed-valued iff for X being Subset of T holds f . X is closed );

:: deftheorem defines open-valued ROUGHS_2:def 18 :
for T being TopSpace
for f being Function of (bool the carrier of T),(bool the carrier of T) holds
( f is open-valued iff for X being Subset of T holds f . X is open );

registration
let T be TopSpace;
coherence
proof end;
coherence
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 Function of ,;
existence
ex b1 being Function of (bool the carrier of T),(bool the carrier of T) st b1 is closed-valued
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 Function of ,;
existence
ex b1 being Function of (bool the carrier of T),(bool the carrier of T) st b1 is open-valued
proof end;
end;

theorem Th25: :: ROUGHS_2:25
for T being TopSpace holds Flip () = IntMap T
proof end;

theorem :: ROUGHS_2:26
for T being TopSpace holds Flip () = ClMap T
proof end;

registration
let T be non empty TopSpace;
coherence
proof end;
coherence
proof end;
end;

:: General Finite Relations
theorem Th27: :: ROUGHS_2:27
for R being non empty RelStr holds Flip (UAp R) = LAp R
proof end;

theorem Th28: :: ROUGHS_2:28
for R being non empty RelStr holds Flip (LAp R) = UAp R
proof end;

theorem Th29: :: ROUGHS_2:29
for A being non empty finite set
for 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 )
proof end;

theorem Th30: :: ROUGHS_2:30
for A being non empty finite set
for 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 )
proof end;

:: Serial Relations
theorem Th31: :: ROUGHS_2:31
for A being non empty finite set
for 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 )
proof end;

theorem Th32: :: ROUGHS_2:32
for A being non empty finite set
for 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 )
proof end;

theorem Th33: :: ROUGHS_2:33
for A being non empty finite set
for 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 )
proof end;

theorem Th34: :: ROUGHS_2:34
for A being non empty finite set
for 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 )
proof end;

:: Reflexive binary relations
theorem :: ROUGHS_2:35
for R being non empty reflexive RelStr
for X being Subset of R holds LAp X c= X
proof end;

theorem :: ROUGHS_2:36
for R being non empty reflexive RelStr
for X being Subset of R holds X c= UAp X
proof end;

theorem Th37: :: ROUGHS_2:37
for A being non empty finite set
for 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 )
proof end;

theorem :: ROUGHS_2:38
for A being non empty finite set
for 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 )
proof end;

:: Mediate Relations
theorem Th39: :: ROUGHS_2:39
for R being non empty mediate RelStr
for X being Subset of R holds UAp X c= UAp (UAp X)
proof end;

theorem :: ROUGHS_2:40
for R being non empty mediate RelStr
for X being Subset of R holds LAp (LAp X) c= LAp X
proof end;

theorem Th41: :: ROUGHS_2:41
for A being non empty finite set
for 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 finite mediate RelStr st
( the carrier of R = A & U = UAp R )
proof end;

theorem :: ROUGHS_2:42
for A being non empty finite set
for 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 finite mediate RelStr st
( the carrier of R = A & L = LAp R )
proof end;

:: Corollaries
theorem :: ROUGHS_2:43
for A being non empty finite set
for 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 . {} = {} )
proof end;

theorem :: ROUGHS_2:44
for A being non empty finite set
for 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 )
proof end;