:: ROUGHS_1 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

registration
let A be set ;
cluster RelStr(# A,(id A) #) -> discrete ;
coherence
RelStr(# A,(id A) #) is discrete
by ORDERS_3:def 1;
end;

theorem Th1: :: ROUGHS_1:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 :
for A being RelStr holds
( A is diagonal iff the InternalRel of A c= id the carrier of A );

registration
let A be non trivial set ;
cluster RelStr(# A,(Total A) #) -> non diagonal ;
coherence
not RelStr(# A,(Total A) #) is diagonal
proof end;
end;

theorem :: ROUGHS_1:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 RelStr ;
coherence
for b1 being reflexive RelStr st not b1 is discrete holds
not b1 is trivial
by Lm1;
cluster trivial reflexive -> discrete RelStr ;
coherence
for b1 being RelStr st b1 is reflexive & b1 is trivial holds
b1 is discrete
by Lm1;
end;

theorem :: ROUGHS_1:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for R being reflexive total Relation of X holds id X c= R
proof end;

Lm2: for A being RelStr st A is discrete holds
A is diagonal
proof end;

registration
cluster discrete -> diagonal RelStr ;
coherence
for b1 being RelStr st b1 is discrete holds
b1 is diagonal
by Lm2;
cluster non diagonal -> non discrete RelStr ;
coherence
for b1 being RelStr st not b1 is diagonal holds
not b1 is discrete
by Lm2;
end;

registration
cluster non empty non discrete non diagonal RelStr ;
existence
ex b1 being RelStr st
( not b1 is diagonal & not b1 is empty )
proof end;
end;

theorem Th4: :: ROUGHS_1:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being Function st q is disjoint_valued & p c= q holds
p is disjoint_valued
proof end;

registration
cluster empty -> disjoint_valued set ;
coherence
for b1 being Function st b1 is empty holds
b1 is disjoint_valued
proof end;
end;

registration
let A be set ;
cluster disjoint_valued FinSequence of A;
existence
ex b1 being FinSequence of A st b1 is disjoint_valued
proof end;
end;

Lm3: for a being set
for k being Nat holds dom (k |-> a) = Seg k
proof end;

registration
let A be non empty set ;
cluster non empty disjoint_valued FinSequence of A;
existence
ex b1 being FinSequence of A st
( not b1 is empty & b1 is disjoint_valued )
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
X . n is Subset of A
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
Union X is Subset of A
proof end;
end;

registration
let A be finite set ;
let R be Relation of A;
cluster RelStr(# A,R #) -> finite ;
coherence
RelStr(# A,R #) is finite
by GROUP_1:def 14;
end;

theorem Th7: :: ROUGHS_1:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, x, y being set
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 :
for P being RelStr holds
( P is with_equivalence iff the InternalRel of P is Equivalence_Relation of the carrier of P );

:: deftheorem Def3 defines with_tolerance ROUGHS_1:def 3 :
for P being RelStr holds
( P is with_tolerance iff the InternalRel of P is Tolerance of the carrier of P );

registration
cluster with_equivalence -> with_tolerance RelStr ;
coherence
for b1 being RelStr st b1 is with_equivalence holds
b1 is with_tolerance
proof end;
end;

registration
let A be set ;
cluster RelStr(# A,(id A) #) -> discrete diagonal with_equivalence with_tolerance ;
coherence
RelStr(# A,(id A) #) is with_equivalence
by Def2;
end;

registration
cluster non empty finite discrete diagonal with_equivalence with_tolerance RelStr ;
existence
ex b1 being RelStr st
( b1 is discrete & b1 is finite & b1 is with_equivalence & not b1 is empty )
proof end;
cluster non empty finite non discrete non diagonal with_equivalence with_tolerance RelStr ;
existence
ex b1 being RelStr st
( not b1 is diagonal & b1 is finite & b1 is with_equivalence & not b1 is empty )
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
( the InternalRel of A is total & the InternalRel of A is reflexive & the InternalRel of A is symmetric )
by Def3;
end;

registration
let A be Approximation_Space;
cluster the InternalRel of A -> reflexive symmetric transitive total ;
coherence
the InternalRel of A is transitive
by Def2;
end;

definition
let A be Tolerance_Space;
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 } ;
coherence
{ x where x is Element of A : Class the InternalRel of A,x c= X } is Subset of A
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 } ;
coherence
{ x where x is Element of A : Class the InternalRel of A,x meets X } is Subset of A
proof end;
end;

:: deftheorem defines LAp ROUGHS_1:def 4 :
for A being Tolerance_Space
for X being Subset of A holds LAp X = { x where x is Element of A : Class the InternalRel of A,x c= X } ;

:: deftheorem defines UAp ROUGHS_1:def 5 :
for A being Tolerance_Space
for X being Subset of A holds UAp X = { x where x is Element of A : Class the InternalRel of A,x meets X } ;

definition
let A be Tolerance_Space;
let X be Subset of A;
func BndAp X -> Subset of A equals :: ROUGHS_1:def 6
(UAp X) \ (LAp X);
coherence
(UAp X) \ (LAp X) is Subset of A
;
end;

:: deftheorem defines BndAp ROUGHS_1:def 6 :
for A being Tolerance_Space
for X being Subset of A holds BndAp X = (UAp X) \ (LAp X);

definition
let A be Tolerance_Space;
let X be Subset of A;
attr X is rough means :Def7: :: ROUGHS_1:def 7
BndAp X <> {} ;
end;

:: deftheorem Def7 defines rough ROUGHS_1:def 7 :
for A being Tolerance_Space
for X being Subset of A holds
( X is rough iff BndAp X <> {} );

notation
let A be Tolerance_Space;
let X be Subset of A;
antonym exact X for rough X;
end;

theorem Th8: :: ROUGHS_1:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being Tolerance_Space
for X being Subset of A
for x being set st x in LAp X holds
Class the InternalRel of A,x c= X
proof end;

theorem :: ROUGHS_1:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being Tolerance_Space
for X being Subset of A holds LAp X c= X
proof end;

theorem Th13: :: ROUGHS_1:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being Tolerance_Space
for X being Subset of A holds X c= UAp X
proof end;

theorem Th14: :: ROUGHS_1:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being Tolerance_Space
for X being Subset of A holds LAp X c= UAp X
proof end;

theorem Th15: :: ROUGHS_1:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being Tolerance_Space
for X being Subset of A holds
( not X is rough iff LAp X = X )
proof end;

theorem Th16: :: ROUGHS_1:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being Tolerance_Space
for X being Subset of A holds
( not X is rough iff UAp X = X )
proof end;

theorem :: ROUGHS_1:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being Tolerance_Space
for X being Subset of A holds
( X = LAp X iff X = UAp X )
proof end;

theorem Th18: :: ROUGHS_1:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being Tolerance_Space holds LAp ({} A) = {}
proof end;

theorem Th19: :: ROUGHS_1:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being Tolerance_Space holds UAp ({} A) = {}
proof end;

theorem Th20: :: ROUGHS_1:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being Tolerance_Space holds LAp ([#] A) = [#] A
proof end;

theorem :: ROUGHS_1:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being Tolerance_Space holds UAp ([#] A) = [#] A
proof end;

theorem :: ROUGHS_1:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being Tolerance_Space
for X being Subset of A holds LAp (X ` ) = (UAp X) `
proof end;

theorem Th29: :: ROUGHS_1:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being Tolerance_Space
for X being Subset of A holds UAp (X ` ) = (LAp X) `
proof end;

theorem :: ROUGHS_1:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being Tolerance_Space
for X being Subset of A holds UAp (LAp (UAp X)) = UAp X
proof end;

theorem :: ROUGHS_1:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being Tolerance_Space
for X being Subset of A holds LAp (UAp (LAp X)) = LAp X
proof end;

theorem :: ROUGHS_1:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being Tolerance_Space
for X being Subset of A holds BndAp X = BndAp (X ` )
proof end;

theorem :: ROUGHS_1:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being Approximation_Space
for X being Subset of A holds LAp (LAp X) = LAp X
proof end;

theorem Th34: :: ROUGHS_1:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being Approximation_Space
for X being Subset of A holds LAp (LAp X) = UAp (LAp X)
proof end;

theorem :: ROUGHS_1:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being Approximation_Space
for X being Subset of A holds UAp (UAp X) = UAp X
proof end;

theorem Th36: :: ROUGHS_1:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Element of bool the carrier of A;
existence
not for b1 being Subset of A holds b1 is rough
proof end;
end;

registration
let A be Approximation_Space;
let X be Subset of A;
cluster LAp X -> exact ;
coherence
not LAp X is rough
proof end;
cluster UAp X -> exact ;
coherence
not UAp X is rough
proof end;
end;

theorem Th37: :: ROUGHS_1:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Element of bool the carrier of A;
existence
ex b1 being Subset of A st b1 is rough
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)];
existence
ex b1 being set st b1 = [(LAp X),(UAp X)]
;
end;

:: deftheorem defines RoughSet ROUGHS_1:def 8 :
for A being Approximation_Space
for X being Subset of A
for b3 being set holds
( b3 is RoughSet of X iff b3 = [(LAp X),(UAp X)] );

registration
let A be finite Tolerance_Space;
let x be Element of A;
cluster Card (Class the InternalRel of A,x) -> non empty ;
coherence
not card (Class the InternalRel of A,x) is 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));
existence
ex b1 being Function of the carrier of A, REAL st
for x being Element of A holds b1 . x = (card (X /\ (Class the InternalRel of A,x))) / (card (Class the InternalRel of A,x))
proof end;
uniqueness
for b1, b2 being Function of the carrier of A, REAL st ( for x being Element of A holds b1 . x = (card (X /\ (Class the InternalRel of A,x))) / (card (Class the InternalRel of A,x)) ) & ( for x being Element of A holds b2 . x = (card (X /\ (Class the InternalRel of A,x))) / (card (Class the InternalRel of A,x)) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def9 defines MemberFunc ROUGHS_1:def 9 :
for A being finite Tolerance_Space
for X being Subset of A
for b3 being Function of the carrier of A, REAL holds
( b3 = MemberFunc X,A iff for x being Element of A holds b3 . x = (card (X /\ (Class the InternalRel of A,x))) / (card (Class the InternalRel of A,x)) );

theorem Th38: :: ROUGHS_1:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being discrete Approximation_Space
for X being Subset of A holds not X is rough
proof end;

registration
let A be discrete Approximation_Space;
cluster -> exact Element of bool the carrier of A;
coherence
for b1 being Subset of A holds not b1 is rough
by Th43;
end;

theorem :: ROUGHS_1:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th48: :: ROUGHS_1:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th49: :: ROUGHS_1:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: ROUGHS_1:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 ) );
existence
ex b1 being FinSequence of REAL st
( dom b1 = dom X & ( for n being Nat st n in dom X holds
b1 . n = (MemberFunc (X . n),A) . x ) )
proof end;
uniqueness
for b1, b2 being FinSequence of REAL st dom b1 = dom X & ( for n being Nat st n in dom X holds
b1 . n = (MemberFunc (X . n),A) . x ) & dom b2 = dom X & ( for n being Nat st n in dom X holds
b2 . n = (MemberFunc (X . n),A) . x ) holds
b1 = b2
proof end;
end;

:: deftheorem Def10 defines FinSeqM ROUGHS_1:def 10 :
for A being finite Tolerance_Space
for X being FinSequence of bool the carrier of A
for x being Element of A
for b4 being FinSequence of REAL holds
( b4 = FinSeqM x,X iff ( dom b4 = dom X & ( for n being Nat st n in dom X holds
b4 . n = (MemberFunc (X . n),A) . x ) ) );

theorem Th53: :: ROUGHS_1:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being finite Approximation_Space
for x being Element of A holds (MemberFunc ({} A),A) . x = 0
proof end;

theorem :: ROUGHS_1:55  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 :Def11: :: ROUGHS_1:def 11
LAp X c= LAp Y;
pred X c=^ Y means :Def12: :: ROUGHS_1:def 12
UAp X c= UAp Y;
end;

:: deftheorem Def11 defines _c= ROUGHS_1:def 11 :
for A being Tolerance_Space
for X, Y being Subset of A holds
( X _c= Y iff LAp X c= LAp Y );

:: deftheorem Def12 defines c=^ ROUGHS_1:def 12 :
for A being Tolerance_Space
for X, Y being Subset of A holds
( X c=^ Y iff UAp X c= UAp Y );

definition
let A be Tolerance_Space;
let X, Y be Subset of A;
pred X _c=^ Y means :Def13: :: ROUGHS_1:def 13
( X _c= Y & X c=^ Y );
end;

:: deftheorem Def13 defines _c=^ ROUGHS_1:def 13 :
for A being Tolerance_Space
for X, Y being Subset of A holds
( X _c=^ Y iff ( X _c= Y & X c=^ Y ) );

theorem Th59: :: ROUGHS_1:59  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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;

definition
let A be Tolerance_Space;
let X, Y be Subset of A;
pred X _= Y means :Def14: :: ROUGHS_1:def 14
LAp X = LAp Y;
reflexivity
for X being Subset of A holds LAp X = LAp X
;
symmetry
for X, Y being Subset of A st LAp X = LAp Y holds
LAp Y = LAp X
;
pred X =^ Y means :Def15: :: ROUGHS_1:def 15
UAp X = UAp Y;
reflexivity
for X being Subset of A holds UAp X = UAp X
;
symmetry
for X, Y being Subset of A st UAp X = UAp Y holds
UAp Y = UAp X
;
pred X _=^ Y means :Def16: :: ROUGHS_1:def 16
( LAp X = LAp Y & UAp X = UAp Y );
reflexivity
for X being Subset of A holds
( LAp X = LAp X & UAp X = UAp X )
;
symmetry
for X, Y being Subset of A st LAp X = LAp Y & UAp X = UAp Y holds
( LAp Y = LAp X & UAp Y = UAp X )
;
end;

:: deftheorem Def14 defines _= ROUGHS_1:def 14 :
for A being Tolerance_Space
for X, Y being Subset of A holds
( X _= Y iff LAp X = LAp Y );

:: deftheorem Def15 defines =^ ROUGHS_1:def 15 :
for A being Tolerance_Space
for X, Y being Subset of A holds
( X =^ Y iff UAp X = UAp Y );

:: deftheorem Def16 defines _=^ ROUGHS_1:def 16 :
for A being Tolerance_Space
for X, Y being Subset of A holds
( X _=^ Y iff ( LAp X = LAp Y & UAp X = UAp Y ) );

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 );
compatibility
( X _= Y iff ( X _c= Y & Y _c= X ) )
proof end;
redefine pred X =^ Y means :: ROUGHS_1:def 18
( X c=^ Y & Y c=^ X );
compatibility
( X =^ Y iff ( X c=^ Y & Y c=^ X ) )
proof end;
redefine pred X _=^ Y means :: ROUGHS_1:def 19
( X _= Y & X =^ Y );
compatibility
( X _=^ Y iff ( X _= Y & X =^ Y ) )
proof end;
end;

:: deftheorem defines _= ROUGHS_1:def 17 :
for A being Tolerance_Space
for X, Y being Subset of A holds
( X _= Y iff ( X _c= Y & Y _c= X ) );

:: deftheorem defines =^ ROUGHS_1:def 18 :
for A being Tolerance_Space
for X, Y being Subset of A holds
( X =^ Y iff ( X c=^ Y & Y c=^ X ) );

:: deftheorem defines _=^ ROUGHS_1:def 19 :
for A being Tolerance_Space
for X, Y being Subset of A holds
( X _=^ Y iff ( X _= Y & X =^ Y ) );