:: by Eliza Niewiadomska and Adam Grabowski

::

:: Received October 7, 2013

:: Copyright (c) 2013-2019 Association of Mizar Users

:: 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 ) );

for X, Y, Z being set holds

( X,Y,Z are_mutually_disjoint iff ( X misses Y & Y misses Z & X misses Z ) );

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

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

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

for R being Relation of X holds R /\ ((R ~) `),R /\ (R ~),(R `) /\ ((R ~) `) are_mutually_disjoint

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 ;

ex b_{1} being Order of X st

( b_{1} is connected & b_{1} is being_linear-order )

end;
cluster Relation-like X -defined X -valued total reflexive antisymmetric connected transitive being_linear-order for Element of bool [:X,X:];

existence ex b

( b

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;

( 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 )

( R is symmetric iff for x, y being object st [x,y] in R holds

[y,x] in R )

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 )

( R is asymmetric iff for x, y being object st [x,y] in R holds

not [y,x] in R )

proof end;

theorem :: PREFER_1:25

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

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 )

for R being total reflexive Relation of X holds

( (R `) /\ ((R ~) `) is irreflexive & (R `) /\ ((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 )

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 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 )

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)) )

( R is connected iff [:(field R),(field R):] = (R \/ (R ~)) \/ (id (field R)) )

proof end;

:: deftheorem defines SymCl PREFER_1:def 2 :

for X being set

for R being Relation of X holds SymCl R = R \/ (R ~);

for X being set

for R being Relation of X holds SymCl R = R \/ (R ~);

definition

attr c_{1} is strict ;

struct PrefStr -> 1-sorted ;

