environ
vocabularies HIDDEN, PREFER_1, PCS_0, ORDERS_1, WELLORD1, WAYBEL_4, CARD_1, SUBSET_1, RELAT_1, XBOOLE_0, PARTFUN1, RELAT_2, STRUCT_0, ZFMISC_1, TARSKI, ORDERS_2, EQREL_1;
notations HIDDEN, TARSKI, XBOOLE_0, XTUPLE_0, SUBSET_1, ZFMISC_1, MCART_1, DOMAIN_1, CARD_1, NAT_1, RELAT_1, FUNCT_1, PARTFUN1, RELSET_1, RELAT_2, EQREL_1, CARD_3, PARTIT_2, FUNCT_4, ORDINAL1, NUMBERS, FUNCOP_1, WELLORD1, STRUCT_0, ORDERS_1, ORDERS_2, YELLOW_3, ENUMSET1, PCS_0, XCMPLX_0, FUNCT_2, VALUED_0;
definitions TARSKI, RELAT_2;
theorems XBOOLE_0, SYSREL, ZFMISC_1, XBOOLE_1, RELAT_1, CARD_2, RELAT_2, ENUMSET1, CARD_1, TARSKI, XTUPLE_0, NECKLA_3, SUBSET_1, PARTFUN1, ORDERS_1, PRE_POLY, WELLSET1, ROUGHS_1;
schemes ;
registrations EQREL_1, PARTFUN1, SUBSET_1, XBOOLE_0, WAYBEL_3, RELAT_1, ORDERS_1, WELLORD1, ORDERS_2, STRUCT_0, YELLOW16, YELLOW_3, RELSET_1, FUNCOP_1, RELAT_2, XTUPLE_0, ORDINAL1, PARTIT_2, TOLER_1, ZFMISC_1, NAT_1, FOMODEL3, REWRITE2, PRE_POLY, FUNCT_1, FINSET_1, XXREAL_0, XREAL_0, CARD_1, NUMBERS, VALUED_0;
constructors HIDDEN, PRALG_1, PARTIT_2, TSEP_1, YELLOW16, YELLOW_3, DOMAIN_1, RELSET_1, FUNCT_4, AFINSQ_1, XTUPLE_0, NUMBERS, PARTFUN2, NAT_1, ORDERS_1, PCS_0, WELLORD1, WELLORD2, FUNCOP_1, XXREAL_0, XREAL_0, CARD_1, XCMPLX_0, INT_1, VALUED_0;
requirements HIDDEN, BOOLE, SUBSET, NUMERALS, REAL, ARITHM;
equalities EQREL_1, SUBSET_1, RELAT_1;
expansions ;
theorem
for
a,
b being
set st
a <> b holds
{[a,a],[b,b]} <> {[a,a],[a,b],[b,a],[b,b]}
Lemma10:
for a, b, c, d being object holds {a,d} \/ {b,c} = {a,b,c,d}
Lemma19:
for X, Y being set st X c= Y & X misses Y holds
X = {}
by XBOOLE_1:68;
Lemma1A:
for A being non empty set holds
( not PrefSpace A is empty & PrefSpace A is preference-like )
IdPrefNot2:
for A being non trivial set holds not IdPrefSpace A is preference-like
definition
let A be 2
-element set ;
let a,
b be
Element of
A;
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 = {} )
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;
definition
let A be non
empty set ;
let a,
b be
Element of
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]} )
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;
Lemma1C:
for A being non empty trivial set holds the ToleranceRel of (PrefSpace A) = id the carrier of (PrefSpace A)
ZZ:
for A being empty set holds IdPrefSpace A = PrefSpace A