:: 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 b1 being MetrSpace st
( b1 is finite & not b1 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 b1 being preRIF of R st
for x, y being Subset of R holds b1 . (x,y) = 1 - (f . (x,y))
proof end;
uniqueness
for b1, b2 being preRIF of R st ( for x, y being Subset of R holds b1 . (x,y) = 1 - (f . (x,y)) ) & ( for x, y being Subset of R holds b2 . (x,y) = 1 - (f . (x,y)) ) holds
b1 = b2
proof end;
end;

:: deftheorem CDef defines CMap ROUGHIF2:def 1 :
for R being finite Approximation_Space
for f, b3 being preRIF of R holds
( b3 = CMap f iff for x, y being Subset of R holds b3 . (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 b1 being preRIF of R st b1 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 b1 being preRIF of R st
for x, y being Subset of R holds b1 . (x,y) = (((CMap (kappa R)) . (x,y)) + ((CMap (kappa R)) . (y,x))) / 2
proof end;
uniqueness
for b1, b2 being preRIF of R st ( for x, y being Subset of R holds b1 . (x,y) = (((CMap (kappa R)) . (x,y)) + ((CMap (kappa R)) . (y,x))) / 2 ) & ( for x, y being Subset of R holds b2 . (x,y) = (((CMap (kappa R)) . (x,y)) + ((CMap (kappa R)) . (y,x))) / 2 ) holds
b1 = b2
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 b1 being preRIF of R st
for x, y being Subset of R holds b1 . (x,y) = ((CMap (kappa_1 R)) . (x,y)) + ((CMap (kappa_1 R)) . (y,x))
proof end;
uniqueness
for b1, b2 being preRIF of R st ( for x, y being Subset of R holds b1 . (x,y) = ((CMap (kappa_1 R)) . (x,y)) + ((CMap (kappa_1 R)) . (y,x)) ) & ( for x, y being Subset of R holds b2 . (x,y) = ((CMap (kappa_1 R)) . (x,y)) + ((CMap (kappa_1 R)) . (y,x)) ) holds
b1 = b2
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 b1 being preRIF of R st
for x, y being Subset of R holds b1 . (x,y) = ((CMap (kappa_2 R)) . (x,y)) + ((CMap (kappa_2 R)) . (y,x))
proof end;
uniqueness
for b1, b2 being preRIF of R st ( for x, y being Subset of R holds b1 . (x,y) = ((CMap (kappa_2 R)) . (x,y)) + ((CMap (kappa_2 R)) . (y,x)) ) & ( for x, y being Subset of R holds b2 . (x,y) = ((CMap (kappa_2 R)) . (x,y)) + ((CMap (kappa_2 R)) . (y,x)) ) holds
b1 = b2
proof end;
end;

:: deftheorem DeltaL defines delta_L ROUGHIF2:def 3 :
for R being finite Approximation_Space
for b2 being preRIF of R holds
( b2 = delta_L R iff for x, y being Subset of R holds b2 . (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 b2 being preRIF of R holds
( b2 = delta_1 R iff for x, y being Subset of R holds b2 . (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 b2 being preRIF of R holds
( b2 = delta_2 R iff for x, y being Subset of R holds b2 . (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 b1 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 b1 being Function of [:(bool R),(bool R):],REAL st
for A, B being Subset of R holds b1 . (A,B) = 1 - (JaccardIndex (A,B))
proof end;
uniqueness
for b1, b2 being Function of [:(bool R),(bool R):],REAL st ( for A, B being Subset of R holds b1 . (A,B) = 1 - (JaccardIndex (A,B)) ) & ( for A, B being Subset of R holds b2 . (A,B) = 1 - (JaccardIndex (A,B)) ) holds
b1 = b2
proof end;
correctness
;
end;

:: deftheorem JacDef2 defines JaccardDist ROUGHIF2:def 7 :
for R being finite set
for b2 being Function of [:(bool R),(bool R):],REAL holds
( b2 = JaccardDist R iff for A, B being Subset of R holds b2 . (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 b1 being Function of [:X,X:],REAL st
( b1 is discerning & b1 is symmetric & b1 is Reflexive & b1 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 b1 being Function of [:X,X:],REAL st b1 is Reflexive & b1 is symmetric & b1 is triangle holds
b1 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 b1 being Function of [:X,X:],REAL st
for x, y being Element of X holds b1 . (x,y) = (2 * (f . (x,y))) / (((f . (x,p)) + (f . (y,p))) + (f . (x,y)))
proof end;
uniqueness
for b1, b2 being Function of [:X,X:],REAL st ( for x, y being Element of X holds b1 . (x,y) = (2 * (f . (x,y))) / (((f . (x,p)) + (f . (y,p))) + (f . (x,y))) ) & ( for x, y being Element of X holds b2 . (x,y) = (2 * (f . (x,y))) / (((f . (x,p)) + (f . (y,p))) + (f . (x,y))) ) holds
b1 = b2
proof end;
end;

:: deftheorem SteinGen defines SteinhausGen ROUGHIF2:def 10 :
for X being non empty set
for p being Element of X
for f, b4 being Function of [:X,X:],REAL holds
( b4 = SteinhausGen (f,p) iff for x, y being Element of X holds b4 . (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 b1 being Function of [:(bool X),(bool X):],REAL st
for x, y being Subset of X holds b1 . (x,y) = card (x \+\ y)
proof end;
uniqueness
for b1, b2 being Function of [:(bool X),(bool X):],REAL st ( for x, y being Subset of X holds b1 . (x,y) = card (x \+\ y) ) & ( for x, y being Subset of X holds b2 . (x,y) = card (x \+\ y) ) holds
b1 = b2
proof end;
end;

:: deftheorem SymDist defines SymmetricDiffDist ROUGHIF2:def 11 :
for X being finite set
for b2 being Function of [:(bool X),(bool X):],REAL holds
( b2 = SymmetricDiffDist X iff for x, y being Subset of X holds b2 . (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 b1 being MetrSpace st
( b1 is finite & not b1 is empty & b1 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;