:: Introduction to Formal Preference Spaces
:: by Eliza Niewiadomska and Adam Grabowski
::
:: Received October 7, 2013
:: Copyright (c) 2013-2021 Association of Mizar Users


definition
let X, Y, Z be set ;
pred X,Y,Z are_mutually_disjoint means :: PREFER_1:def 1
( X misses Y & Y misses Z & X misses Z );
end;

:: deftheorem defines are_mutually_disjoint PREFER_1:def 1 :
for X, Y, Z being set holds
( X,Y,Z are_mutually_disjoint iff ( X misses Y & Y misses Z & X misses Z ) );

theorem Lemma1: :: PREFER_1:1
for A being set holds {} ,A, {} are_mutually_disjoint
proof end;

registration
cluster 2 -element -> non empty for set ;
coherence
for b1 being set st b1 is 2 -element holds
not b1 is empty ;
end;

theorem :: PREFER_1:2
for a, b being set st a <> b holds
{[a,a],[b,b]} <> {[a,a],[a,b],[b,a],[b,b]}
proof end;

theorem Lemma3: :: PREFER_1:3
for A being 2 -element set
for a, b being Element of A st a <> b holds
A = {a,b}
proof end;

theorem :: PREFER_1:4
for A being 2 -element set ex a, b being Element of A st
( a <> b & A = {a,b} )
proof end;

theorem :: PREFER_1:5
for A being non trivial set ex a, b being Element of A st a <> b
proof end;

theorem Lemma6: :: PREFER_1:6
for x1, x2, x3, x4 being set holds ({x1} \/ {x2}) \/ {x3,x4} = {x3,x1,x2,x4}
proof end;

Lemma10: for a, b, c, d being object holds {a,d} \/ {b,c} = {a,b,c,d}
proof end;

theorem Lemma11: :: PREFER_1:7
for a, b being set st a <> b holds
{[a,a],[b,b]} misses {[a,b],[b,a]}
proof end;

theorem Lemma4: :: PREFER_1:8
for A being 2 -element set
for a, b being Element of A st a <> b holds
id A = {[a,a],[b,b]}
proof end;

theorem Lemma7: :: PREFER_1:9
for a, b being object
for R being Relation st R = {[a,b]} holds
R ~ = {[b,a]}
proof end;

theorem Lemma8: :: PREFER_1:10
for a, b being set holds
( a <> b iff {[a,b]} misses {[a,a],[b,b]} )
proof end;

theorem Lemma12b: :: PREFER_1:11
for X being non empty set
for R being Relation of X
for x, y being Element of X st not [x,y] in R ` holds
[x,y] in R
proof end;

theorem :: PREFER_1:12
for X being non empty set
for R being Relation of X holds R /\ ((R ~) `),R /\ (R ~),(R `) /\ ((R ~) `) are_mutually_disjoint
proof end;

theorem LemmaAuxIrr: :: PREFER_1:13
for P, R being Relation st P misses R holds
P ~ misses R ~
proof end;

