:: ROUGHS_1 semantic presentation

registration

let c₁ be set ;
cluster RelStr(# a₁,(id a₁) #) -> discrete ;
coherence by ORDERS_3:def 1;

end;

theorem Th1: :: ROUGHS_1:1

for b₁ being set st Total b₁ c= id b₁ holds
b₁ is trivial

proof end;

definition

let c₁ 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 c₁ be non trivial set ;
cluster RelStr(# a₁,(Total a₁) #) -> non diagonal ;
coherence

proof end;

end;

theorem Th2: :: ROUGHS_1:2

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

proof end;

Lemma3: for b₁ being RelStr st b₁ is reflexive & b₁ is trivial holds
b₁ is discrete

proof end;

registration

cluster reflexive non discrete -> non trivial reflexive RelStr ;
coherence by Lemma3;
cluster trivial reflexive -> discrete RelStr ;
coherence by Lemma3;

end;

theorem Th3: :: ROUGHS_1:3

for b₁ being set
for b₂ being reflexive total Relation of b₁ holds id b₁ c= b₂

proof end;

Lemma4: for b₁ being RelStr st b₁ is discrete holds
b₁ is diagonal

proof end;

registration

cluster discrete -> diagonal RelStr ;
coherence by Lemma4;
cluster non diagonal -> non discrete RelStr ;
coherence by Lemma4;

end;

registration

cluster non empty non discrete non diagonal RelStr ;
existence

proof end;

end;

theorem Th4: :: ROUGHS_1:4

for b₁ being non empty non diagonal RelStr ex b₂, b₃ being Element of b₁ st
( b₂ <> b₃ & [b₂,b₃] in the InternalRel of b₁ )

proof end;

theorem Th5: :: ROUGHS_1:5

for b₁ being set
for b₂, b₃ being FinSequence of b₁ holds Union (b₂ ^ b₃) = (Union b₂) \/ (Union b₃)

proof end;

theorem Th6: :: ROUGHS_1:6

for b₁, b₂ being Function st b₂ is disjoint_valued & b₁ c= b₂ holds
b₁ is disjoint_valued

proof end;

registration

cluster empty -> disjoint_valued set ;
coherence

proof end;

end;

registration

let c₁ be set ;
cluster disjoint_valued FinSequence of a₁;
existence

proof end;

end;

Lemma8: for b₁ being set
for b₂ being Nat holds dom (b₂ |-> b₁) = Seg b₂

proof end;

registration

let c₁ be non empty set ;
cluster non empty disjoint_valued FinSequence of a₁;
existence

proof end;

end;

definition

let c₁ be set ;
let c₂ be FinSequence of bool c₁;
let c₃ be Nat;
redefine func . as c₂ . c₃ -> Subset of a₁;
coherence

proof end;

end;

definition

let c₁ be set ;
let c₂ be FinSequence of bool c₁;
redefine func Union as Union c₂ -> Subset of a₁;
coherence

proof end;

end;

registration

let c₁ be finite set ;
let c₂ be Relation of c₁;
cluster RelStr(# a₁,a₂ #) -> finite ;
coherence by GROUP_1:def 14;

end;

theorem Th7: :: ROUGHS_1:7

for b₁, b₂, b₃ being set
for b₄ being Tolerance of b₁ st b₂ in Class b₄,b₃ holds
b₃ in Class b₄,b₂

proof end;

definition

let c₁ be RelStr ;
attr a₁ is with_equivalence means :Def2: :: ROUGHS_1:def 2
the InternalRel of a₁ is Equivalence_Relation of the carrier of a₁;
attr a₁ is with_tolerance means :Def3: :: ROUGHS_1:def 3
the InternalRel of a₁ is Tolerance of the carrier of a₁;

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 RelStr ;
coherence

proof end;

end;

registration

let c₁ be set ;
cluster RelStr(# a₁,(id a₁) #) -> discrete diagonal with_equivalence with_tolerance ;
coherence by Def2;

end;

registration

cluster non empty finite discrete diagonal with_equivalence with_tolerance RelStr ;
existence

proof end;

cluster non empty finite non discrete non diagonal with_equivalence with_tolerance RelStr ;
existence

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 c₁ be Tolerance_Space;
cluster the InternalRel of a₁ -> reflexive symmetric total ;
coherence by Def3;

end;

registration

let c₁ be Approximation_Space;
cluster the InternalRel of a₁ -> reflexive symmetric transitive total ;
coherence by Def2;

end;

definition

let c₁ be Tolerance_Space;
let c₂ be Subset of c₁;
func LAp c₂ -> Subset of a₁ equals :: ROUGHS_1:def 4
{ b₁ where B is Element of a₁ : Class the InternalRel of a₁,b₁ c= a₂ } ;
coherence

proof end;

func UAp c₂ -> Subset of a₁ equals :: ROUGHS_1:def 5
{ b₁ where B is Element of a₁ : Class the InternalRel of a₁,b₁ meets a₂ } ;
coherence

proof end;

end;

:: deftheorem Def4 defines LAp ROUGHS_1:def 4 :

:: deftheorem Def5 defines UAp ROUGHS_1:def 5 :

definition

let c₁ be Tolerance_Space;
let c₂ be Subset of c₁;
func BndAp c₂ -> Subset of a₁ equals :: ROUGHS_1:def 6
(UAp a₂) \ (LAp a₂);
coherence ;

end;

:: deftheorem Def6 defines BndAp ROUGHS_1:def 6 :

definition

let c₁ be Tolerance_Space;
let c₂ be Subset of c₁;
attr a₂ is rough means :Def7: :: ROUGHS_1:def 7
BndAp a₂ <> {} ;

end;

:: deftheorem Def7 defines rough ROUGHS_1:def 7 :

notation

let c₁ be Tolerance_Space;
let c₂ be Subset of c₁;
antonym exact c₂ for rough c₂;

end;

theorem Th8: :: ROUGHS_1:8

for b₁ being Tolerance_Space
for b₂ being Subset of b₁
for b₃ being set st b₃ in LAp b₂ holds
Class the InternalRel of b₁,b₃ c= b₂

proof end;

theorem Th9: :: ROUGHS_1:9

for b₁ being Tolerance_Space
for b₂ being Subset of b₁
for b₃ being Element of b₁ st Class the InternalRel of b₁,b₃ c= b₂ holds
b₃ in LAp b₂ ;

theorem Th10: :: ROUGHS_1:10

for b₁ being Tolerance_Space
for b₂ being Subset of b₁
for b₃ being set st b₃ in UAp b₂ holds
Class the InternalRel of b₁,b₃ meets b₂

proof end;

theorem Th11: :: ROUGHS_1:11

for b₁ being Tolerance_Space
for b₂ being Subset of b₁
for b₃ being Element of b₁ st Class the InternalRel of b₁,b₃ meets b₂ holds
b₃ in UAp b₂ ;

theorem Th12: :: ROUGHS_1:12

for b₁ being Tolerance_Space
for b₂ being Subset of b₁ holds LAp b₂ c= b₂

proof end;

theorem Th13: :: ROUGHS_1:13

for b₁ being Tolerance_Space
for b₂ being Subset of b₁ holds b₂ c= UAp b₂

proof end;

theorem Th14: :: ROUGHS_1:14

for b₁ being Tolerance_Space
for b₂ being Subset of b₁ holds LAp b₂ c= UAp b₂

proof end;

theorem Th15: :: ROUGHS_1:15

for b₁ being Tolerance_Space
for b₂ being Subset of b₁ holds
( not b₂ is rough iff LAp b₂ = b₂ )

proof end;

theorem Th16: :: ROUGHS_1:16

for b₁ being Tolerance_Space
for b₂ being Subset of b₁ holds
( not b₂ is rough iff UAp b₂ = b₂ )

proof end;

theorem Th17: :: ROUGHS_1:17

for b₁ being Tolerance_Space
for b₂ being Subset of b₁ holds
( b₂ = LAp b₂ iff b₂ = UAp b₂ )

proof end;

theorem Th18: :: ROUGHS_1:18

for b₁ being Tolerance_Space holds LAp ({} b₁) = {}

proof end;

theorem Th19: :: ROUGHS_1:19

for b₁ being Tolerance_Space holds UAp ({} b₁) = {}

proof end;

theorem Th20: :: ROUGHS_1:20

for b₁ being Tolerance_Space holds LAp ([#] b₁) = [#] b₁

proof end;

theorem Th21: :: ROUGHS_1:21

for b₁ being Tolerance_Space holds UAp ([#] b₁) = [#] b₁

proof end;

theorem Th22: :: ROUGHS_1:22

for b₁ being Tolerance_Space
for b₂, b₃ being Subset of b₁ holds LAp (b₂ /\ b₃) = (LAp b₂) /\ (LAp b₃)

proof end;

theorem Th23: :: ROUGHS_1:23

for b₁ being Tolerance_Space
for b₂, b₃ being Subset of b₁ holds UAp (b₂ \/ b₃) = (UAp b₂) \/ (UAp b₃)

proof end;

theorem Th24: :: ROUGHS_1:24

for b₁ being Tolerance_Space
for b₂, b₃ being Subset of b₁ st b₂ c= b₃ holds
LAp b₂ c= LAp b₃

proof end;

theorem Th25: :: ROUGHS_1:25

for b₁ being Tolerance_Space
for b₂, b₃ being Subset of b₁ st b₂ c= b₃ holds
UAp b₂ c= UAp b₃

proof end;

theorem Th26: :: ROUGHS_1:26

for b₁ being Tolerance_Space
for b₂, b₃ being Subset of b₁ holds (LAp b₂) \/ (LAp b₃) c= LAp (b₂ \/ b₃)

proof end;

theorem Th27: :: ROUGHS_1:27

for b₁ being Tolerance_Space
for b₂, b₃ being Subset of b₁ holds UAp (b₂ /\ b₃) c= (UAp b₂) /\ (UAp b₃)

proof end;

theorem Th28: :: ROUGHS_1:28

for b₁ being Tolerance_Space
for b₂ being Subset of b₁ holds LAp (b₂ ` ) = (UAp b₂) `

proof end;

theorem Th29: :: ROUGHS_1:29

for b₁ being Tolerance_Space
for b₂ being Subset of b₁ holds UAp (b₂ ` ) = (LAp b₂) `

proof end;

theorem Th30: :: ROUGHS_1:30

for b₁ being Tolerance_Space
for b₂ being Subset of b₁ holds UAp (LAp (UAp b₂)) = UAp b₂

proof end;

theorem Th31: :: ROUGHS_1:31

for b₁ being Tolerance_Space
for b₂ being Subset of b₁ holds LAp (UAp (LAp b₂)) = LAp b₂

proof end;

theorem Th32: :: ROUGHS_1:32

for b₁ being Tolerance_Space
for b₂ being Subset of b₁ holds BndAp b₂ = BndAp (b₂ ` )

proof end;

theorem Th33: :: ROUGHS_1:33

for b₁ being Approximation_Space
for b₂ being Subset of b₁ holds LAp (LAp b₂) = LAp b₂

proof end;

theorem Th34: :: ROUGHS_1:34

for b₁ being Approximation_Space
for b₂ being Subset of b₁ holds LAp (LAp b₂) = UAp (LAp b₂)

proof end;

theorem Th35: :: ROUGHS_1:35

for b₁ being Approximation_Space
for b₂ being Subset of b₁ holds UAp (UAp b₂) = UAp b₂

proof end;

theorem Th36: :: ROUGHS_1:36

for b₁ being Approximation_Space
for b₂ being Subset of b₁ holds UAp (UAp b₂) = LAp (UAp b₂)

proof end;

registration

let c₁ be Tolerance_Space;
cluster exact Element of bool the carrier of a₁;
existence

proof end;

end;

registration

let c₁ be Approximation_Space;
let c₂ be Subset of c₁;
cluster LAp a₂ -> exact ;
coherence

proof end;

cluster UAp a₂ -> exact ;
coherence

proof end;

end;

theorem Th37: :: ROUGHS_1:37

for b₁ being Approximation_Space
for b₂ being Subset of b₁
for b₃, b₄ being set st b₃ in UAp b₂ & [b₃,b₄] in the InternalRel of b₁ holds
b₄ in UAp b₂

proof end;

registration

let c₁ be non diagonal Approximation_Space;
cluster rough Element of bool the carrier of a₁;
existence

proof end;

end;

definition

let c₁ be Approximation_Space;
let c₂ be Subset of c₁;
mode RoughSet of c₂ -> set means :: ROUGHS_1:def 8
a₃ = [(LAp a₂),(UAp a₂)];
existence ;

end;

:: deftheorem Def8 defines RoughSet ROUGHS_1:def 8 :

registration

let c₁ be finite Tolerance_Space;
let c₂ be Element of c₁;
cluster Card (Class the InternalRel of a₁,a₂) -> non empty ;
coherence

proof end;

end;

definition

let c₁ be finite Tolerance_Space;
let c₂ be Subset of c₁;
func MemberFunc c₂,c₁ -> Function of the carrier of a₁, REAL means :Def9: :: ROUGHS_1:def 9
for b₁ being Element of a₁ holds a₃ . b₁ = (card (a₂ /\ (Class the InternalRel of a₁,b₁))) / (card (Class the InternalRel of a₁,b₁));
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def9 defines MemberFunc ROUGHS_1:def 9 :

theorem Th38: :: ROUGHS_1:38

for b₁ being finite Tolerance_Space
for b₂ being Subset of b₁
for b₃ being Element of b₁ holds
( 0 <= (MemberFunc b₂,b₁) . b₃ & (MemberFunc b₂,b₁) . b₃ <= 1 )

proof end;

theorem Th39: :: ROUGHS_1:39

for b₁ being finite Tolerance_Space
for b₂ being Subset of b₁
for b₃ being Element of b₁ holds (MemberFunc b₂,b₁) . b₃ in [.0,1.]

proof end;

theorem Th40: :: ROUGHS_1:40

for b₁ being finite Approximation_Space
for b₂ being Subset of b₁
for b₃ being Element of b₁ holds
( (MemberFunc b₂,b₁) . b₃ = 1 iff b₃ in LAp b₂ )

proof end;

theorem Th41: :: ROUGHS_1:41

for b₁ being finite Approximation_Space
for b₂ being Subset of b₁
for b₃ being Element of b₁ holds
( (MemberFunc b₂,b₁) . b₃ = 0 iff b₃ in (UAp b₂) ` )

proof end;

theorem Th42: :: ROUGHS_1:42

for b₁ being finite Approximation_Space
for b₂ being Subset of b₁
for b₃ being Element of b₁ holds
( ( 0 < (MemberFunc b₂,b₁) . b₃ & (MemberFunc b₂,b₁) . b₃ < 1 ) iff b₃ in BndAp b₂ )

proof end;

theorem Th43: :: ROUGHS_1:43

for b₁ being discrete Approximation_Space
for b₂ being Subset of b₁ holds not b₂ is rough

proof end;

registration

let c₁ be discrete Approximation_Space;
cluster -> exact Element of bool the carrier of a₁;
coherence by Th43;

end;

theorem Th44: :: ROUGHS_1:44

for b₁ being finite discrete Approximation_Space
for b₂ being Subset of b₁ holds MemberFunc b₂,b₁ = chi b₂,the carrier of b₁

proof end;

theorem Th45: :: ROUGHS_1:45

for b₁ being finite Approximation_Space
for b₂ being Subset of b₁
for b₃, b₄ being set st [b₃,b₄] in the InternalRel of b₁ holds
(MemberFunc b₂,b₁) . b₃ = (MemberFunc b₂,b₁) . b₄

proof end;

theorem Th46: :: ROUGHS_1:46

for b₁ being finite Approximation_Space
for b₂ being Subset of b₁
for b₃ being Element of b₁ holds (MemberFunc (b₂ ` ),b₁) . b₃ = 1 - ((MemberFunc b₂,b₁) . b₃)

proof end;

theorem Th47: :: ROUGHS_1:47

for b₁ being finite Approximation_Space
for b₂, b₃ being Subset of b₁
for b₄ being Element of b₁ st b₂ c= b₃ holds
(MemberFunc b₂,b₁) . b₄ <= (MemberFunc b₃,b₁) . b₄

proof end;

theorem Th48: :: ROUGHS_1:48

for b₁ being finite Approximation_Space
for b₂, b₃ being Subset of b₁
for b₄ being Element of b₁ holds (MemberFunc (b₂ \/ b₃),b₁) . b₄ >= (MemberFunc b₂,b₁) . b₄

proof end;

theorem Th49: :: ROUGHS_1:49

for b₁ being finite Approximation_Space
for b₂, b₃ being Subset of b₁
for b₄ being Element of b₁ holds (MemberFunc (b₂ /\ b₃),b₁) . b₄ <= (MemberFunc b₂,b₁) . b₄

proof end;

theorem Th50: :: ROUGHS_1:50

for b₁ being finite Approximation_Space
for b₂, b₃ being Subset of b₁
for b₄ being Element of b₁ holds (MemberFunc (b₂ \/ b₃),b₁) . b₄ >= max ((MemberFunc b₂,b₁) . b₄),((MemberFunc b₃,b₁) . b₄)

proof end;

theorem Th51: :: ROUGHS_1:51

for b₁ being finite Approximation_Space
for b₂, b₃ being Subset of b₁
for b₄ being Element of b₁ st b₂ misses b₃ holds
(MemberFunc (b₂ \/ b₃),b₁) . b₄ = ((MemberFunc b₂,b₁) . b₄) + ((MemberFunc b₃,b₁) . b₄)

proof end;

theorem Th52: :: ROUGHS_1:52

for b₁ being finite Approximation_Space
for b₂, b₃ being Subset of b₁
for b₄ being Element of b₁ holds (MemberFunc (b₂ /\ b₃),b₁) . b₄ <= min ((MemberFunc b₂,b₁) . b₄),((MemberFunc b₃,b₁) . b₄)

proof end;

definition

let c₁ be finite Tolerance_Space;
let c₂ be FinSequence of bool the carrier of c₁;
let c₃ be Element of c₁;
func FinSeqM c₃,c₂ -> FinSequence of REAL means :Def10: :: ROUGHS_1:def 10
( dom a₄ = dom a₂ & ( for b₁ being Nat st b₁ in dom a₂ holds
a₄ . b₁ = (MemberFunc (a₂ . b₁),a₁) . a₃ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def10 defines FinSeqM ROUGHS_1:def 10 :

theorem Th53: :: ROUGHS_1:53

for b₁ being finite Approximation_Space
for b₂ being FinSequence of bool the carrier of b₁
for b₃ being Element of b₁
for b₄ being Subset of b₁ holds FinSeqM b₃,(b₂ ^ <*b₄*>) = (FinSeqM b₃,b₂) ^ <*((MemberFunc b₄,b₁) . b₃)*>

proof end;

theorem Th54: :: ROUGHS_1:54

for b₁ being finite Approximation_Space
for b₂ being Element of b₁ holds (MemberFunc ({} b₁),b₁) . b₂ = 0

proof end;

theorem Th55: :: ROUGHS_1:55

for b₁ being finite Approximation_Space
for b₂ being Element of b₁
for b₃ being disjoint_valued FinSequence of bool the carrier of b₁ holds (MemberFunc (Union b₃),b₁) . b₂ = Sum (FinSeqM b₂,b₃)

proof end;

theorem Th56: :: ROUGHS_1:56

for b₁ being finite Approximation_Space
for b₂ being Subset of b₁ holds LAp b₂ = { b₃ where B is Element of b₁ : (MemberFunc b₂,b₁) . b₃ = 1 }

proof end;

theorem Th57: :: ROUGHS_1:57

for b₁ being finite Approximation_Space
for b₂ being Subset of b₁ holds UAp b₂ = { b₃ where B is Element of b₁ : (MemberFunc b₂,b₁) . b₃ > 0 }

proof end;

theorem Th58: :: ROUGHS_1:58

for b₁ being finite Approximation_Space
for b₂ being Subset of b₁ holds BndAp b₂ = { b₃ where B is Element of b₁ : ( 0 < (MemberFunc b₂,b₁) . b₃ & (MemberFunc b₂,b₁) . b₃ < 1 ) }

proof end;

definition

let c₁ be Tolerance_Space;
let c₂, c₃ be Subset of c₁;
pred c₂ _c= c₃ means :Def11: :: ROUGHS_1:def 11
LAp a₂ c= LAp a₃;
pred c₂ c=^ c₃ means :Def12: :: ROUGHS_1:def 12
UAp a₂ c= UAp a₃;

end;

:: deftheorem Def11 defines _c= ROUGHS_1:def 11 :

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

definition

let c₁ be Tolerance_Space;
let c₂, c₃ be Subset of c₁;
pred c₂ _c=^ c₃ means :Def13: :: ROUGHS_1:def 13
( a₂ _c= a₃ & a₂ c=^ a₃ );

end;

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

theorem Th59: :: ROUGHS_1:59

for b₁ being Tolerance_Space
for b₂, b₃, b₄ being Subset of b₁ st b₂ _c= b₃ & b₃ _c= b₄ holds
b₂ _c= b₄

proof end;

theorem Th60: :: ROUGHS_1:60

for b₁ being Tolerance_Space
for b₂, b₃, b₄ being Subset of b₁ st b₂ c=^ b₃ & b₃ c=^ b₄ holds
b₂ c=^ b₄

proof end;

theorem Th61: :: ROUGHS_1:61

for b₁ being Tolerance_Space
for b₂, b₃, b₄ being Subset of b₁ st b₂ _c=^ b₃ & b₃ _c=^ b₄ holds
b₂ _c=^ b₄

proof end;

definition

let c₁ be Tolerance_Space;
let c₂, c₃ be Subset of c₁;
pred c₂ _= c₃ means :Def14: :: ROUGHS_1:def 14
LAp a₂ = LAp a₃;
reflexivity ;
symmetry ;
pred c₂ =^ c₃ means :Def15: :: ROUGHS_1:def 15
UAp a₂ = UAp a₃;
reflexivity ;
symmetry ;
pred c₂ _=^ c₃ means :Def16: :: ROUGHS_1:def 16
( LAp a₂ = LAp a₃ & UAp a₂ = UAp a₃ );
reflexivity ;
symmetry ;

end;

:: deftheorem Def14 defines _= ROUGHS_1:def 14 :

:: deftheorem Def15 defines =^ ROUGHS_1:def 15 :

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

definition

let c₁ be Tolerance_Space;
let c₂, c₃ be Subset of c₁;
redefine pred c₂ _= c₃ means :: ROUGHS_1:def 17
( a₂ _c= a₃ & a₃ _c= a₂ );
compatibility

proof end;

redefine pred c₂ =^ c₃ means :: ROUGHS_1:def 18
( a₂ c=^ a₃ & a₃ c=^ a₂ );
compatibility

proof end;

redefine pred c₂ _=^ c₃ means :: ROUGHS_1:def 19
( a₂ _= a₃ & a₂ =^ a₃ );
compatibility

proof end;

end;

:: deftheorem Def17 defines _= ROUGHS_1:def 17 :

:: deftheorem Def18 defines =^ ROUGHS_1:def 18 :

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