:: Developing Complementary Rough Inclusion Functions
:: by Adam Grabowski
::
:: Received February 26, 2020
:: Copyright (c) 2020-2021 Association of Mizar Users

theorem LemacikX1: :: ROUGHIF2:1

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

proof end;

theorem :: ROUGHIF2:2

for x1, x2 being finite set holds card (x1 \+\ x2) = (card (x1 \ x2)) + (card (x2 \ x1)) by CARD_2:40, XBOOLE_1:82;

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 Jajo: :: ROUGHIF2:4

for A, B, C being set holds A \+\ C = (A \+\ B) \+\ (B \+\ C)

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

proof end;

theorem LemmaCard: :: ROUGHIF2:6

for R being finite set
for X, Y being Subset of R holds
( card (X \/ Y) = card (X /\ Y) iff X = Y )

proof end;

registration

cluster non empty finite Reflexive discerning symmetric triangle for MetrStruct ;

existence
ex b₁ being MetrSpace st
( b₁ is finite & not b₁ is empty )

proof end;

end;

definition

let R be finite Approximation_Space;
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
ex b₁ being preRIF of R st
for x, y being Subset of R holds b₁ . (x,y) = 1 - (f . (x,y))

proof end;

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

proof end;

end;

:: deftheorem CDef defines CMap ROUGHIF2:def 1 :
for R being finite Approximation_Space
for f, b₃ being preRIF of R holds
( b₃ = CMap f iff for x, y being Subset of R holds b₃ . (x,y) = 1 - (f . (x,y)) );

theorem CMapMap: :: ROUGHIF2:7

for R being finite Approximation_Space
for f being preRIF of R holds CMap (CMap f) = f

proof end;

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)

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

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

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

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

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

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

proof end;

definition

let R be finite Approximation_Space;
let f be preRIF of R;

attr f is co-RIF-like means :: ROUGHIF2:def 2
CMap f is RIF of R;

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

registration

let R be finite Approximation_Space;
let f be RIF of R;

cluster CMap f -> co-RIF-like ;

coherence
CMap f is co-RIF-like by CMapMap;

end;

registration

let R be finite Approximation_Space;

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₁ being preRIF of R st b₁ is co-RIF-like

proof end;

end;

definition

let R be finite Approximation_Space;
mode co-RIF of R is co-RIF-like preRIF of R;

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 )

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 )

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)

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)

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

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) & (CMap (kappa_1 R)) . (X,Y) <= (CMap (kappa R)) . (X,Y) ) by Lemma6c1, Lemma6c2;

theorem LemacikX: :: ROUGHIF2:20

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

proof end;

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

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

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)

proof end;

::: satisfies the triangle inequality as an attribute?

theorem :: ROUGHIF2:24

for R being finite Approximation_Space
for X, Y being Subset of R holds
( 0 <= (CMap (kappa R)) . (X,Y) & (CMap (kappa R)) . (X,Y) <= 1 ) by XXREAL_1:1;

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 )

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 )

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 )

proof end;

definition

let R be finite Approximation_Space;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

end;

:: deftheorem DeltaL defines delta_L ROUGHIF2:def 3 :
for R being finite Approximation_Space
for b₂ being preRIF of R holds
( b₂ = delta_L R iff for x, y being Subset of R holds b₂ . (x,y) = (((CMap (kappa R)) . (x,y)) + ((CMap (kappa R)) . (y,x))) / 2 );

:: deftheorem Delta1 defines delta_1 ROUGHIF2:def 4 :
for R being finite Approximation_Space
for b₂ being preRIF of R holds
( b₂ = delta_1 R iff for x, y being Subset of R holds b₂ . (x,y) = ((CMap (kappa_1 R)) . (x,y)) + ((CMap (kappa_1 R)) . (y,x)) );

:: deftheorem Delta2 defines delta_2 ROUGHIF2:def 5 :
for R being finite Approximation_Space
for b₂ being preRIF of R holds
( b₂ = delta_2 R iff for x, y being Subset of R holds b₂ . (x,y) = ((CMap (kappa_2 R)) . (x,y)) + ((CMap (kappa_2 R)) . (y,x)) );

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 )

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)

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

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

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

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

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)

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 )

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)

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 )

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)

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)

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)

