let X be finite set ; JaccardDist X = SteinhausGen ((SymmetricDiffDist X),({} X))
set f = JaccardDist X;
set g = SteinhausGen ((SymmetricDiffDist X),({} X));
for x being Element of [:(bool X),(bool X):] holds (JaccardDist X) . x = (SteinhausGen ((SymmetricDiffDist X),({} X))) . x
proof
let x be
Element of
[:(bool X),(bool X):];
(JaccardDist X) . x = (SteinhausGen ((SymmetricDiffDist X),({} X))) . x
consider x1,
x2 being
object such that T1:
(
x1 in bool X &
x2 in bool X &
x = [x1,x2] )
by ZFMISC_1:def 2;
reconsider x1 =
x1,
x2 =
x2 as
Subset of
X by T1;
set h =
SymmetricDiffDist X;
set p =
{} X;
V1:
(SymmetricDiffDist X) . (
x1,
({} X)) =
card (x1 \+\ ({} X))
by SymDist
.=
card x1
;
V2:
(SymmetricDiffDist X) . (
x2,
({} X)) =
card (x2 \+\ ({} X))
by SymDist
.=
card x2
;
V3:
(SymmetricDiffDist X) . (
x1,
x2)
= card (x1 \+\ x2)
by SymDist;
nn:
(SteinhausGen ((SymmetricDiffDist X),({} X))) . (
x1,
x2)
= (2 * (card (x1 \+\ x2))) / (((card x1) + (card x2)) + (card (x1 \+\ x2)))
by V3, V2, V1, SteinGen;
(JaccardDist X) . (
x1,
x2) =
(card (x1 \+\ x2)) / (card (x1 \/ x2))
by Similar2
.=
(SteinhausGen ((SymmetricDiffDist X),({} X))) . (
x1,
x2)
by HoHo, nn
;
hence
(JaccardDist X) . x = (SteinhausGen ((SymmetricDiffDist X),({} X))) . x
by T1;
verum
end;
hence
JaccardDist X = SteinhausGen ((SymmetricDiffDist X),({} X))
; verum