theorem Tilde1: :: PREFER_1:14
for X being non empty set
for R being Relation of X holds R = (((R ~) `) ~) `
proof end;

theorem :: PREFER_1:15
for X being non empty set
for R being Relation of X holds R ~ = ((R `) ~) `
proof end;

theorem Tilde3: :: PREFER_1:16
for X being non empty set
for R being Relation of X holds ((R ~) `) ~ = R `
proof end;

Lemma19: for X, Y being set st X c= Y & X misses Y holds
X = {}
by XBOOLE_1:68;

registration
let X be set ;
cluster Relation-like X -defined X -valued total reflexive antisymmetric connected transitive being_linear-order for Element of bool [:X,X:];
existence
ex b1 being Order of X st
( b1 is connected & b1 is being_linear-order )
proof end;
end;

theorem :: PREFER_1:17
for X being non empty set
for R being total reflexive Relation of X holds R ~ is total
proof end;

theorem FieldTot: :: PREFER_1:18
for X being non empty set
for R being total Relation of X holds field R = X
proof end;

theorem :: PREFER_1:19
for R being Relation holds
( R is irreflexive iff for x being object st x in field R holds
not [x,x] in R ) by RELAT_2:def 10, RELAT_2:def 2;

theorem LemSym: :: PREFER_1:20
for R being Relation holds
( R is symmetric iff for x, y being object st [x,y] in R holds
[y,x] in R )
proof end;

theorem LEM2a: :: PREFER_1:21
for X being set
for R being Relation of X holds R /\ (R ~) is symmetric
proof end;

theorem LemAsym: :: PREFER_1:22
for R being Relation holds
( R is asymmetric iff for x, y being object st [x,y] in R holds
not [y,x] in R )
proof end;

theorem Lemma5: :: PREFER_1:23
for a, b being object st a <> b holds
{[a,b]} is asymmetric
proof end;

theorem LEM1: :: PREFER_1:24
for X being non empty set
for R being Relation of X holds R /\ ((R ~) `) is asymmetric
proof end;

theorem :: PREFER_1:25
for X being non empty set
for R being total reflexive Relation of X holds R /\ (R ~) is reflexive ;

theorem LEM3b: :: PREFER_1:26
for X being non empty set
for R being total reflexive Relation of X holds R /\ (R ~) is total
proof end;

theorem Lemma9: :: PREFER_1:27
for a, b being object st a <> b holds
( {[a,b],[b,a]} is irreflexive & {[a,b],[b,a]} is symmetric )
proof end;

theorem :: PREFER_1:28
for X being non empty set
for R being total Relation of X
for S being Relation of X holds R \/ S is total
proof end;

theorem :: PREFER_1:29
for X being non empty set
for R being total reflexive Relation of X holds
( (R `) /\ ((R ~) `) is irreflexive & (R `) /\ ((R ~) `) is symmetric )
proof end;

theorem :: PREFER_1:30
for X being set
for R being Relation of X st R is symmetric holds
R ` is symmetric
proof end;

theorem LemAntisym: :: PREFER_1:31
for X being object
for R being Relation holds
( R is antisymmetric iff for x, y being object st [x,y] in R & [y,x] in R holds
x = y )
proof end;

theorem Lemma16: :: PREFER_1:32
for A being set
for R being asymmetric Relation of A holds R \/ (id A) is antisymmetric
proof end;

theorem LemCon: :: PREFER_1:33
for X being object
for R being Relation holds
( R is connected iff for x, y being object st x <> y & x in field R & y in field R & not [x,y] in R holds
[y,x] in R )
proof end;

theorem ConField: :: PREFER_1:34
for R being Relation holds
( R is connected iff [:(field R),(field R):] = (R \/ (R ~)) \/ (id (field R)) )
proof end;

theorem Lemma17: :: PREFER_1:35
for A being set
for R being asymmetric Relation of A holds R misses R ~
proof end;

theorem Lemma20: :: PREFER_1:36
for R, P being Relation st R misses P & P is symmetric holds
R ~ misses P
proof end;

theorem Lemma21: :: PREFER_1:37
for X being set
for R being asymmetric Relation of X holds R misses id X
proof end;

theorem Lemma22: :: PREFER_1:38
for X being set
for R being asymmetric Relation of X holds R * R misses id X
proof end;

definition
let X be set ;
let R be Relation of X;
func SymCl R -> Relation of X equals :: PREFER_1:def 2
R \/ (R ~);
coherence
R \/ (R ~) is Relation of X ;
end;

:: deftheorem defines SymCl PREFER_1:def 2 :
for X being set
for R being Relation of X holds SymCl R = R \/ (R ~);

registration
let X be set ;
let R be total Relation of X;
cluster SymCl R -> total ;
coherence
SymCl R is total
proof end;
end;

registration
let X be set ;
let R be Relation of X;
cluster SymCl R -> symmetric ;
coherence
SymCl R is symmetric ;
end;

definition
attr c1 is strict ;
struct PrefStr -> 1-sorted ;
aggr PrefStr(# carrier, PrefRel #) -> PrefStr ;
sel PrefRel c1 -> Relation of the carrier of c1;
end;

definition
attr c1 is strict ;
struct PIStr -> PrefStr , TolStr ;
aggr PIStr(# carrier, PrefRel, ToleranceRel #) -> PIStr ;
end;

definition
attr c1 is strict ;
struct PreferenceStr -> PIStr , RelStr , PrefStr ;
aggr PreferenceStr(# carrier, PrefRel, ToleranceRel, InternalRel #) -> PreferenceStr ;
end;

registration
cluster non empty strict for PIStr ;
existence
ex b1 being PIStr st
( not b1 is empty & b1 is strict )
proof end;
cluster empty strict for PIStr ;
existence
ex b1 being PIStr st
( b1 is empty & b1 is strict )
proof end;
end;

registration
cluster non empty strict for PrefStr ;
existence
ex b1 being PrefStr st
( not b1 is empty & b1 is strict )
proof end;
cluster empty strict for PrefStr ;
existence
ex b1 being PrefStr st
( b1 is empty & b1 is strict )
proof end;
cluster non empty strict for PIStr ;
existence
ex b1 being PIStr st
( not b1 is empty & b1 is strict )
proof end;
cluster non empty strict for PreferenceStr ;
existence
ex b1 being PreferenceStr st
( not b1 is empty & b1 is strict )
proof end;
end;

definition
let X be PreferenceStr ;
attr X is preference-like means :PrefDef: :: PREFER_1:def 3
( the PrefRel of X is asymmetric & the ToleranceRel of X is Tolerance of the carrier of X & the InternalRel of X is irreflexive & the InternalRel of X is symmetric & the PrefRel of X, the ToleranceRel of X, the InternalRel of X are_mutually_disjoint & (( the PrefRel of X \/ ( the PrefRel of X ~)) \/ the ToleranceRel of X) \/ the InternalRel of X = nabla the carrier of X );
end;

:: deftheorem PrefDef defines preference-like PREFER_1:def 3 :
for X being PreferenceStr holds
( X is preference-like iff ( the PrefRel of X is asymmetric & the ToleranceRel of X is Tolerance of the carrier of X & the InternalRel of X is irreflexive & the InternalRel of X is symmetric & the PrefRel of X, the ToleranceRel of X, the InternalRel of X are_mutually_disjoint & (( the PrefRel of X \/ ( the PrefRel of X ~)) \/ the ToleranceRel of X) \/ the InternalRel of X = nabla the carrier of X ) );

definition
let X be set ;
func PrefSpace X -> strict PreferenceStr equals :: PREFER_1:def 4
 PreferenceStr(# X,({} (X,X)),(nabla X),({} (X,X)) #);
coherence
PreferenceStr(# X,({} (X,X)),(nabla X),({} (X,X)) #) is strict PreferenceStr ;
end;

:: deftheorem defines PrefSpace PREFER_1:def 4 :
for X being set holds PrefSpace X = PreferenceStr(# X,({} (X,X)),(nabla X),({} (X,X)) #);

Lemma1A: for A being non empty set holds
( not PrefSpace A is empty & PrefSpace A is preference-like )
proof end;

registration
let A be non empty set ;
cluster PrefSpace A -> non empty strict preference-like ;
coherence
( not PrefSpace A is empty & PrefSpace A is preference-like ) by Lemma1A;
end;

registration
cluster non empty strict preference-like for PreferenceStr ;
existence
ex b1 being PreferenceStr st
( not b1 is empty & b1 is strict & b1 is preference-like )
proof end;
end;

definition
mode PreferenceSpace is preference-like PreferenceStr ;
end;

registration
cluster empty -> preference-like for PreferenceStr ;
coherence
for b1 being PreferenceStr st b1 is empty holds
b1 is preference-like
proof end;
end;

registration
cluster PrefSpace {} -> empty strict preference-like ;
coherence
( PrefSpace {} is empty & PrefSpace {} is preference-like )
proof end;
end;

registration
cluster empty preference-like for PreferenceStr ;
existence
ex b1 being PreferenceSpace st b1 is empty
proof end;
end;

registration
let A be non empty trivial set ;
cluster PrefSpace A -> trivial strict ;
coherence
PrefSpace A is trivial ;
end;

registration
let A be non empty trivial set ;
cluster PrefSpace A -> non empty strict preference-like ;
coherence
( not PrefSpace A is empty & PrefSpace A is preference-like ) ;
end;

definition
let A be set ;
func IdPrefSpace A -> strict PreferenceStr means :Def5: :: PREFER_1:def 5
( the carrier of it = A & the PrefRel of it = {} & the ToleranceRel of it = id A & the InternalRel of it = {} );
existence
ex b1 being strict PreferenceStr st
( the carrier of b1 = A & the PrefRel of b1 = {} & the ToleranceRel of b1 = id A & the InternalRel of b1 = {} )
proof end;
uniqueness
for b1, b2 being strict PreferenceStr st the carrier of b1 = A & the PrefRel of b1 = {} & the ToleranceRel of b1 = id A & the InternalRel of b1 = {} & the carrier of b2 = A & the PrefRel of b2 = {} & the ToleranceRel of b2 = id A & the InternalRel of b2 = {} holds
b1 = b2 ;
end;

:: deftheorem Def5 defines IdPrefSpace PREFER_1:def 5 :
for A being set
for b2 being strict PreferenceStr holds
( b2 = IdPrefSpace A iff ( the carrier of b2 = A & the PrefRel of b2 = {} & the ToleranceRel of b2 = id A & the InternalRel of b2 = {} ) );

IdPrefNot2: for A being non trivial set holds not IdPrefSpace A is preference-like
proof end;

registration
let A be non trivial set ;
cluster IdPrefSpace A -> strict non preference-like ;
coherence
not IdPrefSpace A is preference-like by IdPrefNot2;
end;

definition
let A be 2 -element set ;
let a, b be Element of A;
func PrefSpace (A,a,b) -> strict PreferenceStr means :Def3: :: PREFER_1:def 6
( the carrier of it = A & the PrefRel of it = {[a,b]} & the ToleranceRel of it = {[a,a],[b,b]} & the InternalRel of it = {} );
existence
ex b1 being strict PreferenceStr st
( the carrier of b1 = A & the PrefRel of b1 = {[a,b]} & the ToleranceRel of b1 = {[a,a],[b,b]} & the InternalRel of b1 = {} )
proof end;
uniqueness
for b1, b2 being strict PreferenceStr st the carrier of b1 = A & the PrefRel of b1 = {[a,b]} & the ToleranceRel of b1 = {[a,a],[b,b]} & the InternalRel of b1 = {} & the carrier of b2 = A & the PrefRel of b2 = {[a,b]} & the ToleranceRel of b2 = {[a,a],[b,b]} & the InternalRel of b2 = {} holds
b1 = b2 ;
end;

:: deftheorem Def3 defines PrefSpace PREFER_1:def 6 :
for A being 2 -element set
for a, b being Element of A
for b4 being strict PreferenceStr holds
( b4 = PrefSpace (A,a,b) iff ( the carrier of b4 = A & the PrefRel of b4 = {[a,b]} & the ToleranceRel of b4 = {[a,a],[b,b]} & the InternalRel of b4 = {} ) );

theorem :: PREFER_1:39
for A being 2 -element set
for a, b being Element of A st a <> b holds
PrefSpace (A,a,b) is preference-like
proof end;

definition
let A be non empty set ;
let a, b be Element of A;
func IntPrefSpace (A,a,b) -> strict PreferenceStr means :Def4: :: PREFER_1:def 7
( the carrier of it = A & the PrefRel of it = {} & the ToleranceRel of it = {[a,a],[b,b]} & the InternalRel of it = {[a,b],[b,a]} );
existence
ex b1 being strict PreferenceStr st
( the carrier of b1 = A & the PrefRel of b1 = {} & the ToleranceRel of b1 = {[a,a],[b,b]} & the InternalRel of b1 = {[a,b],[b,a]} )
proof end;
uniqueness
for b1, b2 being strict PreferenceStr st the carrier of b1 = A & the PrefRel of b1 = {} & the ToleranceRel of b1 = {[a,a],[b,b]} & the InternalRel of b1 = {[a,b],[b,a]} & the carrier of b2 = A & the PrefRel of b2 = {} & the ToleranceRel of b2 = {[a,a],[b,b]} & the InternalRel of b2 = {[a,b],[b,a]} holds
b1 = b2 ;
end;

:: deftheorem Def4 defines IntPrefSpace PREFER_1:def 7 :
for A being non empty set
for a, b being Element of A
for b4 being strict PreferenceStr holds
( b4 = IntPrefSpace (A,a,b) iff ( the carrier of b4 = A & the PrefRel of b4 = {} & the ToleranceRel of b4 = {[a,a],[b,b]} & the InternalRel of b4 = {[a,b],[b,a]} ) );

theorem :: PREFER_1:40
for A being 2 -element set
for a, b being Element of A st a <> b holds
( not IntPrefSpace (A,a,b) is empty & IntPrefSpace (A,a,b) is preference-like )
proof end;

definition
let P be PIStr ;
func CharRel P -> Relation of the carrier of P equals :: PREFER_1:def 8
 the PrefRel of P \/ the ToleranceRel of P;
coherence
the PrefRel of P \/ the ToleranceRel of P is Relation of the carrier of P ;
end;

:: deftheorem defines CharRel PREFER_1:def 8 :
for P being PIStr holds CharRel P = the PrefRel of P \/ the ToleranceRel of P;

definition
let P be PIStr ;
attr P is PI-preference-like means :: PREFER_1:def 9
( the PrefRel of P is asymmetric & the ToleranceRel of P is Tolerance of the carrier of P & the PrefRel of P /\ the ToleranceRel of P = {} & ( the PrefRel of P \/ ( the PrefRel of P ~)) \/ the ToleranceRel of P = nabla the carrier of P );
end;

:: deftheorem defines PI-preference-like PREFER_1:def 9 :
for P being PIStr holds
( P is PI-preference-like iff ( the PrefRel of P is asymmetric & the ToleranceRel of P is Tolerance of the carrier of P & the PrefRel of P /\ the ToleranceRel of P = {} & ( the PrefRel of P \/ ( the PrefRel of P ~)) \/ the ToleranceRel of P = nabla the carrier of P ) );

registration
cluster non empty strict PI-preference-like for PIStr ;
existence
ex b1 being non empty strict PIStr st b1 is PI-preference-like
proof end;
cluster empty trivial V53() 0 -element strict PI-preference-like for PIStr ;
existence
ex b1 being empty strict PIStr st b1 is PI-preference-like
proof end;
end;

theorem :: PREFER_1:41
for P being non empty PIStr st P is PI-preference-like holds
the PrefRel of P = (CharRel P) /\ (((CharRel P) ~) `)
proof end;

theorem :: PREFER_1:42
for P being non empty PIStr st P is PI-preference-like holds
the ToleranceRel of P = (CharRel P) /\ ((CharRel P) ~)
proof end;

theorem :: PREFER_1:43
for P being non empty PreferenceStr st P is preference-like holds
the PrefRel of P = (CharRel P) /\ (((CharRel P) ~) `)
proof end;

theorem :: PREFER_1:44
for P being non empty PreferenceStr st P is preference-like holds
the ToleranceRel of P = (CharRel P) /\ ((CharRel P) ~)
proof end;

theorem Th2: :: PREFER_1:45
for P being non empty PreferenceStr st P is preference-like holds
the InternalRel of P = ((CharRel P) `) /\ (((CharRel P) ~) `)
proof end;

definition
let X be set ;
let R be Relation of X;
func Aux R -> Relation of X equals :: PREFER_1:def 10
 SymCl ((((R /\ ((R ~) `)) \/ ((R /\ ((R ~) `)) ~)) \/ (R /\ (R ~))) `);
coherence
SymCl ((((R /\ ((R ~) `)) \/ ((R /\ ((R ~) `)) ~)) \/ (R /\ (R ~))) `) is Relation of X ;
end;

:: deftheorem defines Aux PREFER_1:def 10 :
for X being set
for R being Relation of X holds Aux R = SymCl ((((R /\ ((R ~) `)) \/ ((R /\ ((R ~) `)) ~)) \/ (R /\ (R ~))) `);

theorem SumNabla2: :: PREFER_1:46
for X being non empty set
for R being Relation of X holds (((R /\ ((R ~) `)) \/ ((R /\ ((R ~) `)) ~)) \/ (R /\ (R ~))) \/ (Aux R) = nabla X
proof end;

theorem AuxEq: :: PREFER_1:47
for X being non empty set
for R being total reflexive Relation of X holds Aux R = (((R ~) `) /\ (R `)) \/ (((R `) ~) /\ ((R `) \/ (R ~)))
proof end;

theorem AuxEq2: :: PREFER_1:48
for X being non empty set
for R being total reflexive Relation of X holds R /\ ((R ~) `) misses Aux R
proof end;

theorem AuxIrr: :: PREFER_1:49
for X being non empty set
for R being total reflexive Relation of X holds
( Aux R is irreflexive & Aux R is symmetric )
proof end;

registration
let X be non empty set ;
let R be total reflexive Relation of X;
cluster Aux R -> irreflexive symmetric ;
coherence
( Aux R is irreflexive & Aux R is symmetric ) by AuxIrr;
end;

theorem AuxEq3: :: PREFER_1:50
for X being non empty set
for R being total reflexive Relation of X holds R /\ (R ~) misses Aux R
proof end;

theorem MutuDis2: :: PREFER_1:51
for X being non empty set
for R being total reflexive Relation of X holds R /\ ((R ~) `),R /\ (R ~), Aux R are_mutually_disjoint
proof end;

definition
let X be set ;
let P be Relation of X;
func CharPrefSpace P -> strict PreferenceStr means :Def55: :: PREFER_1:def 11
( the carrier of it = X & the PrefRel of it = P /\ ((P ~) `) & the ToleranceRel of it = P /\ (P ~) & the InternalRel of it = Aux P );
existence
ex b1 being strict PreferenceStr st
( the carrier of b1 = X & the PrefRel of b1 = P /\ ((P ~) `) & the ToleranceRel of b1 = P /\ (P ~) & the InternalRel of b1 = Aux P )
proof end;
uniqueness
for b1, b2 being strict PreferenceStr st the carrier of b1 = X & the PrefRel of b1 = P /\ ((P ~) `) & the ToleranceRel of b1 = P /\ (P ~) & the InternalRel of b1 = Aux P & the carrier of b2 = X & the PrefRel of b2 = P /\ ((P ~) `) & the ToleranceRel of b2 = P /\ (P ~) & the InternalRel of b2 = Aux P holds
b1 = b2 ;
end;

:: deftheorem Def55 defines CharPrefSpace PREFER_1:def 11 :
for X being set
for P being Relation of X
for b3 being strict PreferenceStr holds
( b3 = CharPrefSpace P iff ( the carrier of b3 = X & the PrefRel of b3 = P /\ ((P ~) `) & the ToleranceRel of b3 = P /\ (P ~) & the InternalRel of b3 = Aux P ) );

theorem CharIsPref: :: PREFER_1:52
for A being non empty set
for R being total reflexive Relation of A holds CharPrefSpace R is preference-like
proof end;

registration
let X be non empty set ;
let P be Relation of X;
cluster CharPrefSpace P -> non empty strict ;
coherence
not CharPrefSpace P is empty by Def55;
end;

registration
let X be non empty set ;
let P be total reflexive Relation of X;
cluster CharPrefSpace P -> strict preference-like ;
coherence
CharPrefSpace P is preference-like by CharIsPref;
end;

definition
let P be PreferenceStr ;
attr P is flat means :: PREFER_1:def 12
( the ToleranceRel of P = id the carrier of P & ex a being Element of P st
( the PrefRel of P = [:{a},( the carrier of P \ {a}):] & the InternalRel of P = [:( the carrier of P \ {a}),( the carrier of P \ {a}):] ) );
end;

:: deftheorem defines flat PREFER_1:def 12 :
for P being PreferenceStr holds
( P is flat iff ( the ToleranceRel of P = id the carrier of P & ex a being Element of P st
( the PrefRel of P = [:{a},( the carrier of P \ {a}):] & the InternalRel of P = [:( the carrier of P \ {a}),( the carrier of P \ {a}):] ) ) );

Lemma1C: for A being non empty trivial set holds the ToleranceRel of (PrefSpace A) = id the carrier of (PrefSpace A)
proof end;

ZZ: for A being empty set holds IdPrefSpace A = PrefSpace A
proof end;

theorem :: PREFER_1:53
for A being trivial set holds IdPrefSpace A = PrefSpace A
proof end;

registration
let A be non empty trivial set ;
cluster IdPrefSpace A -> non empty strict preference-like ;
coherence
( not IdPrefSpace A is empty & IdPrefSpace A is preference-like )
proof end;
end;

registration
let A be non empty trivial set ;
cluster IdPrefSpace A -> strict flat ;
coherence
IdPrefSpace A is flat
proof end;
end;

definition
let P be PreferenceStr ;
attr P is tournament-like means :: PREFER_1:def 13
( the ToleranceRel of P = id the carrier of P & the InternalRel of P = {} );
end;

:: deftheorem defines tournament-like PREFER_1:def 13 :
for P being PreferenceStr holds
( P is tournament-like iff ( the ToleranceRel of P = id the carrier of P & the InternalRel of P = {} ) );

registration
cluster empty -> tournament-like for PreferenceStr ;
coherence
for b1 being PreferenceStr st b1 is empty holds
b1 is tournament-like ;
end;

registration
cluster tournament-like -> void for PreferenceStr ;
coherence
for b1 being PreferenceStr st b1 is tournament-like holds
b1 is void ;
end;

registration
cluster empty trivial V53() 0 -element void preference-like tournament-like for PreferenceStr ;
existence
ex b1 being empty PreferenceSpace st b1 is tournament-like
proof end;
cluster non empty preference-like tournament-like for PreferenceStr ;
existence
ex b1 being non empty PreferenceSpace st b1 is tournament-like
proof end;
end;

theorem :: PREFER_1:54
for P being non empty PreferenceSpace holds
( P is tournament-like iff ( CharRel P is connected & CharRel P is antisymmetric & CharRel P is total ) )
proof end;

definition
let P be PreferenceStr ;
attr P is total means :: PREFER_1:def 14
( the PrefRel of P is transitive & the ToleranceRel of P = id the carrier of P & the InternalRel of P = {} );
end;

:: deftheorem defines total PREFER_1:def 14 :
for P being PreferenceStr holds
( P is total iff ( the PrefRel of P is transitive & the ToleranceRel of P = id the carrier of P & the InternalRel of P = {} ) );

registration
cluster total -> void for PreferenceStr ;
coherence
for b1 being PreferenceStr st b1 is total holds
b1 is void ;
end;

registration
cluster total -> tournament-like for PreferenceStr ;
coherence
for b1 being PreferenceStr st b1 is total holds
b1 is tournament-like ;
end;

registration
cluster PrefSpace {} -> strict total ;
coherence
PrefSpace {} is total ;
end;

registration
let A be set ;
cluster IdPrefSpace A -> strict total ;
coherence
IdPrefSpace A is total
proof end;
end;

registration
let A be non empty trivial set ;
cluster PrefSpace A -> strict total ;
coherence
PrefSpace A is total
proof end;
end;

registration
cluster empty trivial V53() 0 -element void preference-like tournament-like total for PreferenceStr ;
existence
ex b1 being empty PreferenceSpace st b1 is total
proof end;
cluster non empty preference-like total for PreferenceStr ;
existence
ex b1 being non empty PreferenceSpace st b1 is total
proof end;
end;

theorem :: PREFER_1:55
for P being non empty PreferenceSpace holds
( P is total iff CharRel P is connected Order of the carrier of P )
proof end;