proof end;

definition

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

end;

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

theorem JacRefl: :: ROUGHIF2:41

for R being finite set
for A, B being Subset of R holds
( JaccardIndex (A,B) = 1 iff A = B )

proof end;

theorem JacSym: :: ROUGHIF2:42

for R being finite set
for A, B being Subset of R holds JaccardIndex (A,B) = JaccardIndex (B,A)

proof end;

definition

let R be finite set ;

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
ex b₁ being Function of [:(bool R),(bool R):],REAL st
for A, B being Subset of R holds b₁ . (A,B) = 1 - (JaccardIndex (A,B))

proof end;

uniqueness
for b₁, b₂ being Function of [:(bool R),(bool R):],REAL st ( for A, B being Subset of R holds b₁ . (A,B) = 1 - (JaccardIndex (A,B)) ) & ( for A, B being Subset of R holds b₂ . (A,B) = 1 - (JaccardIndex (A,B)) ) holds
b₁ = b₂

proof end;

correctness
;

end;

:: deftheorem JacDef2 defines JaccardDist ROUGHIF2:def 7 :
for R being finite set
for b₂ being Function of [:(bool R),(bool R):],REAL holds
( b₂ = JaccardDist R iff for A, B being Subset of R holds b₂ . (A,B) = 1 - (JaccardIndex (A,B)) );

definition

let R be finite 1-sorted ;

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) is Function of [:(bool the carrier of R),(bool the carrier of R):],REAL ;

end;

:: deftheorem defines MarczewskiDistance ROUGHIF2:def 8 :
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;

:: 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
( f is nonnegative-yielding iff for x, y being Element of X holds f . (x,y) >= 0 )

proof end;

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

registration

let X be non empty set ;

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₁ being Function of [:X,X:],REAL st
( b₁ is discerning & b₁ is symmetric & b₁ is Reflexive & b₁ is triangle )

proof end;

end;

registration

let X be non empty set ;

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

coherence
for b₁ being Function of [:X,X:],REAL st b₁ is Reflexive & b₁ is symmetric & b₁ is triangle holds
b₁ is V154()

proof end;

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

proof end;

definition

let X be non empty set ;
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
ex b₁ being Function of [:X,X:],REAL st
for x, y being Element of X holds b₁ . (x,y) = (2 * (f . (x,y))) / (((f . (x,p)) + (f . (y,p))) + (f . (x,y)))

proof end;

