:: by Adam Grabowski

::

:: Received February 26, 2020

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

theorem :: ROUGHIF2:2

theorem HoHo: :: ROUGHIF2:3

for x1, x2 being finite set holds (2 * (card (x1 \+\ x2))) / (((card x1) + (card x2)) + (card (x1 \+\ x2))) = (card (x1 \+\ x2)) / (card (x1 \/ x2))

proof end;

theorem Lemacik: :: ROUGHIF2:5

for A, B being finite set st A \/ B <> {} holds

1 - ((card (A /\ B)) / (card (A \/ B))) = (card (A \+\ B)) / (card (A \/ B))

1 - ((card (A /\ B)) / (card (A \/ B))) = (card (A \+\ B)) / (card (A \/ B))

proof end;

registration
end;

definition

let R be finite Approximation_Space;

let f be preRIF of R;

ex b_{1} being preRIF of R st

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

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

b_{1} = b_{2}

end;
let f be preRIF of R;

func CMap f -> preRIF of R means :CDef: :: ROUGHIF2:def 1

for x, y being Subset of R holds it . (x,y) = 1 - (f . (x,y));

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

ex b

for x, y being Subset of R holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem CDef defines CMap ROUGHIF2:def 1 :

for R being finite Approximation_Space

for f, b_{3} being preRIF of R holds

( b_{3} = CMap f iff for x, y being Subset of R holds b_{3} . (x,y) = 1 - (f . (x,y)) );

for R being finite Approximation_Space

for f, b