aggr PrefStr(# carrier, PrefRel #) -> PrefStr ;

sel PrefRel c_{1} -> Relation of the carrier of c_{1};

end;
struct PrefStr -> 1-sorted ;

aggr PrefStr(# carrier, PrefRel #) -> PrefStr ;

sel PrefRel c

definition

attr c_{1} is strict ;

struct PIStr -> PrefStr , TolStr ;

aggr PIStr(# carrier, PrefRel, ToleranceRel #) -> PIStr ;

end;
struct PIStr -> PrefStr , TolStr ;

aggr PIStr(# carrier, PrefRel, ToleranceRel #) -> PIStr ;

definition

attr c_{1} is strict ;

struct PreferenceStr -> PIStr , RelStr , PrefStr ;

aggr PreferenceStr(# carrier, PrefRel, ToleranceRel, InternalRel #) -> PreferenceStr ;

end;
struct PreferenceStr -> PIStr , RelStr , PrefStr ;

aggr PreferenceStr(# carrier, PrefRel, ToleranceRel, InternalRel #) -> PreferenceStr ;

registration

existence

ex b_{1} being PIStr st

( not b_{1} is empty & b_{1} is strict )

ex b_{1} being PIStr st

( b_{1} is empty & b_{1} is strict )

end;
ex b

( not b

proof end;

existence ex b

( b

proof end;

registration

existence

ex b_{1} being PrefStr st

( not b_{1} is empty & b_{1} is strict )

ex b_{1} being PrefStr st

( b_{1} is empty & b_{1} is strict )

ex b_{1} being PIStr st

( not b_{1} is empty & b_{1} is strict )

ex b_{1} being PreferenceStr st

( not b_{1} is empty & b_{1} is strict )

end;
ex b

( not b

proof end;

existence ex b

( b

proof end;

existence ex b

( not b

proof end;

existence ex b

( not b

proof end;

definition

let X be PreferenceStr ;

end;
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 );

( 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 );

:: 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 ) );

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 ;

PreferenceStr(# X,({} (X,X)),(nabla X),({} (X,X)) #) is strict PreferenceStr ;

end;
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)) #);

PreferenceStr(# X,({} (X,X)),(nabla X),({} (X,X)) #) is strict PreferenceStr ;

:: deftheorem defines PrefSpace PREFER_1:def 4 :

for X being set holds PrefSpace X = PreferenceStr(# X,({} (X,X)),(nabla X),({} (X,X)) #);

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 ;

coherence

( not PrefSpace A is empty & PrefSpace A is preference-like ) by Lemma1A;

end;
coherence

( not PrefSpace A is empty & PrefSpace A is preference-like ) by Lemma1A;

registration

existence

ex b_{1} being PreferenceStr st

( not b_{1} is empty & b_{1} is strict & b_{1} is preference-like )

end;
ex b

( not b

proof end;

registration
end;

registration

let A be non empty trivial set ;

coherence

( not PrefSpace A is empty & PrefSpace A is preference-like ) ;

end;
coherence

( not PrefSpace A is empty & PrefSpace A is preference-like ) ;

definition

let A be set ;

ex b_{1} being strict PreferenceStr st

( the carrier of b_{1} = A & the PrefRel of b_{1} = {} & the ToleranceRel of b_{1} = id A & the InternalRel of b_{1} = {} )

for b_{1}, b_{2} being strict PreferenceStr st the carrier of b_{1} = A & the PrefRel of b_{1} = {} & the ToleranceRel of b_{1} = id A & the InternalRel of b_{1} = {} & the carrier of b_{2} = A & the PrefRel of b_{2} = {} & the ToleranceRel of b_{2} = id A & the InternalRel of b_{2} = {} holds

b_{1} = b_{2}
;

end;
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 ( the carrier of it = A & the PrefRel of it = {} & the ToleranceRel of it = id A & the InternalRel of it = {} );

ex b

( the carrier of b

proof end;

uniqueness for b

b

:: deftheorem Def5 defines IdPrefSpace PREFER_1:def 5 :

for A being set

for b_{2} being strict PreferenceStr holds

( b_{2} = IdPrefSpace A iff ( the carrier of b_{2} = A & the PrefRel of b_{2} = {} & the ToleranceRel of b_{2} = id A & the InternalRel of b_{2} = {} ) );

for A being set

for b

( b

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

proof end;

registration
end;

definition

let A be 2 -element set ;

let a, b be Element of A;

ex b_{1} being strict PreferenceStr st

( the carrier of b_{1} = A & the PrefRel of b_{1} = {[a,b]} & the ToleranceRel of b_{1} = {[a,a],[b,b]} & the InternalRel of b_{1} = {} )

for b_{1}, b_{2} being strict PreferenceStr st the carrier of b_{1} = A & the PrefRel of b_{1} = {[a,b]} & the ToleranceRel of b_{1} = {[a,a],[b,b]} & the InternalRel of b_{1} = {} & the carrier of b_{2} = A & the PrefRel of b_{2} = {[a,b]} & the ToleranceRel of b_{2} = {[a,a],[b,b]} & the InternalRel of b_{2} = {} holds

b_{1} = b_{2}
;

end;
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 ( the carrier of it = A & the PrefRel of it = {[a,b]} & the ToleranceRel of it = {[a,a],[b,b]} & the InternalRel of it = {} );

ex b

( the carrier of b

proof end;

uniqueness for b

b

:: deftheorem Def3 defines PrefSpace PREFER_1:def 6 :

for A being 2 -element set

for a, b being Element of A

for b_{4} being strict PreferenceStr holds

( b_{4} = PrefSpace (A,a,b) iff ( the carrier of b_{4} = A & the PrefRel of b_{4} = {[a,b]} & the ToleranceRel of b_{4} = {[a,a],[b,b]} & the InternalRel of b_{4} = {} ) );

for A being 2 -element set

for a, b being Element of A

for b

( b

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

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;

ex b_{1} being strict PreferenceStr st

( the carrier of b_{1} = A & the PrefRel of b_{1} = {} & the ToleranceRel of b_{1} = {[a,a],[b,b]} & the InternalRel of b_{1} = {[a,b],[b,a]} )

for b_{1}, b_{2} being strict PreferenceStr st the carrier of b_{1} = A & the PrefRel of b_{1} = {} & the ToleranceRel of b_{1} = {[a,a],[b,b]} & the InternalRel of b_{1} = {[a,b],[b,a]} & the carrier of b_{2} = A & the PrefRel of b_{2} = {} & the ToleranceRel of b_{2} = {[a,a],[b,b]} & the InternalRel of b_{2} = {[a,b],[b,a]} holds

b_{1} = b_{2}
;

end;
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 ( 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]} );

ex b

( the carrier of b

proof end;

uniqueness for b

b

:: deftheorem Def4 defines IntPrefSpace PREFER_1:def 7 :

for A being non empty set

for a, b being Element of A

for b_{4} being strict PreferenceStr holds

( b_{4} = IntPrefSpace (A,a,b) iff ( the carrier of b_{4} = A & the PrefRel of b_{4} = {} & the ToleranceRel of b_{4} = {[a,a],[b,b]} & the InternalRel of b_{4} = {[a,b],[b,a]} ) );

for A being non empty set

for a, b being Element of A

for b

( b

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 )

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 ;

the PrefRel of P \/ the ToleranceRel of P is Relation of the carrier of P ;

end;
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;

the PrefRel of P \/ the ToleranceRel of P is Relation of the carrier of P ;

:: deftheorem defines CharRel PREFER_1:def 8 :

for P being PIStr holds CharRel P = the PrefRel of P \/ the ToleranceRel of P;

for P being PIStr holds CharRel P = the PrefRel of P \/ the ToleranceRel of P;

definition

let P be PIStr ;

end;
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 );

( 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 );

:: 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 ) );

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

existence

ex b_{1} being non empty strict PIStr st b_{1} is PI-preference-like

ex b_{1} being empty strict PIStr st b_{1} is PI-preference-like

end;
ex b

proof end;

existence ex b

proof 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) ~) `)

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) ~)

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) ~) `)

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) ~)

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) ~) `)

the InternalRel of P = ((CharRel P) `) /\ (((CharRel P) ~) `)

proof end;

definition

let X be set ;

let R be Relation of X;

SymCl ((((R /\ ((R ~) `)) \/ ((R /\ ((R ~) `)) ~)) \/ (R /\ (R ~))) `) is Relation of X ;

end;
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 ~))) `);

SymCl ((((R /\ ((R ~) `)) \/ ((R /\ ((R ~) `)) ~)) \/ (R /\ (R ~))) `) is Relation of X ;

:: 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 ~))) `);

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

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 ~)))

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

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 )

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;

coherence

( Aux R is irreflexive & Aux R is symmetric ) by AuxIrr;

end;
let R be total reflexive Relation of X;

coherence

( Aux R is irreflexive & Aux R is symmetric ) by AuxIrr;

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

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;

ex b_{1} being strict PreferenceStr st

( the carrier of b_{1} = X & the PrefRel of b_{1} = P /\ ((P ~) `) & the ToleranceRel of b_{1} = P /\ (P ~) & the InternalRel of b_{1} = Aux P )

