:: Formal Development of Rough Inclusion Functions
:: by Adam Grabowski
::
:: Received August 29, 2019
:: Copyright (c) 2019-2021 Association of Mizar Users

theorem Lemacik: :: ROUGHIF1:1

for a, b, c being Real st a <= b & b > 0 & c >= 0 holds
a / b <= (a + c) / (b + c)

proof end;

registration

cluster non empty finite strict with_equivalence with_tolerance for RelStr ;

existence
ex b₁ being Approximation_Space st
( b₁ is strict & b₁ is finite )

proof end;

end;

registration

let R be finite 1-sorted ;

cluster -> finite for Element of bool the carrier of R;

coherence
for b₁ being Subset of R holds b₁ is finite ;

end;

theorem LemmaSet: :: ROUGHIF1:2

for R being 1-sorted
for X, Y being Subset of R holds
( X c= Y iff (X `) \/ Y = [#] R )

proof end;

theorem LemmaCard: :: ROUGHIF1:3

for R being finite 1-sorted
for X, Y being Subset of R holds
( card (X \/ Y) = card Y iff X c= Y )

proof end;

theorem LemmaCard2: :: ROUGHIF1:4

for R being finite 1-sorted
for X, Y being Subset of R st card ((X `) \/ Y) = card ([#] R) holds
(X `) \/ Y = [#] R by CARD_2:102;

registration

let R be non empty 1-sorted ;
let X be Subset of R;

reduce ([#] R) \/ X to [#] R;

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

reduce ([#] R) /\ X to X;

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

end;

definition

let R be finite Approximation_Space;
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
( ( 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₁ being Element of [.0,1.] holds verum ;

end;

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

theorem :: ROUGHIF1:5

for R being finite Approximation_Space
for X being Subset of R holds kappa (({} R),X) = 1 by KappaDef;

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 )

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)

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)

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

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

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;

definition

let R be 1-sorted ;
mode preRIF of R is preRoughInclusionFunction of R;

end;

scheme :: ROUGHIF1:sch 1
BinOpEq{ F₁() -> non empty 1-sorted , F₂( Subset of F₁(), Subset of F₁()) -> Element of [.0,1.] } :

for f1, f2 being preRIF of F₁() st ( for x, y being Subset of F₁() holds f1 . (x,y) = F₂(x,y) ) & ( for x, y being Subset of F₁() holds f2 . (x,y) = F₂(x,y) ) holds
f1 = f2

proof end;

definition

let R be finite Approximation_Space;

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
ex b₁ being preRIF of R st
for x, y being Subset of R holds b₁ . (x,y) = kappa (x,y)

proof end;

uniqueness
for b₁, b₂ being preRIF of R st ( for x, y being Subset of R holds b₁ . (x,y) = kappa (x,y) ) & ( for x, y being Subset of R holds b₂ . (x,y) = kappa (x,y) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem DefKappa defines kappa ROUGHIF1:def 2 :
for R being finite Approximation_Space
for b₂ being preRIF of R holds
( b₂ = kappa R iff for x, y being Subset of R holds b₂ . (x,y) = kappa (x,y) );

definition

let R be finite Approximation_Space;
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
( ( 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₁ being Element of [.0,1.] holds verum ;

func kappa_2 (X,Y) -> Element of [.0,1.] equals :: ROUGHIF1:def 4
(card ((X `) \/ Y)) / (card ([#] R));

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

proof end;

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

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

definition

let R be finite Approximation_Space;

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
ex b₁ being preRIF of R st
for x, y being Subset of R holds b₁ . (x,y) = kappa_1 (x,y)

proof end;

uniqueness
for b₁, b₂ being preRIF of R st ( for x, y being Subset of R holds b₁ . (x,y) = kappa_1 (x,y) ) & ( for x, y being Subset of R holds b₂ . (x,y) = kappa_1 (x,y) ) holds
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
ex b₁ being preRIF of R st
for x, y being Subset of R holds b₁ . (x,y) = kappa_2 (x,y)

proof end;

uniqueness
for b₁, b₂ being preRIF of R st ( for x, y being Subset of R holds b₁ . (x,y) = kappa_2 (x,y) ) & ( for x, y being Subset of R holds b₂ . (x,y) = kappa_2 (x,y) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem DefKappa1 defines kappa_1 ROUGHIF1:def 5 :
for R being finite Approximation_Space
for b₂ being preRIF of R holds
( b₂ = kappa_1 R iff for x, y being Subset of R holds b₂ . (x,y) = kappa_1 (x,y) );

:: deftheorem DefKappa2 defines kappa_2 ROUGHIF1:def 6 :
for R being finite Approximation_Space
for b₂ being preRIF of R holds
( b₂ = kappa_2 R iff for x, y being Subset of R holds b₂ . (x,y) = kappa_2 (x,y) );

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 )

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 )

proof end;

theorem LemmaProp4a: :: ROUGHIF1:13

for R being finite Approximation_Space
for X, Y being Subset of R st kappa_1 (X,Y) = 0 holds
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 = {} )

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

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)

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)

proof end;

theorem Lemma2: :: ROUGHIF1:18

for R being finite Approximation_Space
for X being Subset of R holds kappa_1 (({} R),X) = 1

proof end;

theorem Lemma3: :: ROUGHIF1:19

for R being finite Approximation_Space
for X being Subset of R holds kappa_2 (({} R),X) = 1

proof end;

definition

let R be non empty RelStr ;
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 );

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

attr f is satisfying_RIF3 means :: ROUGHIF1:def 9
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;

end;

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

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

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

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

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

definition

let R be non empty RelStr ;
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;

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;

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

