:: by Adam Grabowski

::

:: Received August 29, 2019

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

registration
end;

registration
end;

registration

let R be non empty 1-sorted ;

let X be Subset of R;

reducibility

([#] R) \/ X = [#] R by XBOOLE_1:12;

reducibility

([#] R) /\ X = X by XBOOLE_1:28;

end;
let X be Subset of R;

reducibility

([#] R) \/ X = [#] R by XBOOLE_1:12;

reducibility

([#] R) /\ X = X by XBOOLE_1:28;

definition

let R be finite Approximation_Space;

let X, Y be Subset of R;

( ( X <> {} implies (card (X /\ Y)) / (card X) is Element of [.0,1.] ) & ( not X <> {} implies 1 is Element of [.0,1.] ) )

for b_{1} being Element of [.0,1.] holds verum
;

end;
let X, Y be Subset of R;

func kappa (X,Y) -> Element of [.0,1.] equals :KappaDef: :: ROUGHIF1:def 1

(card (X /\ Y)) / (card X) if X <> {}

otherwise 1;

coherence (card (X /\ Y)) / (card X) if X <> {}

otherwise 1;

( ( X <> {} implies (card (X /\ Y)) / (card X) is Element of [.0,1.] ) & ( not X <> {} implies 1 is Element of [.0,1.] ) )

proof end;

consistency for b

:: deftheorem KappaDef defines kappa ROUGHIF1:def 1 :

for R being finite Approximation_Space

for X, Y being Subset of R holds

( ( X <> {} implies kappa (X,Y) = (card (X /\ Y)) / (card X) ) & ( not X <> {} implies kappa (X,Y) = 1 ) );

for R being finite Approximation_Space

for X, Y being Subset of R holds

( ( X <> {} implies kappa (X,Y) = (card (X /\ Y)) / (card X) ) & ( not X <> {} implies kappa (X,Y) = 1 ) );

theorem :: ROUGHIF1:5

theorem Prop1a: :: ROUGHIF1:6

for R being finite Approximation_Space

for X, Y being Subset of R holds

( kappa (X,Y) = 1 iff X c= Y )

for X, Y being Subset of R holds

( kappa (X,Y) = 1 iff X c= Y )

proof end;

theorem Prop1b: :: ROUGHIF1:7

for R being finite Approximation_Space

for X, Y, Z being Subset of R st Y c= Z holds

kappa (X,Y) <= kappa (X,Z)

for X, Y, Z being Subset of R st Y c= Z holds

kappa (X,Y) <= kappa (X,Z)

proof end;

theorem :: ROUGHIF1:8

for R being finite Approximation_Space

for X, Y, Z being Subset of R st Z c= Y & Y c= X holds

kappa (X,Z) <= kappa (Y,Z)

for X, Y, Z being Subset of R st Z c= Y & Y c= X holds

kappa (X,Z) <= kappa (Y,Z)

proof end;

theorem Prop1d: :: ROUGHIF1:9

for R being finite Approximation_Space

for X, Y, Z being Subset of R holds kappa (X,(Y \/ Z)) <= (kappa (X,Y)) + (kappa (X,Z))

for X, Y, Z being Subset of R holds kappa (X,(Y \/ Z)) <= (kappa (X,Y)) + (kappa (X,Z))

proof end;

theorem Prop1e: :: ROUGHIF1:10

for R being finite Approximation_Space

for X, Y, Z being Subset of R st X <> {} & Y misses Z holds

kappa (X,(Y \/ Z)) = (kappa (X,Y)) + (kappa (X,Z))

for X, Y, Z being Subset of R st X <> {} & Y misses Z holds

kappa (X,(Y \/ Z)) = (kappa (X,Y)) + (kappa (X,Z))

proof end;

definition

let R be 1-sorted ;

mode preRoughInclusionFunction of R is Function of [:(bool the carrier of R),(bool the carrier of R):],[.0,1.];

end;
mode preRoughInclusionFunction of R is Function of [:(bool the carrier of R),(bool the carrier of R):],[.0,1.];

scheme :: ROUGHIF1:sch 1

BinOpEq{ F_{1}() -> non empty 1-sorted , F_{2}( Subset of F_{1}(), Subset of F_{1}()) -> Element of [.0,1.] } :

BinOpEq{ F

for f1, f2 being preRIF of F_{1}() st ( for x, y being Subset of F_{1}() holds f1 . (x,y) = F_{2}(x,y) ) & ( for x, y being Subset of F_{1}() holds f2 . (x,y) = F_{2}(x,y) ) holds

f1 = f2

f1 = f2

proof end;

definition

let R be finite Approximation_Space;

ex b_{1} being preRIF of R st

for x, y being Subset of R holds b_{1} . (x,y) = kappa (x,y)

for b_{1}, b_{2} being preRIF of R st ( for x, y being Subset of R holds b_{1} . (x,y) = kappa (x,y) ) & ( for x, y being Subset of R holds b_{2} . (x,y) = kappa (x,y) ) holds

b_{1} = b_{2}

end;
func kappa R -> preRIF of R means :DefKappa: :: ROUGHIF1:def 2

for x, y being Subset of R holds it . (x,y) = kappa (x,y);

existence for x, y being Subset of R holds it . (x,y) = kappa (x,y);

ex b

for x, y being Subset of R holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem DefKappa defines kappa ROUGHIF1:def 2 :

for R being finite Approximation_Space

for b_{2} being preRIF of R holds

( b_{2} = kappa R iff for x, y being Subset of R holds b_{2} . (x,y) = kappa (x,y) );

for R being finite Approximation_Space

for b

( b

definition

let R be finite Approximation_Space;

let X, Y be Subset of R;

( ( X \/ Y <> {} implies (card Y) / (card (X \/ Y)) is Element of [.0,1.] ) & ( not X \/ Y <> {} implies 1 is Element of [.0,1.] ) )

for b_{1} being Element of [.0,1.] holds verum
;

(card ((X `) \/ Y)) / (card ([#] R)) is Element of [.0,1.]

end;
let X, Y be Subset of R;

func kappa_1 (X,Y) -> Element of [.0,1.] equals :Kappa1: :: ROUGHIF1:def 3

(card Y) / (card (X \/ Y)) if X \/ Y <> {}

otherwise 1;

coherence (card Y) / (card (X \/ Y)) if X \/ Y <> {}

otherwise 1;

( ( X \/ Y <> {} implies (card Y) / (card (X \/ Y)) is Element of [.0,1.] ) & ( not X \/ Y <> {} implies 1 is Element of [.0,1.] ) )

proof end;

consistency for b

func kappa_2 (X,Y) -> Element of [.0,1.] equals :: ROUGHIF1:def 4

(card ((X `) \/ Y)) / (card ([#] R));

coherence (card ((X `) \/ Y)) / (card ([#] R));

(card ((X `) \/ Y)) / (card ([#] R)) is Element of [.0,1.]

proof end;

:: deftheorem Kappa1 defines kappa_1 ROUGHIF1:def 3 :

for R being finite Approximation_Space

for X, Y being Subset of R holds

( ( X \/ Y <> {} implies kappa_1 (X,Y) = (card Y) / (card (X \/ Y)) ) & ( not X \/ Y <> {} implies kappa_1 (X,Y) = 1 ) );

for R being finite Approximation_Space

for X, Y being Subset of R holds

( ( X \/ Y <> {} implies kappa_1 (X,Y) = (card Y) / (card (X \/ Y)) ) & ( not X \/ Y <> {} implies kappa_1 (X,Y) = 1 ) );

:: deftheorem defines kappa_2 ROUGHIF1:def 4 :

for R being finite Approximation_Space

for X, Y being Subset of R holds kappa_2 (X,Y) = (card ((X `) \/ Y)) / (card ([#] R));

for R being finite Approximation_Space

for X, Y being Subset of R holds kappa_2 (X,Y) = (card ((X `) \/ Y)) / (card ([#] R));

definition

let R be finite Approximation_Space;

ex b_{1} being preRIF of R st

for x, y being Subset of R holds b_{1} . (x,y) = kappa_1 (x,y)

for b_{1}, b_{2} being preRIF of R st ( for x, y being Subset of R holds b_{1} . (x,y) = kappa_1 (x,y) ) & ( for x, y being Subset of R holds b_{2} . (x,y) = kappa_1 (x,y) ) holds

b_{1} = b_{2}

ex b_{1} being preRIF of R st

for x, y being Subset of R holds b_{1} . (x,y) = kappa_2 (x,y)

for b_{1}, b_{2} being preRIF of R st ( for x, y being Subset of R holds b_{1} . (x,y) = kappa_2 (x,y) ) & ( for x, y being Subset of R holds b_{2} . (x,y) = kappa_2 (x,y) ) holds

b_{1} = b_{2}

end;
func kappa_1 R -> preRIF of R means :DefKappa1: :: ROUGHIF1:def 5

for x, y being Subset of R holds it . (x,y) = kappa_1 (x,y);

existence for x, y being Subset of R holds it . (x,y) = kappa_1 (x,y);

ex b

for x, y being Subset of R holds b

proof end;

uniqueness for b

b

proof end;

func kappa_2 R -> preRIF of R means :DefKappa2: :: ROUGHIF1:def 6

for x, y being Subset of R holds it . (x,y) = kappa_2 (x,y);

existence for x, y being Subset of R holds it . (x,y) = kappa_2 (x,y);

ex b

for x, y being Subset of R holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem DefKappa1 defines kappa_1 ROUGHIF1:def 5 :

for R being finite Approximation_Space

for b_{2} being preRIF of R holds

( b_{2} = kappa_1 R iff for x, y being Subset of R holds b_{2} . (x,y) = kappa_1 (x,y) );

for R being finite Approximation_Space

for b

( b

:: deftheorem DefKappa2 defines kappa_2 ROUGHIF1:def 6 :

for R being finite Approximation_Space

for b_{2} being preRIF of R holds

( b_{2} = kappa_2 R iff for x, y being Subset of R holds b_{2} . (x,y) = kappa_2 (x,y) );

for R being finite Approximation_Space

for b

( b

theorem Prop11a: :: ROUGHIF1:11

for R being finite Approximation_Space

for X, Y being Subset of R holds

( kappa_1 (X,Y) = 1 iff X c= Y )

for X, Y being Subset of R holds

( kappa_1 (X,Y) = 1 iff X c= Y )

proof end;

theorem Prop11b: :: ROUGHIF1:12

for R being finite Approximation_Space

for X, Y being Subset of R holds

( kappa_2 (X,Y) = 1 iff X c= Y )

for X, Y being Subset of R holds

( kappa_2 (X,Y) = 1 iff X c= Y )

proof end;

theorem Prop4a: :: ROUGHIF1:14

for R being finite Approximation_Space

for X, Y being Subset of R st X <> {} holds

( kappa_1 (X,Y) = 0 iff Y = {} )

for X, Y being Subset of R st X <> {} holds

( kappa_1 (X,Y) = 0 iff Y = {} )

proof end;

theorem Prop4b: :: ROUGHIF1:15

for R being finite Approximation_Space

for X, Y being Subset of R holds

( kappa_2 (X,Y) = 0 iff ( X = [#] R & Y = {} ) )

for X, Y being Subset of R holds

( kappa_2 (X,Y) = 0 iff ( X = [#] R & Y = {} ) )

proof end;

theorem Prop2b: :: ROUGHIF1:16

for R being finite Approximation_Space

for X, Y, Z being Subset of R st Y c= Z holds

kappa_1 (X,Y) <= kappa_1 (X,Z)

for X, Y, Z being Subset of R st Y c= Z holds

kappa_1 (X,Y) <= kappa_1 (X,Z)

proof end;

theorem Prop3b: :: ROUGHIF1:17

for R being finite Approximation_Space

for X, Y, Z being Subset of R st Y c= Z holds

kappa_2 (X,Y) <= kappa_2 (X,Z)

for X, Y, Z being Subset of R st Y c= Z holds

kappa_2 (X,Y) <= kappa_2 (X,Z)

proof end;

definition

let R be non empty RelStr ;

let f be preRIF of R;

end;
let f be preRIF of R;

attr f is satisfying_RIF1 means :RIF1Def: :: ROUGHIF1:def 7

for X, Y being Subset of R holds

( f . (X,Y) = 1 iff X c= Y );

for X, Y being Subset of R holds

( f . (X,Y) = 1 iff X c= Y );

attr f is satisfying_RIF2 means :: ROUGHIF1:def 8

for X, Y, Z being Subset of R st Y c= Z holds

f . (X,Y) <= f . (X,Z);

for X, Y, Z being Subset of R st Y c= Z holds

f . (X,Y) <= f . (X,Z);

attr f is satisfying_RIF3 means :: ROUGHIF1:def 9

for X being Subset of R st X <> {} holds

f . (X,({} R)) = 0 ;

for X being Subset of R st X <> {} holds

f . (X,({} R)) = 0 ;

attr f is satisfying_RIF4 means :: ROUGHIF1:def 10

for X, Y being Subset of R st f . (X,Y) = 0 holds

X misses Y;

for X, Y being Subset of R st f . (X,Y) = 0 holds

X misses Y;

:: deftheorem RIF1Def defines satisfying_RIF1 ROUGHIF1:def 7 :

for R being non empty RelStr

for f being preRIF of R holds

( f is satisfying_RIF1 iff for X, Y being Subset of R holds

( f . (X,Y) = 1 iff X c= Y ) );

for R being non empty RelStr

for f being preRIF of R holds

( f is satisfying_RIF1 iff for X, Y being Subset of R holds

( f . (X,Y) = 1 iff X c= Y ) );

:: deftheorem defines satisfying_RIF2 ROUGHIF1:def 8 :

for R being non empty RelStr

for f being preRIF of R holds

( f is satisfying_RIF2 iff for X, Y, Z being Subset of R st Y c= Z holds

f . (X,Y) <= f . (X,Z) );

for R being non empty RelStr

for f being preRIF of R holds

( f is satisfying_RIF2 iff for X, Y, Z being Subset of R st Y c= Z holds

f . (X,Y) <= f . (X,Z) );

:: deftheorem defines satisfying_RIF3 ROUGHIF1:def 9 :

for R being non empty RelStr

for f being preRIF of R holds

( f is satisfying_RIF3 iff for X being Subset of R st X <> {} holds

f . (X,({} R)) = 0 );

for R being non empty RelStr

for f being preRIF of R holds

( f is satisfying_RIF3 iff for X being Subset of R st X <> {} holds

f . (X,({} R)) = 0 );

:: deftheorem defines satisfying_RIF4 ROUGHIF1:def 10 :

for R being non empty RelStr

for f being preRIF of R holds

( f is satisfying_RIF4 iff for X, Y being Subset of R st f . (X,Y) = 0 holds

X misses Y );

for R being non empty RelStr

for f being preRIF of R holds

( f is satisfying_RIF4 iff for X, Y being Subset of R st f . (X,Y) = 0 holds

X misses Y );

:: Towards weak quasi-RIFs, will be developed later on

definition

let R be non empty RelStr ;

let f be preRIF of R;

end;
let f be preRIF of R;

attr f is satisfying_RIF0 means :: ROUGHIF1:def 11

for X, Y being Subset of R st X c= Y holds

f . (X,Y) = 1;

for X, Y being Subset of R st X c= Y holds

f . (X,Y) = 1;

attr f is satisfying_RIF01 means :: ROUGHIF1:def 12

for X, Y being Subset of R st f . (X,Y) = 1 holds

X c= Y;

for X, Y being Subset of R st f . (X,Y) = 1 holds

X c= Y;

attr f is satisfying_RIF2* means :: ROUGHIF1:def 13

for X, Y, Z being Subset of R st f . (Y,Z) = 1 holds

f . (X,Y) <= f . (X,Z);

for X, Y, Z being Subset of R st f . (Y,Z) = 1 holds

f . (X,Y) <= f . (X,Z);

:: deftheorem defines satisfying_RIF0 ROUGHIF1:def 11 :

for R being non empty RelStr

for f being preRIF of R holds

( f is satisfying_RIF0 iff for X, Y being Subset of R st X c= Y holds

f . (X,Y) = 1 );

for R being non empty RelStr

for f being preRIF of R holds

( f is satisfying_RIF0 iff for X, Y being Subset of R st X c= Y holds

f . (X,Y) = 1 );

:: deftheorem defines satisfying_RIF01 ROUGHIF1:def 12 :

for R being non empty RelStr

for f being preRIF of R holds

( f is satisfying_RIF01 iff for X, Y being Subset of R st f . (X,Y) = 1 holds

X c= Y );

for R being non empty RelStr

for f being preRIF of R holds

( f is satisfying_RIF01 iff for X, Y being Subset of R st f . (X,Y) = 1 holds

X c= Y );

:: deftheorem defines satisfying_RIF2* ROUGHIF1:def 13 :

for R being non empty RelStr

for f being preRIF of R holds

( f is satisfying_RIF2* iff for X, Y, Z being Subset of R st f . (Y,Z) = 1 holds

f . (X,Y) <= f . (X,Z) );

for R being non empty RelStr

for f being preRIF of R holds

( f is satisfying_RIF2* iff for X, Y, Z being Subset of R st f . (Y,Z) = 1 holds

f . (X,Y) <= f . (X,Z) );

:: rif1 -> (rif2 iff rif2*)

:: qRifs are rif0 and rif2*

:: weak qRIFs are rif0 and rif2

:: qRifs are rif0 and rif2*

:: weak qRIFs are rif0 and rif2

registration

let R be non empty RelStr ;

for b_{1} being preRIF of R st b_{1} is satisfying_RIF1 holds

( b_{1} is satisfying_RIF0 & b_{1} is satisfying_RIF01 )
;

for b_{1} being preRIF of R st b_{1} is satisfying_RIF0 & b_{1} is satisfying_RIF01 holds

b_{1} is satisfying_RIF1
;

end;
cluster V6() V18([:(bool the carrier of R),(bool the carrier of R):],[.0,1.]) satisfying_RIF1 -> satisfying_RIF0 satisfying_RIF01 for Element of bool [:[:(bool the carrier of R),(bool the carrier of R):],[.0,1.]:];

coherence for b

( b

cluster V6() V18([:(bool the carrier of R),(bool the carrier of R):],[.0,1.]) satisfying_RIF0 satisfying_RIF01 -> satisfying_RIF1 for Element of bool [:[:(bool the carrier of R),(bool the carrier of R):],[.0,1.]:];

coherence for b

b

registration

let R be finite Approximation_Space;

coherence

kappa R is satisfying_RIF1

kappa R is satisfying_RIF2

kappa_1 R is satisfying_RIF1

kappa_1 R is satisfying_RIF2

kappa_2 R is satisfying_RIF1

kappa_2 R is satisfying_RIF2

end;
coherence

kappa R is satisfying_RIF1

proof end;

coherence kappa R is satisfying_RIF2

proof end;

coherence kappa_1 R is satisfying_RIF1

proof end;

coherence kappa_1 R is satisfying_RIF2

proof end;

coherence kappa_2 R is satisfying_RIF1

proof end;

coherence kappa_2 R is satisfying_RIF2

proof end;

registration

let R be finite Approximation_Space;

ex b_{1} being preRIF of R st

( b_{1} is satisfying_RIF1 & b_{1} is satisfying_RIF2 )

end;
cluster V6() V18([:(bool the carrier of R),(bool the carrier of R):],[.0,1.]) finite satisfying_RIF1 satisfying_RIF2 for Element of bool [:[:(bool the carrier of R),(bool the carrier of R):],[.0,1.]:];

existence ex b

( b

proof end;

theorem RIF2Iff: :: ROUGHIF1:20

for R being finite Approximation_Space

for f being satisfying_RIF1 preRIF of R holds

( f is satisfying_RIF2 iff f is satisfying_RIF2* )

for f being satisfying_RIF1 preRIF of R holds

( f is satisfying_RIF2 iff f is satisfying_RIF2* )

proof end;

registration

let R be finite Approximation_Space;

for b_{1} being satisfying_RIF1 preRIF of R st b_{1} is satisfying_RIF2 holds

b_{1} is satisfying_RIF2*
by RIF2Iff;

for b_{1} being satisfying_RIF1 preRIF of R st b_{1} is satisfying_RIF2* holds

b_{1} is satisfying_RIF2
by RIF2Iff;

end;
cluster V6() V18([:(bool the carrier of R),(bool the carrier of R):],[.0,1.]) satisfying_RIF1 satisfying_RIF2 -> satisfying_RIF1 satisfying_RIF2* for Element of bool [:[:(bool the carrier of R),(bool the carrier of R):],[.0,1.]:];

coherence for b

b

cluster V6() V18([:(bool the carrier of R),(bool the carrier of R):],[.0,1.]) satisfying_RIF1 satisfying_RIF2* -> satisfying_RIF1 satisfying_RIF2 for Element of bool [:[:(bool the carrier of R),(bool the carrier of R):],[.0,1.]:];

coherence for b

b

registration

let R be finite Approximation_Space;

coherence

( kappa R is satisfying_RIF0 & kappa R is satisfying_RIF2* ) ;

end;
coherence

( kappa R is satisfying_RIF0 & kappa R is satisfying_RIF2* ) ;

registration

let R be finite Approximation_Space;

ex b_{1} being preRoughInclusionFunction of R st

( b_{1} is satisfying_RIF0 & b_{1} is satisfying_RIF1 & b_{1} is satisfying_RIF2 & b_{1} is satisfying_RIF2* )

end;
cluster V6() V18([:(bool the carrier of R),(bool the carrier of R):],[.0,1.]) finite satisfying_RIF1 satisfying_RIF2 satisfying_RIF0 satisfying_RIF2* for Element of bool [:[:(bool the carrier of R),(bool the carrier of R):],[.0,1.]:];

existence ex b

( b

proof end;

definition

let R be finite Approximation_Space;

mode RoughInclusionFunction of R is satisfying_RIF1 satisfying_RIF2 preRoughInclusionFunction of R;

end;
mode RoughInclusionFunction of R is satisfying_RIF1 satisfying_RIF2 preRoughInclusionFunction of R;

definition

let R be finite Approximation_Space;

mode quasi-RoughInclusionFunction of R is satisfying_RIF0 satisfying_RIF2* preRIF of R;

mode weak_quasi-RoughInclusionFunction of R is satisfying_RIF2 satisfying_RIF0 preRIF of R;

end;
mode quasi-RoughInclusionFunction of R is satisfying_RIF0 satisfying_RIF2* preRIF of R;

mode weak_quasi-RoughInclusionFunction of R is satisfying_RIF2 satisfying_RIF0 preRIF of R;

definition

let R be finite Approximation_Space;

mode RIF of R is RoughInclusionFunction of R;

mode qRIF of R is quasi-RoughInclusionFunction of R;

mode wqRIF of R is weak_quasi-RoughInclusionFunction of R;

end;
mode RIF of R is RoughInclusionFunction of R;

mode qRIF of R is quasi-RoughInclusionFunction of R;

mode wqRIF of R is weak_quasi-RoughInclusionFunction of R;

:: The following three should be obvious (Proposition 3)

:: kappa R is RIF of R;

:: kappa_1 R is RIF of R;

:: kappa_2 R is RIF of R;

:: kappa R is RIF of R;

:: kappa_1 R is RIF of R;

:: kappa_2 R is RIF of R;

theorem :: ROUGHIF1:21

for R being finite Approximation_Space

for X, Z, W being Subset of R st X <> {} & Z \/ W = [#] R & Z misses W holds

(kappa (X,Z)) + (kappa (X,W)) = 1

for X, Z, W being Subset of R st X <> {} & Z \/ W = [#] R & Z misses W holds

(kappa (X,Z)) + (kappa (X,W)) = 1

proof end;

theorem LemmaProp2b: :: ROUGHIF1:22

for R being finite Approximation_Space

for X, Y being Subset of R st kappa (X,Y) = 0 holds

X misses Y

for X, Y being Subset of R st kappa (X,Y) = 0 holds

X misses Y

proof end;

theorem Prop2b: :: ROUGHIF1:23

for R being finite Approximation_Space

for X, Y being Subset of R st X <> {} holds

( kappa (X,Y) = 0 iff X misses Y )

for X, Y being Subset of R st X <> {} holds

( kappa (X,Y) = 0 iff X misses Y )

proof end;

theorem Prop2c: :: ROUGHIF1:24

for R being finite Approximation_Space

for X being Subset of R st X <> {} holds

kappa (X,({} R)) = 0

for X being Subset of R st X <> {} holds

kappa (X,({} R)) = 0

proof end;

theorem :: ROUGHIF1:25

for R being finite Approximation_Space

for X, Y, Z being Subset of R st X <> {} & X misses Y holds

( kappa (X,(Z \ Y)) = kappa (X,(Z \/ Y)) & kappa (X,(Z \/ Y)) = kappa (X,Z) )

for X, Y, Z being Subset of R st X <> {} & X misses Y holds

( kappa (X,(Z \ Y)) = kappa (X,(Z \/ Y)) & kappa (X,(Z \/ Y)) = kappa (X,Z) )

proof end;

Test1: for R being finite Approximation_Space

for Y, Z, W being Subset of R st Z misses W holds

kappa ((Y \/ Z),W) <= kappa (Y,W)

proof end;

Test2: for R being finite Approximation_Space

for Y, Z, W being Subset of R st Z misses W holds

kappa (Y,W) <= kappa ((Y \ Z),W)

proof end;

theorem :: ROUGHIF1:26

Test1AAA: for R being finite Approximation_Space

for Y, Z, W being Subset of R st Y misses Z & Z c= W holds

kappa ((Y \/ Z),W) >= kappa (Y,W)

proof end;

Test2AAA: for R being finite Approximation_Space

for Y, Z, W being Subset of R st Y misses Z & Z c= W holds

kappa (Y,W) >= kappa ((Y \ Z),W)

proof end;

theorem :: ROUGHIF1:27

registration

let R be finite Approximation_Space;

let X be non empty Subset of R;

coherence

kappa (X,({} R)) is empty by Prop2c;

end;
let X be non empty Subset of R;

coherence

kappa (X,({} R)) is empty by Prop2c;

theorem Kappa1RIF4: :: ROUGHIF1:28

for R being finite Approximation_Space

for X, Y being Subset of R st kappa_1 (X,Y) = 0 holds

X misses Y

for X, Y being Subset of R st kappa_1 (X,Y) = 0 holds

X misses Y

proof end;

theorem Kappa2RIF4: :: ROUGHIF1:29

for R being finite Approximation_Space

for X, Y being Subset of R st kappa_2 (X,Y) = 0 holds

X misses Y

for X, Y being Subset of R st kappa_2 (X,Y) = 0 holds

X misses Y

proof end;

registration

let R be finite Approximation_Space;

coherence

kappa R is satisfying_RIF4

kappa_1 R is satisfying_RIF4

kappa_2 R is satisfying_RIF4

end;
coherence

kappa R is satisfying_RIF4

proof end;

coherence kappa_1 R is satisfying_RIF4

proof end;

coherence kappa_2 R is satisfying_RIF4

proof end;

theorem :: ROUGHIF1:30

for R being finite Approximation_Space

for X, Y being Subset of R holds

( kappa (X,Y) <= kappa_1 (X,Y) & kappa_1 (X,Y) <= kappa_2 (X,Y) )

for X, Y being Subset of R holds

( kappa (X,Y) <= kappa_1 (X,Y) & kappa_1 (X,Y) <= kappa_2 (X,Y) )

proof end;

theorem :: ROUGHIF1:31

for R being finite Approximation_Space

for X, Y being Subset of R holds kappa_1 (X,Y) = kappa ((X \/ Y),Y)

for X, Y being Subset of R holds kappa_1 (X,Y) = kappa ((X \/ Y),Y)

proof end;

LemmaKap1: for R being finite Approximation_Space

for X, Y being Subset of R holds kappa (X,Y) = kappa (X,(X /\ Y))

proof end;

LemmaKap2: for R being finite Approximation_Space

for X, Y being Subset of R holds kappa_1 (X,(X /\ Y)) = kappa_1 ((X \ Y),(X /\ Y))

proof end;

LemmaKap3: for R being finite Approximation_Space

for X, Y being Subset of R holds kappa (X,(X /\ Y)) = kappa_1 (X,(X /\ Y))

proof end;

Lemma4f1: for R being finite Approximation_Space

for X, Y being Subset of R holds kappa_2 (X,Y) = kappa (([#] R),((X `) \/ Y))

proof end;

Lemma4f2: for R being finite Approximation_Space

for X, Y being Subset of R holds kappa (([#] R),((X `) \/ Y)) = (kappa (([#] R),(X `))) + (kappa (([#] R),(X /\ Y)))

proof end;

theorem :: ROUGHIF1:32

theorem :: ROUGHIF1:33

theorem :: ROUGHIF1:34

for R being finite Approximation_Space

for X, Y being Subset of R st X \/ Y = [#] R holds

kappa_1 (X,Y) = kappa_2 (X,Y)

for X, Y being Subset of R st X \/ Y = [#] R holds

kappa_1 (X,Y) = kappa_2 (X,Y)

proof end;

theorem :: ROUGHIF1:35

for R being finite Approximation_Space

for X, Y being Subset of R st X <> {} holds

1 - (kappa (X,Y)) = kappa (X,(Y `))

for X, Y being Subset of R st X <> {} holds

1 - (kappa (X,Y)) = kappa (X,(Y `))

proof end;

:: are distinct -- Example 1 and 2 translated

:: calculations in Mizar seem to be too complex, my propositions are a bit

:: shorter than in the original

:: calculations in Mizar seem to be too complex, my propositions are a bit

:: shorter than in the original

:: deftheorem defines DiscreteApproxSpace ROUGHIF1:def 14 :

for X being set holds DiscreteApproxSpace X = RelStr(# X,(id X) #);

for X being set holds DiscreteApproxSpace X = RelStr(# X,(id X) #);

definition

coherence

DiscreteApproxSpace {1,2,3,4,5} is finite strict Approximation_Space;

;

end;

func ExampleRIFSpace -> finite strict Approximation_Space equals :: ROUGHIF1:def 15

DiscreteApproxSpace {1,2,3,4,5};

correctness DiscreteApproxSpace {1,2,3,4,5};

coherence

DiscreteApproxSpace {1,2,3,4,5} is finite strict Approximation_Space;

;

:: deftheorem defines ExampleRIFSpace ROUGHIF1:def 15 :

ExampleRIFSpace = DiscreteApproxSpace {1,2,3,4,5};

ExampleRIFSpace = DiscreteApproxSpace {1,2,3,4,5};

theorem :: ROUGHIF1:36

for X, Y being Subset of ExampleRIFSpace st X = {1,2} & Y = {2,3,4} holds

kappa (X,Y) <> kappa (Y,X)

kappa (X,Y) <> kappa (Y,X)

proof end;

theorem :: ROUGHIF1:37

for X, Y, U being Subset of ExampleRIFSpace st X = {1,2} & Y = {1,2,3} & U = {2,4,5} holds

not kappa (X,U) <= kappa (Y,U)

not kappa (X,U) <= kappa (Y,U)

proof end;

theorem :: ROUGHIF1:38

for X, Y being Subset of ExampleRIFSpace st X = {1,2} & Y = {2,3,4} holds

kappa (X,Y), kappa_1 (X,Y), kappa_2 (X,Y) are_mutually_distinct

kappa (X,Y), kappa_1 (X,Y), kappa_2 (X,Y) are_mutually_distinct

proof end;

:: A Comparative Study of Some Generalized Rough Approximations"

:: Fundamenta Informaticae, 51(2002), pp. 103-119

:: Fundamenta Informaticae, 51(2002), pp. 103-119

theorem :: ROUGHIF1:39

for R being finite Approximation_Space

for u being Element of R

for x, y being Subset of R st u in (f_1 R) . x & (UncertaintyMap R) . u = y holds

kappa (y,x) > 0

for u being Element of R

for x, y being Subset of R st u in (f_1 R) . x & (UncertaintyMap R) . u = y holds

kappa (y,x) > 0

proof end;

theorem :: ROUGHIF1:40

for R being finite Approximation_Space

for u being Element of R

for x, y being Subset of R st u in (Flip (f_1 R)) . x & (UncertaintyMap R) . u = y holds

kappa (y,x) = 1

for u being Element of R

for x, y being Subset of R st u in (Flip (f_1 R)) . x & (UncertaintyMap R) . u = y holds

kappa (y,x) = 1

proof end;