for b_{1}, b_{2} being strict PreferenceStr st the carrier of b_{1} = X & the PrefRel of b_{1} = P /\ ((P ~) `) & the ToleranceRel of b_{1} = P /\ (P ~) & the InternalRel of b_{1} = Aux P & the carrier of b_{2} = X & the PrefRel of b_{2} = P /\ ((P ~) `) & the ToleranceRel of b_{2} = P /\ (P ~) & the InternalRel of b_{2} = Aux P holds

b_{1} = b_{2}
;

end;
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 ( the carrier of it = X & the PrefRel of it = P /\ ((P ~) `) & the ToleranceRel of it = P /\ (P ~) & the InternalRel of it = Aux P );

ex b

( the carrier of b

proof end;

uniqueness for b

b

:: deftheorem Def55 defines CharPrefSpace PREFER_1:def 11 :

for X being set

for P being Relation of X

for b_{3} being strict PreferenceStr holds

( b_{3} = CharPrefSpace P iff ( the carrier of b_{3} = X & the PrefRel of b_{3} = P /\ ((P ~) `) & the ToleranceRel of b_{3} = P /\ (P ~) & the InternalRel of b_{3} = Aux P ) );

for X being set

for P being Relation of X

for b

( b

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

for R being total reflexive Relation of A holds CharPrefSpace R is preference-like

proof end;

registration
end;

registration

let X be non empty set ;

let P be total reflexive Relation of X;

coherence

CharPrefSpace P is preference-like by CharIsPref;

end;
let P be total reflexive Relation of X;

coherence

CharPrefSpace P is preference-like by CharIsPref;

:: 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}):] ) ) );

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;

registration

let A be non empty trivial set ;

coherence

( not IdPrefSpace A is empty & IdPrefSpace A is preference-like )

end;
coherence

( not IdPrefSpace A is empty & IdPrefSpace A is preference-like )

proof end;

definition

let P be PreferenceStr ;

end;
attr P is tournament-like means :: PREFER_1:def 13

( the ToleranceRel of P = id the carrier of P & the InternalRel of P = {} );

( the ToleranceRel of P = id the carrier of P & the InternalRel of P = {} );

:: 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 = {} ) );

for P being PreferenceStr holds

( P is tournament-like iff ( the ToleranceRel of P = id the carrier of P & the InternalRel of P = {} ) );

registration
end;

registration
end;

registration

existence

ex b_{1} being empty PreferenceSpace st b_{1} is tournament-like

ex b_{1} being non empty PreferenceSpace st b_{1} is tournament-like

end;
ex b

proof end;

existence ex b

proof 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 ) )

( P is tournament-like iff ( CharRel P is connected & CharRel P is antisymmetric & CharRel P is total ) )

proof end;

definition

let P be PreferenceStr ;

end;
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 = {} );

( the PrefRel of P is transitive & the ToleranceRel of P = id the carrier of P & the InternalRel of P = {} );

:: 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 = {} ) );

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
end;

registration
end;

registration

ex b_{1} being empty PreferenceSpace st b_{1} is total

ex b_{1} being non empty PreferenceSpace st b_{1} is total
end;

cluster empty trivial V53() 0 -element void preference-like tournament-like total for PreferenceStr ;

existence ex b

proof end;

existence ex b

proof 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 )

( P is total iff CharRel P is connected Order of the carrier of P )

proof end;