let R be finite set ; :: thesis: for A, B being Subset of R holds
( JaccardIndex (A,B) = 1 iff A = B )
let A, B be Subset of R; :: thesis: ( JaccardIndex (A,B) = 1 iff A = B )
hereby :: thesis: ( A = B implies JaccardIndex (A,B) = 1 )
assume T1: JaccardIndex (A,B) = 1 ; :: thesis: A = B
per cases ( A \/ B = {} or A \/ B <> {} ) ;
suppose A \/ B = {} ; :: thesis: A = B
then ( A = {} & B = {} ) ;
hence A = B ; :: thesis: verum
end;
suppose A \/ B <> {} ; :: thesis: A = B
then JaccardIndex (A,B) = (card (A /\ B)) / (card (A \/ B)) by JacInd;
then card (A /\ B) = card (A \/ B) by XCMPLX_1:58, T1;
hence A = B by LemmaCard; :: thesis: verum
end;
end;
end;
assume A0: A = B ; :: thesis: JaccardIndex (A,B) = 1
per cases ( A = {} or A <> {} ) ;
suppose A = {} ; :: thesis: JaccardIndex (A,B) = 1
then A \/ B = {} by A0;
hence JaccardIndex (A,B) = 1 by JacInd; :: thesis: verum
end;
suppose B1: A <> {} ; :: thesis: JaccardIndex (A,B) = 1
then JaccardIndex (A,B) = (card (A /\ A)) / (card (A \/ A)) by JacInd, A0
.= (card A) / (card A) ;
hence JaccardIndex (A,B) = 1 by B1, XCMPLX_1:60; :: thesis: verum
end;
end;