:: by Adam Grabowski

::

:: Received November 23, 2003

:: Copyright (c) 2003-2021 Association of Mizar Users

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

for A being RelStr holds

( A is diagonal iff the InternalRel of A c= id the carrier of A );

registration
end;

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

A is discrete

proof end;

registration

coherence

for b_{1} being reflexive RelStr st not b_{1} is discrete holds

not b_{1} is trivial
by Lm1;

coherence

for b_{1} being RelStr st b_{1} is reflexive & b_{1} is trivial holds

b_{1} is discrete
;

end;
for b

not b

coherence

for b

b

Lm2: for A being RelStr st A is discrete holds

A is diagonal

by ORDERS_3:def 1;

registration

coherence

for b_{1} being RelStr st b_{1} is discrete holds

b_{1} is diagonal
by Lm2;

coherence

for b_{1} being RelStr st not b_{1} is diagonal holds

not b_{1} is discrete
;

end;
for b

b

coherence

for b

not b

registration
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 )

( x <> y & [x,y] in the InternalRel of A )

proof end;

registration
end;

registration

let A be set ;

ex b_{1} being FinSequence of A st b_{1} is disjoint_valued

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

existence ex b

proof end;

registration

let A be non empty set ;

ex b_{1} being FinSequence of A st

( not b_{1} is empty & b_{1} is disjoint_valued )

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

existence ex b

( not b

proof 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

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

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

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

registration
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)

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 ;

end;
attr P is with_equivalence means :Def2: :: ROUGHS_1:def 2

the InternalRel of P is Equivalence_Relation of the carrier of P;

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;

the InternalRel of P is Tolerance of the carrier of P;

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

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

for P being RelStr holds

( P is with_tolerance iff the InternalRel of P is Tolerance of the carrier of P );

registration
end;

registration

existence

ex b_{1} being RelStr st

( b_{1} is discrete & b_{1} is finite & b_{1} is with_equivalence & not b_{1} is empty )

ex b_{1} being RelStr st

( not b_{1} is diagonal & b_{1} is finite & b_{1} is with_equivalence & not b_{1} is empty )

end;
ex b

( b

proof end;

existence ex b

( not b

proof end;

definition

mode Approximation_Space is non empty with_equivalence RelStr ;

mode Tolerance_Space is non empty with_tolerance RelStr ;

end;
mode Tolerance_Space is non empty with_tolerance RelStr ;

registration

let A be Tolerance_Space;

coherence

( the InternalRel of A is total & the InternalRel of A is reflexive & the InternalRel of A is symmetric ) by Def3;

end;
coherence

( the InternalRel of A is total & the InternalRel of A is reflexive & the InternalRel of A is symmetric ) by Def3;

registration
end;

definition

let A be non empty RelStr ;

let X be Subset of A;

{ x where x is Element of A : Class ( the InternalRel of A,x) c= X } is Subset of A

{ x where x is Element of A : Class ( the InternalRel of A,x) meets X } is Subset of A

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

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

{ x where x is Element of A : Class ( the InternalRel of A,x) meets X } is Subset of A

proof end;

:: deftheorem defines LAp ROUGHS_1:def 4 :

for A being non empty RelStr

for X being Subset of A holds LAp X = { x where x is Element of A : Class ( the InternalRel of A,x) c= X } ;

for A being non empty RelStr

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 non empty RelStr

for X being Subset of A holds UAp X = { x where x is Element of A : Class ( the InternalRel of A,x) meets X } ;

for A being non empty RelStr

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

:: deftheorem defines BndAp ROUGHS_1:def 6 :

for A being non empty RelStr

for X being Subset of A holds BndAp X = (UAp X) \ (LAp X);

for A being non empty RelStr

for X being Subset of A holds BndAp X = (UAp X) \ (LAp X);

:: deftheorem defines rough ROUGHS_1:def 7 :

for A being non empty RelStr

for X being Subset of A holds

( X is rough iff BndAp X <> {} );

for A being non empty RelStr

for X being Subset of A holds

( X is rough iff BndAp X <> {} );

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

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 ;

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

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 ;

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 :: ROUGHS_1:17

registration
end;

registration

let A be Approximation_Space;

let X be Subset of A;

coherence

not LAp X is rough

not UAp X is rough

end;
let X be Subset of A;

coherence

not LAp X is rough

proof end;

coherence not UAp X is rough

proof 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

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;

existence

ex b_{1} being Subset of A st b_{1} is rough

end;
existence

ex b

proof end;

definition

let A be Approximation_Space;

let X be Subset of A;

existence

ex b_{1} being set st b_{1} = [(LAp X),(UAp X)]
;

end;
let X be Subset of A;

existence

ex b

:: deftheorem defines RoughSet ROUGHS_1:def 8 :

for A being Approximation_Space

for X being Subset of A

for b_{3} being set holds

( b_{3} is RoughSet of X iff b_{3} = [(LAp X),(UAp X)] );

for A being Approximation_Space

for X being Subset of A

for b

( b

registration

let A be finite Tolerance_Space;

let x be Element of A;

coherence

not card (Class ( the InternalRel of A,x)) is empty

end;
let x be Element of A;

coherence

not card (Class ( the InternalRel of A,x)) is empty

proof end;

definition

let A be finite Tolerance_Space;

let X be Subset of A;

ex b_{1} being Function of the carrier of A,REAL st

for x being Element of A holds b_{1} . x = (card (X /\ (Class ( the InternalRel of A,x)))) / (card (Class ( the InternalRel of A,x)))

for b_{1}, b_{2} being Function of the carrier of A,REAL st ( for x being Element of A holds b_{1} . x = (card (X /\ (Class ( the InternalRel of A,x)))) / (card (Class ( the InternalRel of A,x))) ) & ( for x being Element of A holds b_{2} . x = (card (X /\ (Class ( the InternalRel of A,x)))) / (card (Class ( the InternalRel of A,x))) ) holds

b_{1} = b_{2}

end;
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 for x being Element of A holds it . x = (card (X /\ (Class ( the InternalRel of A,x)))) / (card (Class ( the InternalRel of A,x)));

ex b

for x being Element of A holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def9 defines MemberFunc ROUGHS_1:def 9 :

for A being finite Tolerance_Space

for X being Subset of A

for b_{3} being Function of the carrier of A,REAL holds

( b_{3} = MemberFunc (X,A) iff for x being Element of A holds b_{3} . x = (card (X /\ (Class ( the InternalRel of A,x)))) / (card (Class ( the InternalRel of A,x))) );

for A being finite Tolerance_Space

for X being Subset of A

for b

( b

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 )

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.]

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 )

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

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 )

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;

