let P be non empty PreferenceSpace; ( P is tournament-like iff ( CharRel P is connected & CharRel P is antisymmetric & CharRel P is total ) )
A1:
( P is tournament-like implies ( CharRel P is connected & CharRel P is antisymmetric & CharRel P is total ) )
proof
assume Z0:
P is
tournament-like
;
( CharRel P is connected & CharRel P is antisymmetric & CharRel P is total )
w0:
the
PrefRel of
P is
asymmetric
by PrefDef;
for
x,
y being
object st
x <> y &
x in field (CharRel P) &
y in field (CharRel P) & not
[x,y] in CharRel P holds
[y,x] in CharRel P
proof
let x,
y be
object ;
( x <> y & x in field (CharRel P) & y in field (CharRel P) & not [x,y] in CharRel P implies [y,x] in CharRel P )
assume W1:
x <> y
;
( not x in field (CharRel P) or not y in field (CharRel P) or [x,y] in CharRel P or [y,x] in CharRel P )
t1:
(( the PrefRel of P \/ ( the PrefRel of P ~)) \/ (id the carrier of P)) \/ {} = nabla the
carrier of
P
by Z0, PrefDef;
T2:
( not
[x,y] in id the
carrier of
P & not
[y,x] in id the
carrier of
P )
by W1, RELAT_1:def 10;
assume
(
x in field (CharRel P) &
y in field (CharRel P) )
;
( [x,y] in CharRel P or [y,x] in CharRel P )
then
(
[x,y] in [: the carrier of P, the carrier of P:] &
[y,x] in [: the carrier of P, the carrier of P:] )
by ZFMISC_1:87;
then
(
[x,y] in the
PrefRel of
P \/ ( the PrefRel of P ~) &
[y,x] in the
PrefRel of
P \/ ( the PrefRel of P ~) )
by t1, T2, XBOOLE_0:def 3;
then
(
[x,y] in the
PrefRel of
P or (
[x,y] in the
PrefRel of
P ~ &
[y,x] in the
PrefRel of
P ) or
[y,x] in the
PrefRel of
P ~ )
by XBOOLE_0:def 3;
then
(
[x,y] in the
PrefRel of
P or
[y,x] in the
PrefRel of
P )
by RELAT_1:def 7;
hence
(
[x,y] in CharRel P or
[y,x] in CharRel P )
by XBOOLE_0:def 3;
verum
end;
hence
CharRel P is
connected
by LemCon;
( CharRel P is antisymmetric & CharRel P is total )
dom (CharRel P) =
(dom the PrefRel of P) \/ (dom the ToleranceRel of P)
by XTUPLE_0:23
.=
the
carrier of
P
by XBOOLE_1:12, Z0
;
hence
(
CharRel P is
antisymmetric &
CharRel P is
total )
by w0, PARTFUN1:def 2, Z0, Lemma16;
verum
end;
( CharRel P is connected & CharRel P is total & CharRel P is antisymmetric implies P is tournament-like )
proof
assume S1:
CharRel P is
connected
;
( not CharRel P is total or not CharRel P is antisymmetric or P is tournament-like )
assume S3:
CharRel P is
total
;
( not CharRel P is antisymmetric or P is tournament-like )
assume S2:
CharRel P is
antisymmetric
;
P is tournament-like
set PP = the
PrefRel of
P;
set J = the
ToleranceRel of
P;
set X = the
carrier of
P;
set I = the
InternalRel of
P;
set RT = the
PrefRel of
P \/ the
ToleranceRel of
P;
KK:
the
PrefRel of
P \/ the
ToleranceRel of
P = CharRel P
;
kk:
dom ( the PrefRel of P \/ the ToleranceRel of P) = the
carrier of
P
by PARTFUN1:def 2, S3;
then k1:
(dom ( the PrefRel of P \/ the ToleranceRel of P)) \/ (rng ( the PrefRel of P \/ the ToleranceRel of P)) = the
carrier of
P
by XBOOLE_1:12;
B0:
( the PrefRel of P \/ the ToleranceRel of P) /\ (( the PrefRel of P \/ the ToleranceRel of P) ~) c= id (dom ( the PrefRel of P \/ the ToleranceRel of P))
by RELAT_2:22, S2;
for
x,
y being
object st
[x,y] in id the
carrier of
P holds
[x,y] in ( the PrefRel of P \/ the ToleranceRel of P) /\ (( the PrefRel of P \/ the ToleranceRel of P) ~)
proof
let x,
y be
object ;
( [x,y] in id the carrier of P implies [x,y] in ( the PrefRel of P \/ the ToleranceRel of P) /\ (( the PrefRel of P \/ the ToleranceRel of P) ~) )
assume n1:
[x,y] in id the
carrier of
P
;
[x,y] in ( the PrefRel of P \/ the ToleranceRel of P) /\ (( the PrefRel of P \/ the ToleranceRel of P) ~)
then N1:
(
x in the
carrier of
P &
x = y )
by RELAT_1:def 10;
assume
not
[x,y] in ( the PrefRel of P \/ the ToleranceRel of P) /\ (( the PrefRel of P \/ the ToleranceRel of P) ~)
;
contradiction
then
( not
[x,y] in the
PrefRel of
P \/ the
ToleranceRel of
P or not
[x,y] in ( the PrefRel of P \/ the ToleranceRel of P) ~ )
by XBOOLE_0:def 4;
then
( not
[x,y] in the
PrefRel of
P \/ the
ToleranceRel of
P or not
[x,y] in ( the PrefRel of P ~) \/ ( the ToleranceRel of P ~) )
by RELAT_1:23;
then
( ( not
[x,y] in the
PrefRel of
P & not
[x,y] in the
ToleranceRel of
P ) or ( not
[x,y] in the
PrefRel of
P ~ & not
[x,y] in the
ToleranceRel of
P ~ ) )
by XBOOLE_0:def 3;
then N2:
not
[x,x] in the
ToleranceRel of
P
by N1, RELAT_1:def 7;
the
ToleranceRel of
P is
total
by PrefDef;
then N3:
dom the
ToleranceRel of
P = the
carrier of
P
by PARTFUN1:def 2;
field the
ToleranceRel of
P =
(dom the ToleranceRel of P) \/ (rng the ToleranceRel of P)
.=
the
carrier of
P
by N3, XBOOLE_1:12
;
then N4:
x in field the
ToleranceRel of
P
by n1, RELAT_1:def 10;
the
ToleranceRel of
P is
reflexive
by PrefDef;
hence
contradiction
by N2, N4, RELAT_2:def 1, RELAT_2:def 9;
verum
end;
then
id the
carrier of
P c= ( the PrefRel of P \/ the ToleranceRel of P) /\ (( the PrefRel of P \/ the ToleranceRel of P) ~)
by RELAT_1:def 3;
then B1:
( the PrefRel of P \/ the ToleranceRel of P) /\ (( the PrefRel of P \/ the ToleranceRel of P) ~) = id the
carrier of
P
by B0, XBOOLE_0:def 10, kk;
Y1:
( the PrefRel of P \/ the ToleranceRel of P) ~ = ( the PrefRel of P ~) \/ ( the ToleranceRel of P ~)
by RELAT_1:23;
the
ToleranceRel of
P is
symmetric
by PrefDef;
then
( the PrefRel of P \/ the ToleranceRel of P) /\ (( the PrefRel of P ~) \/ the ToleranceRel of P) = id the
carrier of
P
by B1, Y1, RELAT_2:13;
then Y3:
( the PrefRel of P /\ ( the PrefRel of P ~)) \/ the
ToleranceRel of
P = id the
carrier of
P
by XBOOLE_1:24;
the
PrefRel of
P is
asymmetric
by PrefDef;
then a3:
the
PrefRel of
P /\ ( the PrefRel of P ~) = {}
by Lemma17, XBOOLE_0:def 7;
[:(field ( the PrefRel of P \/ the ToleranceRel of P)),(field ( the PrefRel of P \/ the ToleranceRel of P)):] = (( the PrefRel of P \/ the ToleranceRel of P) \/ (( the PrefRel of P \/ the ToleranceRel of P) ~)) \/ (id (field ( the PrefRel of P \/ the ToleranceRel of P)))
by S1, ConField;
then df:
[: the carrier of P, the carrier of P:] =
the
ToleranceRel of
P \/ ( the ToleranceRel of P \/ ( the PrefRel of P \/ (( the PrefRel of P \/ the ToleranceRel of P) ~)))
by XBOOLE_1:4, a3, k1, Y3
.=
( the ToleranceRel of P \/ the ToleranceRel of P) \/ ( the PrefRel of P \/ (( the PrefRel of P \/ the ToleranceRel of P) ~))
by XBOOLE_1:4
.=
( the PrefRel of P \/ the ToleranceRel of P) \/ (( the PrefRel of P \/ the ToleranceRel of P) ~)
by XBOOLE_1:4
;
the
InternalRel of
P = (( the PrefRel of P \/ the ToleranceRel of P) `) /\ ((( the PrefRel of P \/ the ToleranceRel of P) ~) `)
by KK, Th2;
then the
InternalRel of
P =
(({} [: the carrier of P, the carrier of P:]) `) `
by df, XBOOLE_1:53
.=
{} [: the carrier of P, the carrier of P:]
;
hence
P is
tournament-like
by a3, Y3;
verum
end;
hence
( P is tournament-like iff ( CharRel P is connected & CharRel P is antisymmetric & CharRel P is total ) )
by A1; verum