( b

theorem PropEx3k: :: ROUGHIF2:8

for R being finite Approximation_Space

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

(CMap (kappa R)) . (X,Y) = (card (X \ Y)) / (card X)

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

(CMap (kappa R)) . (X,Y) = (card (X \ Y)) / (card X)

proof end;

theorem PropEx3k0: :: ROUGHIF2:9

for R being finite Approximation_Space

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

(CMap (kappa R)) . (X,Y) = 0

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

(CMap (kappa R)) . (X,Y) = 0

proof end;

theorem :: ROUGHIF2:10

for R being finite Approximation_Space

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

(CMap (kappa R)) . (X,Y) = kappa (X,(Y `))

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

(CMap (kappa R)) . (X,Y) = kappa (X,(Y `))

proof end;

theorem PropEx3: :: ROUGHIF2:11

for R being finite Approximation_Space

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

(CMap (kappa_1 R)) . (X,Y) = (card (X \ Y)) / (card (X \/ Y))

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

(CMap (kappa_1 R)) . (X,Y) = (card (X \ Y)) / (card (X \/ Y))

proof end;

theorem PropEx30: :: ROUGHIF2:12

for R being finite Approximation_Space

for X, Y being Subset of R st X \/ Y = {} holds

(CMap (kappa_1 R)) . (X,Y) = 0

for X, Y being Subset of R st X \/ Y = {} holds

(CMap (kappa_1 R)) . (X,Y) = 0

proof end;

theorem PropEx31: :: ROUGHIF2:13

for R being finite Approximation_Space

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

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

proof end;

Lemma1: for R being finite Approximation_Space

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

kappa (X,Y) = ((CMap (kappa_1 R)) . (X,(Y `))) / (kappa_1 ((Y `),X))

proof end;

Lemma2: for R being finite Approximation_Space

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

kappa (X,Y) = ((CMap (kappa_2 R)) . (X,(Y `))) / (kappa_2 (([#] R),X))

proof end;

theorem :: ROUGHIF2:14

for R being finite Approximation_Space

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

( kappa (X,Y) = ((CMap (kappa_1 R)) . (X,(Y `))) / (kappa_1 ((Y `),X)) & ((CMap (kappa_1 R)) . (X,(Y `))) / (kappa_1 ((Y `),X)) = ((CMap (kappa_2 R)) . (X,(Y `))) / (kappa_2 (([#] R),X)) )

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

( kappa (X,Y) = ((CMap (kappa_1 R)) . (X,(Y `))) / (kappa_1 ((Y `),X)) & ((CMap (kappa_1 R)) . (X,(Y `))) / (kappa_1 ((Y `),X)) = ((CMap (kappa_2 R)) . (X,(Y `))) / (kappa_2 (([#] R),X)) )

proof end;

:: deftheorem defines co-RIF-like ROUGHIF2:def 2 :

for R being finite Approximation_Space

for f being preRIF of R holds

( f is co-RIF-like iff CMap f is RIF of R );

for R being finite Approximation_Space

for f being preRIF of R holds

( f is co-RIF-like iff CMap f is RIF of R );

registration
end;

registration

let R be finite Approximation_Space;

ex b_{1} being preRIF of R st b_{1} is co-RIF-like

end;
cluster Relation-like V6() non empty V14([:(bool the carrier of R),(bool the carrier of R):]) V18([:(bool the carrier of R),(bool the carrier of R):],[.K89(),1.]) finite co-RIF-like for Element of bool [:[:(bool the carrier of R),(bool the carrier of R):],[.K89(),1.]:];

existence ex b

proof end;

theorem Prop6a: :: ROUGHIF2:15

for R being finite Approximation_Space

for X, Y being Subset of R

for kap being RIF of R holds

( (CMap kap) . (X,Y) = 0 iff X c= Y )

for X, Y being Subset of R

for kap being RIF of R holds

( (CMap kap) . (X,Y) = 0 iff X c= Y )

proof end;

theorem :: ROUGHIF2:16

for R being finite Approximation_Space

for X, Y being Subset of R holds

( (CMap (kappa R)) . (X,Y) = 0 iff X c= Y )

for X, Y being Subset of R holds

( (CMap (kappa R)) . (X,Y) = 0 iff X c= Y )

proof end;

theorem :: ROUGHIF2:17

for R being finite Approximation_Space

for X, Y, Z being Subset of R

for kap being RIF of R st Y c= Z holds

(CMap kap) . (X,Z) <= (CMap kap) . (X,Y)

for X, Y, Z being Subset of R

for kap being RIF of R st Y c= Z holds

(CMap kap) . (X,Z) <= (CMap kap) . (X,Y)

proof end;

theorem :: ROUGHIF2:18

for R being finite Approximation_Space

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

(CMap (kappa R)) . (X,Z) <= (CMap (kappa R)) . (X,Y)

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

(CMap (kappa R)) . (X,Z) <= (CMap (kappa R)) . (X,Y)

proof end;

Lemma6c1: for R being finite Approximation_Space

for X, Y being Subset of R holds (CMap (kappa_2 R)) . (X,Y) <= (CMap (kappa_1 R)) . (X,Y)

proof end;

Lemma6c2: for R being finite Approximation_Space

for X, Y being Subset of R holds (CMap (kappa_1 R)) . (X,Y) <= (CMap (kappa R)) . (X,Y)

proof end;

theorem :: ROUGHIF2:19

Jaga1: for R being finite Approximation_Space

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

((CMap (kappa_1 R)) . (X,Y)) + ((CMap (kappa_1 R)) . (Y,Z)) >= (CMap (kappa_1 R)) . (X,Z)

proof end;

Lack: for X, Y being set holds X \+\ Y c= X \/ Y

proof end;

Lemma6f1: for R being finite Approximation_Space

for X, Y being Subset of R st ( ( X = {} & Y <> {} ) or ( X <> {} & Y = {} ) ) holds

((CMap (kappa_1 R)) . (X,Y)) + ((CMap (kappa_1 R)) . (Y,X)) = 1

proof end;

theorem Ble1: :: ROUGHIF2:21

for R being finite Approximation_Space

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

(CMap (kappa_1 R)) . (X,Y) = 1

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

(CMap (kappa_1 R)) . (X,Y) = 1

proof end;

theorem :: ROUGHIF2:22

for R being finite Approximation_Space

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

(CMap (kappa_1 R)) . (X,Y) = 0

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

(CMap (kappa_1 R)) . (X,Y) = 0

proof end;

theorem Prop6d1: :: ROUGHIF2:23

for R being finite Approximation_Space

for X, Y, Z being Subset of R holds ((CMap (kappa_1 R)) . (X,Y)) + ((CMap (kappa_1 R)) . (Y,Z)) >= (CMap (kappa_1 R)) . (X,Z)

for X, Y, Z being Subset of R holds ((CMap (kappa_1 R)) . (X,Y)) + ((CMap (kappa_1 R)) . (Y,Z)) >= (CMap (kappa_1 R)) . (X,Z)

proof end;

::: satisfies the triangle inequality as an attribute?

theorem :: ROUGHIF2:24

theorem Prop6e1: :: ROUGHIF2:25

for R being finite Approximation_Space

for X, Y being Subset of R holds

( 0 <= ((CMap (kappa_1 R)) . (X,Y)) + ((CMap (kappa_1 R)) . (Y,X)) & ((CMap (kappa_1 R)) . (X,Y)) + ((CMap (kappa_1 R)) . (Y,X)) <= 1 )

for X, Y being Subset of R holds

( 0 <= ((CMap (kappa_1 R)) . (X,Y)) + ((CMap (kappa_1 R)) . (Y,X)) & ((CMap (kappa_1 R)) . (X,Y)) + ((CMap (kappa_1 R)) . (Y,X)) <= 1 )

proof end;

theorem Prop6e2: :: ROUGHIF2:26

for R being finite Approximation_Space

for X, Y being Subset of R holds

( 0 <= ((CMap (kappa_2 R)) . (X,Y)) + ((CMap (kappa_2 R)) . (Y,X)) & ((CMap (kappa_2 R)) . (X,Y)) + ((CMap (kappa_2 R)) . (Y,X)) <= 1 )

for X, Y being Subset of R holds

( 0 <= ((CMap (kappa_2 R)) . (X,Y)) + ((CMap (kappa_2 R)) . (Y,X)) & ((CMap (kappa_2 R)) . (X,Y)) + ((CMap (kappa_2 R)) . (Y,X)) <= 1 )

proof end;

Lemma6f: for R being finite Approximation_Space

for X, Y being Subset of R st ( ( X = {} & Y <> {} ) or ( X <> {} & Y = {} ) ) holds

((CMap (kappa R)) . (X,Y)) + ((CMap (kappa R)) . (Y,X)) = 1

proof end;

theorem :: ROUGHIF2:27

for R being finite Approximation_Space

for X, Y being Subset of R st ( ( X = {} & Y <> {} ) or ( X <> {} & Y = {} ) ) holds

( ((CMap (kappa R)) . (X,Y)) + ((CMap (kappa R)) . (Y,X)) = ((CMap (kappa_1 R)) . (X,Y)) + ((CMap (kappa_1 R)) . (Y,X)) & ((CMap (kappa_1 R)) . (X,Y)) + ((CMap (kappa_1 R)) . (Y,X)) = 1 )

for X, Y being Subset of R st ( ( X = {} & Y <> {} ) or ( X <> {} & Y = {} ) ) holds

( ((CMap (kappa R)) . (X,Y)) + ((CMap (kappa R)) . (Y,X)) = ((CMap (kappa_1 R)) . (X,Y)) + ((CMap (kappa_1 R)) . (Y,X)) & ((CMap (kappa_1 R)) . (X,Y)) + ((CMap (kappa_1 R)) . (Y,X)) = 1 )

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) = (((CMap (kappa R)) . (x,y)) + ((CMap (kappa R)) . (y,x))) / 2

for b_{1}, b_{2} being preRIF of R st ( for x, y being Subset of R holds b_{1} . (x,y) = (((CMap (kappa R)) . (x,y)) + ((CMap (kappa R)) . (y,x))) / 2 ) & ( for x, y being Subset of R holds b_{2} . (x,y) = (((CMap (kappa R)) . (x,y)) + ((CMap (kappa R)) . (y,x))) / 2 ) 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) = ((CMap (kappa_1 R)) . (x,y)) + ((CMap (kappa_1 R)) . (y,x))

for b_{1}, b_{2} being preRIF of R st ( for x, y being Subset of R holds b_{1} . (x,y) = ((CMap (kappa_1 R)) . (x,y)) + ((CMap (kappa_1 R)) . (y,x)) ) & ( for x, y being Subset of R holds b_{2} . (x,y) = ((CMap (kappa_1 R)) . (x,y)) + ((CMap (kappa_1 R)) . (y,x)) ) 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) = ((CMap (kappa_2 R)) . (x,y)) + ((CMap (kappa_2 R)) . (y,x))

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

b_{1} = b_{2}

end;
func delta_L R -> preRIF of R means :DeltaL: :: ROUGHIF2:def 3

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

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

ex b

for x, y being Subset of R holds b

proof end;

uniqueness for b

b

proof end;

func delta_1 R -> preRIF of R means :Delta1: :: ROUGHIF2:def 4

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

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

ex b

for x, y being Subset of R holds b

proof end;

uniqueness for b

b

proof end;

func delta_2 R -> preRIF of R means :Delta2: :: ROUGHIF2:def 5

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

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

ex b

for x, y being Subset of R holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem DeltaL defines delta_L ROUGHIF2:def 3 :

for R being finite Approximation_Space

for b_{2} being preRIF of R holds

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

for R being finite Approximation_Space

for b

( b

:: deftheorem Delta1 defines delta_1 ROUGHIF2:def 4 :

for R being finite Approximation_Space

for b_{2} being preRIF of R holds

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

for R being finite Approximation_Space

for b

( b

:: deftheorem Delta2 defines delta_2 ROUGHIF2:def 5 :

for R being finite Approximation_Space

for b_{2} being preRIF of R holds

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

for R being finite Approximation_Space

for b

( b

theorem :: ROUGHIF2:28

for R being finite Approximation_Space

for X, Y being Subset of R holds

( (delta_L R) . (X,Y) = 0 iff X = Y )

for X, Y being Subset of R holds

( (delta_L R) . (X,Y) = 0 iff X = Y )

proof end;

theorem :: ROUGHIF2:29

for R being finite Approximation_Space

for X, Y being Subset of R holds (delta_L R) . (X,Y) = (delta_L R) . (Y,X)

for X, Y being Subset of R holds (delta_L R) . (X,Y) = (delta_L R) . (Y,X)

proof end;

theorem :: ROUGHIF2:30

for R being finite Approximation_Space

for X, Y being Subset of R st ( ( X <> {} & Y = {} ) or ( X = {} & Y <> {} ) ) holds

(delta_L R) . (X,Y) = 1 / 2

for X, Y being Subset of R st ( ( X <> {} & Y = {} ) or ( X = {} & Y <> {} ) ) holds

(delta_L R) . (X,Y) = 1 / 2

proof end;

theorem :: ROUGHIF2:31

for R being finite Approximation_Space

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

(delta_L R) . (X,Y) = (((card (X \ Y)) / (card X)) + ((card (Y \ X)) / (card Y))) / 2

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

(delta_L R) . (X,Y) = (((card (X \ Y)) / (card X)) + ((card (Y \ X)) / (card Y))) / 2

proof end;

theorem For191: :: ROUGHIF2:32

for R being finite Approximation_Space

for X, Y being Subset of R holds (delta_1 R) . (X,Y) = (card (X \+\ Y)) / (card (X \/ Y))

for X, Y being Subset of R holds (delta_1 R) . (X,Y) = (card (X \+\ Y)) / (card (X \/ Y))

proof end;

theorem :: ROUGHIF2:33

for R being finite Approximation_Space

for X, Y being Subset of R holds (delta_2 R) . (X,Y) = (card (X \+\ Y)) / (card ([#] R))

for X, Y being Subset of R holds (delta_2 R) . (X,Y) = (card (X \+\ Y)) / (card ([#] R))

proof end;

theorem :: ROUGHIF2:34

for R being finite Approximation_Space

for X, Y, Z being Subset of R holds ((delta_1 R) . (X,Y)) + ((delta_1 R) . (Y,Z)) >= (delta_1 R) . (X,Z)

for X, Y, Z being Subset of R holds ((delta_1 R) . (X,Y)) + ((delta_1 R) . (Y,Z)) >= (delta_1 R) . (X,Z)

proof end;

theorem :: ROUGHIF2:35

for R being finite Approximation_Space

for X, Y being Subset of R holds

( (delta_1 R) . (X,Y) = 0 iff X = Y )

for X, Y being Subset of R holds

( (delta_1 R) . (X,Y) = 0 iff X = Y )

proof end;

theorem :: ROUGHIF2:36

for R being finite Approximation_Space

for X, Y being Subset of R holds (delta_1 R) . (X,Y) = (delta_1 R) . (Y,X)

for X, Y being Subset of R holds (delta_1 R) . (X,Y) = (delta_1 R) . (Y,X)

proof end;

theorem :: ROUGHIF2:37

for R being finite Approximation_Space

for X, Y being Subset of R holds

( (delta_2 R) . (X,Y) = 0 iff X = Y )

for X, Y being Subset of R holds

( (delta_2 R) . (X,Y) = 0 iff X = Y )

proof end;

theorem :: ROUGHIF2:38

for R being finite Approximation_Space

for X, Y being Subset of R holds (delta_2 R) . (X,Y) = (delta_2 R) . (Y,X)

for X, Y being Subset of R holds (delta_2 R) . (X,Y) = (delta_2 R) . (Y,X)

proof end;

theorem Prop6d2: :: ROUGHIF2:39

for R being finite Approximation_Space

for X, Y, Z being Subset of R holds ((CMap (kappa_2 R)) . (X,Y)) + ((CMap (kappa_2 R)) . (Y,Z)) >= (CMap (kappa_2 R)) . (X,Z)

for X, Y, Z being Subset of R holds ((CMap (kappa_2 R)) . (X,Y)) + ((CMap (kappa_2 R)) . (Y,Z)) >= (CMap (kappa_2 R)) . (X,Z)

proof end;

theorem :: ROUGHIF2:40

for R being finite Approximation_Space

for X, Y, Z being Subset of R holds ((delta_2 R) . (X,Y)) + ((delta_2 R) . (Y,Z)) >= (delta_2 R) . (X,Z)

for X, Y, Z being Subset of R holds ((delta_2 R) . (X,Y)) + ((delta_2 R) . (Y,Z)) >= (delta_2 R) . (X,Z)

proof end;

definition

let R be finite set ;

let A, B be Subset of R;

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

consistency

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

;

end;
let A, B be Subset of R;

func JaccardIndex (A,B) -> Element of [.0,1.] equals :JacInd: :: ROUGHIF2:def 6

(card (A /\ B)) / (card (A \/ B)) if A \/ B <> {}

otherwise 1;

coherence (card (A /\ B)) / (card (A \/ B)) if A \/ B <> {}

otherwise 1;

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

proof end;

correctness consistency

for b

;

:: deftheorem JacInd defines JaccardIndex ROUGHIF2:def 6 :

for R being finite set

for A, B being Subset of R holds

( ( A \/ B <> {} implies JaccardIndex (A,B) = (card (A /\ B)) / (card (A \/ B)) ) & ( not A \/ B <> {} implies JaccardIndex (A,B) = 1 ) );

for R being finite set

for A, B being Subset of R holds

( ( A \/ B <> {} implies JaccardIndex (A,B) = (card (A /\ B)) / (card (A \/ B)) ) & ( not A \/ B <> {} implies JaccardIndex (A,B) = 1 ) );

definition

let R be finite set ;

ex b_{1} being Function of [:(bool R),(bool R):],REAL st

for A, B being Subset of R holds b_{1} . (A,B) = 1 - (JaccardIndex (A,B))

for b_{1}, b_{2} being Function of [:(bool R),(bool R):],REAL st ( for A, B being Subset of R holds b_{1} . (A,B) = 1 - (JaccardIndex (A,B)) ) & ( for A, B being Subset of R holds b_{2} . (A,B) = 1 - (JaccardIndex (A,B)) ) holds

b_{1} = b_{2}

;

end;
func JaccardDist R -> Function of [:(bool R),(bool R):],REAL means :JacDef2: :: ROUGHIF2:def 7

for A, B being Subset of R holds it . (A,B) = 1 - (JaccardIndex (A,B));

existence for A, B being Subset of R holds it . (A,B) = 1 - (JaccardIndex (A,B));

ex b

for A, B being Subset of R holds b

proof end;

uniqueness for b

b

proof end;

correctness ;

:: deftheorem JacDef2 defines JaccardDist ROUGHIF2:def 7 :

for R being finite set

for b_{2} being Function of [:(bool R),(bool R):],REAL holds

( b_{2} = JaccardDist R iff for A, B being Subset of R holds b_{2} . (A,B) = 1 - (JaccardIndex (A,B)) );

for R being finite set

for b

( b

definition

let R be finite 1-sorted ;

JaccardDist ([#] R) is Function of [:(bool the carrier of R),(bool the carrier of R):],REAL ;

end;
func MarczewskiDistance R -> Function of [:(bool the carrier of R),(bool the carrier of R):],REAL equals :: ROUGHIF2:def 8

JaccardDist ([#] R);

coherence JaccardDist ([#] R);

JaccardDist ([#] R) is Function of [:(bool the carrier of R),(bool the carrier of R):],REAL ;

:: deftheorem defines MarczewskiDistance ROUGHIF2:def 8 :

for R being finite 1-sorted holds MarczewskiDistance R = JaccardDist ([#] R);

for R being finite 1-sorted holds MarczewskiDistance R = JaccardDist ([#] R);

definition

let X be non empty set ;

let f be Function of [:X,X:],REAL;

( f is nonnegative-yielding iff for x, y being Element of X holds f . (x,y) >= 0 )

end;
let f be Function of [:X,X:],REAL;

:: original: nonnegative-yielding

redefine attr f is nonnegative-yielding means :Non: :: ROUGHIF2:def 9

for x, y being Element of X holds f . (x,y) >= 0 ;

compatibility redefine attr f is nonnegative-yielding means :Non: :: ROUGHIF2:def 9

for x, y being Element of X holds f . (x,y) >= 0 ;

( f is nonnegative-yielding iff for x, y being Element of X holds f . (x,y) >= 0 )

proof end;

:: deftheorem Non defines nonnegative-yielding ROUGHIF2:def 9 :

for X being non empty set

for f being Function of [:X,X:],REAL holds

( f is nonnegative-yielding iff for x, y being Element of X holds f . (x,y) >= 0 );

for X being non empty set

for f being Function of [:X,X:],REAL holds

( f is nonnegative-yielding iff for x, y being Element of X holds f . (x,y) >= 0 );

registration

let X be non empty set ;

ex b_{1} being Function of [:X,X:],REAL st

( b_{1} is discerning & b_{1} is symmetric & b_{1} is Reflexive & b_{1} is triangle )

end;
cluster Relation-like V6() non empty V14([:X,X:]) V18([:X,X:], REAL ) Reflexive discerning symmetric triangle for Element of bool [:[:X,X:],REAL:];

existence ex b

( b

proof end;

registration

let X be non empty set ;

for b_{1} being Function of [:X,X:],REAL st b_{1} is Reflexive & b_{1} is symmetric & b_{1} is triangle holds

b_{1} is V154()

end;
cluster V6() V18([:X,X:], REAL ) Reflexive symmetric triangle -> V154() for Element of bool [:[:X,X:],REAL:];

coherence for b

b

proof end;

theorem ME7: :: ROUGHIF2:43

for X being non empty set

for f being V154() Reflexive discerning triangle Function of [:X,X:],REAL

for x, y being Element of X st x <> y holds

f . (x,y) > 0

for f being V154() Reflexive discerning triangle Function of [:X,X:],REAL

for x, y being Element of X st x <> y holds

f . (x,y) > 0

proof end;

definition

let X be non empty set ;

let p be Element of X;

let f be Function of [:X,X:],REAL;

ex b_{1} being Function of [:X,X:],REAL st

for x, y being Element of X holds b_{1} . (x,y) = (2 * (f . (x,y))) / (((f . (x,p)) + (f . (y,p))) + (f . (x,y)))

for b_{1}, b_{2} being Function of [:X,X:],REAL st ( for x, y being Element of X holds b_{1} . (x,y) = (2 * (f . (x,y))) / (((f . (x,p)) + (f . (y,p))) + (f . (x,y))) ) & ( for x, y being Element of X holds b_{2} . (x,y) = (2 * (f . (x,y))) / (((f . (x,p)) + (f . (y,p))) + (f . (x,y))) ) holds

b_{1} = b_{2}

end;
let p be Element of X;

let f be Function of [:X,X:],REAL;

func SteinhausGen (f,p) -> Function of [:X,X:],REAL means :SteinGen: :: ROUGHIF2:def 10

for x, y being Element of X holds it . (x,y) = (2 * (f . (x,y))) / (((f . (x,p)) + (f . (y,p))) + (f . (x,y)));

existence for x, y being Element of X holds it . (x,y) = (2 * (f . (x,y))) / (((f . (x,p)) + (f . (y,p))) + (f . (x,y)));

ex b

for x, y being Element of X holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem SteinGen defines SteinhausGen ROUGHIF2:def 10 :

for X being non empty set

for p being Element of X

for f, b_{4} being Function of [:X,X:],REAL holds

( b_{4} = SteinhausGen (f,p) iff for x, y being Element of X holds b_{4} . (x,y) = (2 * (f . (x,y))) / (((f . (x,p)) + (f . (y,p))) + (f . (x,y))) );

for X being non empty set

for p being Element of X

for f, b

( b

ZeZo: for X being non empty set

for f being V154() Function of [:X,X:],REAL

for p, x, y being Element of X holds (SteinhausGen (f,p)) . (x,y) >= 0

proof end;

registration

let X be non empty set ;

let f be V154() Function of [:X,X:],REAL;

let p be Element of X;

coherence

SteinhausGen (f,p) is nonnegative-yielding by ZeZo;

end;
let f be V154() Function of [:X,X:],REAL;

let p be Element of X;

coherence

SteinhausGen (f,p) is nonnegative-yielding by ZeZo;

registration

let X be non empty set ;

let f be V154() Reflexive Function of [:X,X:],REAL;

let p be Element of X;

coherence

SteinhausGen (f,p) is Reflexive

end;
let f be V154() Reflexive Function of [:X,X:],REAL;

let p be Element of X;

coherence

SteinhausGen (f,p) is Reflexive

proof end;

registration

let X be non empty set ;

let f be V154() discerning Function of [:X,X:],REAL;

let p be Element of X;

coherence

SteinhausGen (f,p) is discerning

end;
let f be V154() discerning Function of [:X,X:],REAL;

let p be Element of X;

coherence

SteinhausGen (f,p) is discerning

proof end;

registration

let X be non empty set ;

let f be V154() symmetric Function of [:X,X:],REAL;

let p be Element of X;

coherence

SteinhausGen (f,p) is symmetric

end;
let f be V154() symmetric Function of [:X,X:],REAL;

let p be Element of X;

coherence

SteinhausGen (f,p) is symmetric

proof end;

registration

let X be non empty set ;

let f be Reflexive discerning symmetric triangle Function of [:X,X:],REAL;

let p be Element of X;

coherence

SteinhausGen (f,p) is triangle

end;
let f be Reflexive discerning symmetric triangle Function of [:X,X:],REAL;

let p be Element of X;

coherence

SteinhausGen (f,p) is triangle

proof end;

:: Minsum Location Problem by Sp\"ath

definition

let X be finite set ;

ex b_{1} being Function of [:(bool X),(bool X):],REAL st

for x, y being Subset of X holds b_{1} . (x,y) = card (x \+\ y)

for b_{1}, b_{2} being Function of [:(bool X),(bool X):],REAL st ( for x, y being Subset of X holds b_{1} . (x,y) = card (x \+\ y) ) & ( for x, y being Subset of X holds b_{2} . (x,y) = card (x \+\ y) ) holds

b_{1} = b_{2}

end;
func SymmetricDiffDist X -> Function of [:(bool X),(bool X):],REAL means :SymDist: :: ROUGHIF2:def 11

for x, y being Subset of X holds it . (x,y) = card (x \+\ y);

existence for x, y being Subset of X holds it . (x,y) = card (x \+\ y);

ex b

for x, y being Subset of X holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem SymDist defines SymmetricDiffDist ROUGHIF2:def 11 :

for X being finite set

for b_{2} being Function of [:(bool X),(bool X):],REAL holds

( b_{2} = SymmetricDiffDist X iff for x, y being Subset of X holds b_{2} . (x,y) = card (x \+\ y) );

for X being finite set

for b

( b

registration

let X be finite set ;

coherence

( SymmetricDiffDist X is Reflexive & SymmetricDiffDist X is discerning & SymmetricDiffDist X is symmetric & SymmetricDiffDist X is triangle )

end;
coherence

( SymmetricDiffDist X is Reflexive & SymmetricDiffDist X is discerning & SymmetricDiffDist X is symmetric & SymmetricDiffDist X is triangle )

proof end;

definition

let X be finite set ;

MetrStruct(# (bool X),(SymmetricDiffDist X) #) is MetrStruct ;

end;
func SymDifMetrSpace X -> MetrStruct equals :: ROUGHIF2:def 12

MetrStruct(# (bool X),(SymmetricDiffDist X) #);

coherence MetrStruct(# (bool X),(SymmetricDiffDist X) #);

MetrStruct(# (bool X),(SymmetricDiffDist X) #) is MetrStruct ;

:: deftheorem defines SymDifMetrSpace ROUGHIF2:def 12 :

for X being finite set holds SymDifMetrSpace X = MetrStruct(# (bool X),(SymmetricDiffDist X) #);

for X being finite set holds SymDifMetrSpace X = MetrStruct(# (bool X),(SymmetricDiffDist X) #);

registration

let X be finite set ;

coherence

( SymDifMetrSpace X is Reflexive & SymDifMetrSpace X is discerning & SymDifMetrSpace X is symmetric & SymDifMetrSpace X is triangle ) by METRIC_1:def 6, METRIC_1:def 7, METRIC_1:def 8, METRIC_1:def 9;

end;
coherence

( SymDifMetrSpace X is Reflexive & SymDifMetrSpace X is discerning & SymDifMetrSpace X is symmetric & SymDifMetrSpace X is triangle ) by METRIC_1:def 6, METRIC_1:def 7, METRIC_1:def 8, METRIC_1:def 9;

theorem Similar2: :: ROUGHIF2:44

for R being finite set

for A, B being Subset of R holds (JaccardDist R) . (A,B) = (card (A \+\ B)) / (card (A \/ B))

for A, B being Subset of R holds (JaccardDist R) . (A,B) = (card (A \+\ B)) / (card (A \/ B))

proof end;

registration

let M be non empty finite MetrSpace;

coherence

( the distance of M is symmetric & the distance of M is Reflexive & the distance of M is discerning & the distance of M is triangle ) by METRIC_1:def 9, METRIC_1:def 6, METRIC_1:def 7, METRIC_1:def 8;

end;
coherence

( the distance of M is symmetric & the distance of M is Reflexive & the distance of M is discerning & the distance of M is triangle ) by METRIC_1:def 9, METRIC_1:def 6, METRIC_1:def 7, METRIC_1:def 8;

definition

let M be non empty finite MetrStruct ;

let p be Element of M;

MetrStruct(# the carrier of M,(SteinhausGen ( the distance of M,p)) #) is MetrStruct ;

end;
let p be Element of M;

func SteinhausMetrSpace (M,p) -> MetrStruct equals :: ROUGHIF2:def 13

MetrStruct(# the carrier of M,(SteinhausGen ( the distance of M,p)) #);

coherence MetrStruct(# the carrier of M,(SteinhausGen ( the distance of M,p)) #);

MetrStruct(# the carrier of M,(SteinhausGen ( the distance of M,p)) #) is MetrStruct ;

:: deftheorem defines SteinhausMetrSpace ROUGHIF2:def 13 :

for M being non empty finite MetrStruct

for p being Element of M holds SteinhausMetrSpace (M,p) = MetrStruct(# the carrier of M,(SteinhausGen ( the distance of M,p)) #);

for M being non empty finite MetrStruct

for p being Element of M holds SteinhausMetrSpace (M,p) = MetrStruct(# the carrier of M,(SteinhausGen ( the distance of M,p)) #);

definition

let M be MetrStruct ;

end;
attr M is with_nonnegative_distance means :NonDist: :: ROUGHIF2:def 14

the distance of M is nonnegative-yielding ;

the distance of M is nonnegative-yielding ;

:: deftheorem NonDist defines with_nonnegative_distance ROUGHIF2:def 14 :

for M being MetrStruct holds

( M is with_nonnegative_distance iff the distance of M is nonnegative-yielding );

for M being MetrStruct holds

( M is with_nonnegative_distance iff the distance of M is nonnegative-yielding );

registration

let A be non empty finite set ;

coherence

( discrete_dist A is finite & not discrete_dist A is empty & discrete_dist A is nonnegative-yielding )

end;
coherence

( discrete_dist A is finite & not discrete_dist A is empty & discrete_dist A is nonnegative-yielding )

proof end;

registration

ex b_{1} being MetrSpace st

( b_{1} is finite & not b_{1} is empty & b_{1} is with_nonnegative_distance )
end;

cluster non empty finite Reflexive discerning symmetric triangle with_nonnegative_distance for MetrStruct ;

existence ex b

( b

proof end;

registration

let M be non empty finite with_nonnegative_distance MetrStruct ;

let p be Element of M;

coherence

SteinhausMetrSpace (M,p) is with_nonnegative_distance

end;
let p be Element of M;

coherence

SteinhausMetrSpace (M,p) is with_nonnegative_distance

proof end;

registration

let M be non empty finite discerning with_nonnegative_distance MetrStruct ;

let p be Element of M;

coherence

SteinhausMetrSpace (M,p) is discerning

end;
let p be Element of M;

coherence

SteinhausMetrSpace (M,p) is discerning

proof end;

registration

let M be non empty finite Reflexive with_nonnegative_distance MetrStruct ;

let p be Element of M;

coherence

SteinhausMetrSpace (M,p) is Reflexive

end;
let p be Element of M;

coherence

SteinhausMetrSpace (M,p) is Reflexive

proof end;

registration

let M be non empty finite symmetric with_nonnegative_distance MetrStruct ;

let p be Element of M;

coherence

SteinhausMetrSpace (M,p) is symmetric

end;
let p be Element of M;

coherence

SteinhausMetrSpace (M,p) is symmetric

proof end;

registration

let M be non empty finite Reflexive discerning symmetric triangle MetrStruct ;

let p be Element of M;

coherence

SteinhausMetrSpace (M,p) is triangle by METRIC_1:def 9;

end;
let p be Element of M;

coherence

SteinhausMetrSpace (M,p) is triangle by METRIC_1:def 9;

registration

let R be finite 1-sorted ;

coherence

( MarczewskiDistance R is Reflexive & MarczewskiDistance R is discerning & MarczewskiDistance R is symmetric )

end;
coherence

( MarczewskiDistance R is Reflexive & MarczewskiDistance R is discerning & MarczewskiDistance R is symmetric )

proof end;

theorem :: ROUGHIF2:46

for R being finite Approximation_Space

for A, B being Subset of R holds (MarczewskiDistance R) . (A,B) = (delta_1 R) . (A,B)

for A, B being Subset of R holds (MarczewskiDistance R) . (A,B) = (delta_1 R) . (A,B)

proof end;