end;

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

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

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

:: rif1 -> (rif2 iff rif2*)
:: qRifs are rif0 and rif2*
:: weak qRIFs are rif0 and rif2

registration

let R be non empty RelStr ;

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₁ being preRIF of R st b₁ is satisfying_RIF1 holds
( b₁ is satisfying_RIF0 & b₁ is satisfying_RIF01 ) ;

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₁ being preRIF of R st b₁ is satisfying_RIF0 & b₁ is satisfying_RIF01 holds
b₁ is satisfying_RIF1 ;

end;

registration

let R be finite Approximation_Space;

cluster kappa R -> satisfying_RIF1 ;

coherence
kappa R is satisfying_RIF1

proof end;

cluster kappa R -> satisfying_RIF2 ;

coherence
kappa R is satisfying_RIF2

proof end;

cluster kappa_1 R -> satisfying_RIF1 ;

coherence
kappa_1 R is satisfying_RIF1

proof end;

cluster kappa_1 R -> satisfying_RIF2 ;

coherence
kappa_1 R is satisfying_RIF2

proof end;

cluster kappa_2 R -> satisfying_RIF1 ;

coherence
kappa_2 R is satisfying_RIF1

proof end;

cluster kappa_2 R -> satisfying_RIF2 ;

coherence
kappa_2 R is satisfying_RIF2

proof end;

end;

registration

let R be finite Approximation_Space;

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₁ being preRIF of R st
( b₁ is satisfying_RIF1 & b₁ is satisfying_RIF2 )

proof end;

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

proof end;

registration

let R be finite Approximation_Space;

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₁ being satisfying_RIF1 preRIF of R st b₁ is satisfying_RIF2 holds
b₁ is satisfying_RIF2* by RIF2Iff;

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₁ being satisfying_RIF1 preRIF of R st b₁ is satisfying_RIF2* holds
b₁ is satisfying_RIF2 by RIF2Iff;

end;

registration

let R be finite Approximation_Space;

cluster kappa R -> satisfying_RIF0 satisfying_RIF2* ;

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

end;

registration

let R be finite Approximation_Space;

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₁ being preRoughInclusionFunction of R st
( b₁ is satisfying_RIF0 & b₁ is satisfying_RIF1 & b₁ is satisfying_RIF2 & b₁ is satisfying_RIF2* )

proof end;

end;

definition

let R be finite Approximation_Space;
mode RoughInclusionFunction of R is satisfying_RIF1 satisfying_RIF2 preRoughInclusionFunction of R;

end;

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;

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;

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

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

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

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 )

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

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

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

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) & kappa (Y,W) <= kappa ((Y \ Z),W) ) by Test1, Test2;

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

for R being finite Approximation_Space
for Y, Z, W being Subset of R st Z misses Y & Z c= W holds
( kappa ((Y \ Z),W) <= kappa (Y,W) & kappa (Y,W) <= kappa ((Y \/ Z),W) ) by Test1AAA, Test2AAA;

registration

let R be finite Approximation_Space;
let X be non empty Subset of R;

cluster kappa (X,({} R)) -> empty ;

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

end;

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

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

proof end;

registration

let R be finite Approximation_Space;

cluster kappa R -> satisfying_RIF4 ;

coherence
kappa R is satisfying_RIF4

proof end;

cluster kappa_1 R -> satisfying_RIF4 ;

coherence
kappa_1 R is satisfying_RIF4

proof end;

cluster kappa_2 R -> satisfying_RIF4 ;

coherence
kappa_2 R is satisfying_RIF4

proof end;

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

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)

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

for R being finite Approximation_Space
for X, Y being Subset of R holds
( kappa_2 (X,Y) = kappa (([#] R),((X `) \/ Y)) & kappa (([#] R),((X `) \/ Y)) = (kappa (([#] R),(X `))) + (kappa (([#] R),(X /\ Y))) ) by Lemma4f1, Lemma4f2;

theorem :: ROUGHIF1:33

for R being finite Approximation_Space
for X, Y being Subset of R holds
( kappa (X,Y) = kappa (X,(X /\ Y)) & kappa (X,(X /\ Y)) = kappa_1 (X,(X /\ Y)) & kappa_1 (X,(X /\ Y)) = kappa_1 ((X \ Y),(X /\ Y)) ) by LemmaKap1, LemmaKap2, LemmaKap3;

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)

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

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

definition

let X be set ;

func DiscreteApproxSpace X -> strict RelStr equals :: ROUGHIF1:def 14
RelStr(# X,(id X) #);

coherence
RelStr(# X,(id X) #) is strict RelStr ;

end;

:: deftheorem defines DiscreteApproxSpace ROUGHIF1:def 14 :
for X being set holds DiscreteApproxSpace X = RelStr(# X,(id X) #);

registration

let X be set ;

cluster DiscreteApproxSpace X -> strict with_equivalence ;

coherence
DiscreteApproxSpace X is with_equivalence ;

end;

registration

let X be non empty set ;

cluster DiscreteApproxSpace X -> non empty strict ;

coherence
not DiscreteApproxSpace X is empty ;

end;

registration

let X be finite set ;

cluster DiscreteApproxSpace X -> finite strict ;

coherence
DiscreteApproxSpace X is finite ;

end;

definition

func ExampleRIFSpace -> finite strict Approximation_Space equals :: ROUGHIF1:def 15
DiscreteApproxSpace {1,2,3,4,5};

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

end;

:: deftheorem defines ExampleRIFSpace ROUGHIF1:def 15 :
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)

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)

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

proof end;

:: A Comparative Study of Some Generalized Rough Approximations"
:: 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

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

proof end;