registration

let A be discrete Approximation_Space;

coherence

for b_{1} being Subset of A holds b_{1} is exact
by Th43;

end;
coherence

for b

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)

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

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)

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

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;

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;

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

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)

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

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;

ex b_{1} being FinSequence of REAL st

( dom b_{1} = dom X & ( for n being Nat st n in dom X holds

b_{1} . n = (MemberFunc ((X . n),A)) . x ) )

for b_{1}, b_{2} being FinSequence of REAL st dom b_{1} = dom X & ( for n being Nat st n in dom X holds

b_{1} . n = (MemberFunc ((X . n),A)) . x ) & dom b_{2} = dom X & ( for n being Nat st n in dom X holds

b_{2} . n = (MemberFunc ((X . n),A)) . x ) holds

b_{1} = b_{2}

end;
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 ( dom it = dom X & ( for n being Nat st n in dom X holds

it . n = (MemberFunc ((X . n),A)) . x ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof 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 b_{4} being FinSequence of REAL holds

( b_{4} = FinSeqM (x,X) iff ( dom b_{4} = dom X & ( for n being Nat st n in dom X holds

b_{4} . n = (MemberFunc ((X . n),A)) . x ) ) );

for A being finite Tolerance_Space

for X being FinSequence of bool the carrier of A

for x being Element of A

for b

( b

b

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)*>

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

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

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 }

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 }

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

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;

reflexivity

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

reflexivity

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

end;
let X, Y be Subset of A;

reflexivity

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

reflexivity

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

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

for A being Tolerance_Space

for X, Y being Subset of A holds

( X _c= Y iff LAp X c= LAp Y );

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

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;

reflexivity

for X being Subset of A holds

( X _c= X & X c=^ X ) ;

end;
let X, Y be Subset of A;

reflexivity

for X being Subset of A holds

( X _c= X & X c=^ X ) ;

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

for A being Tolerance_Space

for X, Y being Subset of A holds

( X _c=^ Y iff ( X _c= Y & X c=^ Y ) );

theorem :: ROUGHS_1:61

definition

let A be Tolerance_Space;

let X, Y be Subset of A;

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 ;

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 ;

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;
let X, Y be Subset of A;

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 ;

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 ;

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

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

for A being Tolerance_Space

for X, Y being Subset of A holds

( X _= Y iff LAp X = LAp Y );

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

for A being Tolerance_Space

for X, Y being Subset of A holds

( X =^ Y iff UAp X = UAp Y );

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

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;

compatibility

( X _= Y iff ( X _c= Y & Y _c= X ) )

( X =^ Y iff ( X c=^ Y & Y c=^ X ) )

( X _=^ Y iff ( X _= Y & X =^ Y ) ) ;

end;
let X, Y be Subset of A;

compatibility

( X _= Y iff ( X _c= Y & Y _c= X ) )

proof end;

compatibility ( X =^ Y iff ( X c=^ Y & Y c=^ X ) )

proof end;

compatibility ( X _=^ Y iff ( X _= Y & X =^ Y ) ) ;

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

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

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

for A being Tolerance_Space

for X, Y being Subset of A holds

( X _=^ Y iff ( X _= Y & X =^ Y ) );