uniqueness
for b₁, b₂ being Function of [:X,X:],REAL st ( for x, y being Element of X holds b₁ . (x,y) = (2 * (f . (x,y))) / (((f . (x,p)) + (f . (y,p))) + (f . (x,y))) ) & ( for x, y being Element of X holds b₂ . (x,y) = (2 * (f . (x,y))) / (((f . (x,p)) + (f . (y,p))) + (f . (x,y))) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem SteinGen defines SteinhausGen ROUGHIF2:def 10 :
for X being non empty set
for p being Element of X
for f, b₄ being Function of [:X,X:],REAL holds
( b₄ = SteinhausGen (f,p) iff for x, y being Element of X holds b₄ . (x,y) = (2 * (f . (x,y))) / (((f . (x,p)) + (f . (y,p))) + (f . (x,y))) );

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;

cluster SteinhausGen (f,p) -> V154() ;

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

end;

registration

let X be non empty set ;
let f be V154() Reflexive Function of [:X,X:],REAL;
let p be Element of X;

cluster SteinhausGen (f,p) -> Reflexive ;

coherence
SteinhausGen (f,p) is Reflexive

proof end;

end;

registration

let X be non empty set ;
let f be V154() discerning Function of [:X,X:],REAL;
let p be Element of X;

cluster SteinhausGen (f,p) -> discerning ;

coherence
SteinhausGen (f,p) is discerning

proof end;

end;

registration

let X be non empty set ;
let f be V154() symmetric Function of [:X,X:],REAL;
let p be Element of X;

cluster SteinhausGen (f,p) -> symmetric ;

coherence
SteinhausGen (f,p) is symmetric

proof end;

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;

cluster SteinhausGen (f,p) -> triangle ;

coherence
SteinhausGen (f,p) is triangle

proof end;

end;

:: Minsum Location Problem by Sp\"ath

definition

let X be finite set ;

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
ex b₁ being Function of [:(bool X),(bool X):],REAL st
for x, y being Subset of X holds b₁ . (x,y) = card (x \+\ y)

proof end;

uniqueness
for b₁, b₂ being Function of [:(bool X),(bool X):],REAL st ( for x, y being Subset of X holds b₁ . (x,y) = card (x \+\ y) ) & ( for x, y being Subset of X holds b₂ . (x,y) = card (x \+\ y) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem SymDist defines SymmetricDiffDist ROUGHIF2:def 11 :
for X being finite set
for b₂ being Function of [:(bool X),(bool X):],REAL holds
( b₂ = SymmetricDiffDist X iff for x, y being Subset of X holds b₂ . (x,y) = card (x \+\ y) );

registration

let X be finite set ;

cluster SymmetricDiffDist X -> Reflexive discerning symmetric triangle ;

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

proof end;

end;

definition

let X be finite set ;

func SymDifMetrSpace X -> MetrStruct equals :: ROUGHIF2:def 12
MetrStruct(# (bool X),(SymmetricDiffDist X) #);

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

end;

:: deftheorem defines SymDifMetrSpace ROUGHIF2:def 12 :
for X being finite set holds SymDifMetrSpace X = MetrStruct(# (bool X),(SymmetricDiffDist X) #);

registration

let X be finite set ;

cluster SymDifMetrSpace X -> non empty ;

coherence
not SymDifMetrSpace X is empty ;

end;

registration

let X be finite set ;

cluster SymDifMetrSpace X -> Reflexive discerning symmetric triangle ;

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;

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

proof end;

theorem LastLemma: :: ROUGHIF2:45

for X being finite set holds JaccardDist X = SteinhausGen ((SymmetricDiffDist X),({} X))

proof end;

registration

let M be non empty finite MetrSpace;

cluster the distance of M -> Reflexive discerning symmetric triangle ;

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;

definition

let M be non empty finite MetrStruct ;
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)) #) is MetrStruct ;

end;

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

definition

let M be MetrStruct ;

attr M is with_nonnegative_distance means :NonDist: :: ROUGHIF2:def 14
the distance of M is nonnegative-yielding ;

end;

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

registration

let A be non empty finite set ;

cluster discrete_dist A -> non empty finite V154() ;

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

proof end;

end;

registration

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

existence
ex b₁ being MetrSpace st
( b₁ is finite & not b₁ is empty & b₁ is with_nonnegative_distance )

proof end;

end;

registration

let M be non empty finite with_nonnegative_distance MetrStruct ;
let p be Element of M;

cluster SteinhausMetrSpace (M,p) -> with_nonnegative_distance ;

coherence
SteinhausMetrSpace (M,p) is with_nonnegative_distance

proof end;

end;

registration

let M be non empty finite discerning with_nonnegative_distance MetrStruct ;
let p be Element of M;

cluster SteinhausMetrSpace (M,p) -> discerning ;

coherence
SteinhausMetrSpace (M,p) is discerning

proof end;

end;

registration

let M be non empty finite Reflexive with_nonnegative_distance MetrStruct ;
let p be Element of M;

cluster SteinhausMetrSpace (M,p) -> Reflexive ;

coherence
SteinhausMetrSpace (M,p) is Reflexive

proof end;

end;

registration

let M be non empty finite symmetric with_nonnegative_distance MetrStruct ;
let p be Element of M;

cluster SteinhausMetrSpace (M,p) -> symmetric ;

coherence
SteinhausMetrSpace (M,p) is symmetric

proof end;

end;

registration

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

cluster SteinhausMetrSpace (M,p) -> triangle ;

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

end;

registration

let R be finite 1-sorted ;

cluster MarczewskiDistance R -> Reflexive discerning symmetric ;

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

proof end;

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)

proof end;

registration

let R be finite 1-sorted ;

cluster MarczewskiDistance R -> triangle ;

coherence
MarczewskiDistance R is triangle

proof end;

end;