environ
vocabularies HIDDEN, NUMBERS, XBOOLE_0, SUBSET_1, FUNCT_3, XXREAL_1, CARD_1, RELAT_1, TARSKI, FUNCT_1, VALUED_0, LATTICE3, XXREAL_0, PARTFUN1, SEQ_4, ARYTM_1, ARYTM_3, COMPLEX1, FUZZY_1, MEASURE5, FUNCT_7;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XXREAL_0, XCMPLX_0, COMPLEX1, XREAL_0, RELAT_1, RELSET_1, FUNCT_1, PARTFUN1, FUNCT_2, VALUED_0, SEQ_4, RFUNCT_1, MEASURE5, INTEGRA1, RCOMP_1;
definitions RELAT_1;
theorems TARSKI, FUNCT_1, FUNCT_3, ABSVALUE, PARTFUN1, ZFMISC_1, INTEGRA1, INTEGRA2, XBOOLE_0, XBOOLE_1, COMPLEX1, XREAL_1, XXREAL_0, XXREAL_1, FUNCT_2, RELAT_1, MEASURE5, XREAL_0;
schemes SEQ_1, PARTFUN1;
registrations RELSET_1, NUMBERS, XXREAL_0, MEMBERED, XBOOLE_0, VALUED_0, RFUNCT_1, FUNCT_2, MEASURE5, XREAL_0, ORDINAL1;
constructors HIDDEN, REAL_1, SQUARE_1, COMPLEX1, RFUNCT_1, INTEGRA1, SEQ_4, RELSET_1, NUMBERS;
requirements HIDDEN, NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
equalities ORDINAL1;
expansions ;
Lm1:
for C being non empty set
for f, g being Membership_Func of C st g c= & f c= holds
f = g
reconsider jj = 1 as Element of REAL by XREAL_0:def 1;
definition
let C be non
empty set ;
let h,
g be
Membership_Func of
C;
existence
ex b1 being Membership_Func of C st
for c being Element of C holds b1 . c = min ((h . c),(g . c))
uniqueness
for b1, b2 being Membership_Func of C st ( for c being Element of C holds b1 . c = min ((h . c),(g . c)) ) & ( for c being Element of C holds b2 . c = min ((h . c),(g . c)) ) holds
b1 = b2
idempotence
for h being Membership_Func of C
for c being Element of C holds h . c = min ((h . c),(h . c))
;
commutativity
for b1, h, g being Membership_Func of C st ( for c being Element of C holds b1 . c = min ((h . c),(g . c)) ) holds
for c being Element of C holds b1 . c = min ((g . c),(h . c))
;
end;
definition
let C be non
empty set ;
let h,
g be
Membership_Func of
C;
existence
ex b1 being Membership_Func of C st
for c being Element of C holds b1 . c = max ((h . c),(g . c))
uniqueness
for b1, b2 being Membership_Func of C st ( for c being Element of C holds b1 . c = max ((h . c),(g . c)) ) & ( for c being Element of C holds b2 . c = max ((h . c),(g . c)) ) holds
b1 = b2
idempotence
for h being Membership_Func of C
for c being Element of C holds h . c = max ((h . c),(h . c))
;
commutativity
for b1, h, g being Membership_Func of C st ( for c being Element of C holds b1 . c = max ((h . c),(g . c)) ) holds
for c being Element of C holds b1 . c = max ((g . c),(h . c))
;
end;
theorem
for
C being non
empty set for
f,
h,
g being
Membership_Func of
C holds
(
max (
h,
h)
= h &
min (
h,
h)
= h &
max (
h,
h)
= min (
h,
h) &
min (
f,
g)
= min (
g,
f) &
max (
f,
g)
= max (
g,
f) ) ;
theorem Th7:
for
C being non
empty set for
f,
h,
g being
Membership_Func of
C holds
(
max (
(max (f,g)),
h)
= max (
f,
(max (g,h))) &
min (
(min (f,g)),
h)
= min (
f,
(min (g,h))) )
theorem Th9:
for
C being non
empty set for
f,
h,
g being
Membership_Func of
C holds
(
min (
f,
(max (g,h)))
= max (
(min (f,g)),
(min (f,h))) &
max (
f,
(min (g,h)))
= min (
(max (f,g)),
(max (f,h))) )
Lm2:
for C being non empty set
for f, g being Membership_Func of C st g c= holds
1_minus f c=
definition
let C be non
empty set ;
let h,
g be
Membership_Func of
C;
coherence
max ((min (h,(1_minus g))),(min ((1_minus h),g))) is Membership_Func of C
;
commutativity
for b1, h, g being Membership_Func of C st b1 = max ((min (h,(1_minus g))),(min ((1_minus h),g))) holds
b1 = max ((min (g,(1_minus h))),(min ((1_minus g),h)))
;
end;
theorem
for
C being non
empty set for
f,
h,
g being
Membership_Func of
C holds
min (
(min ((max (f,g)),(max (g,h)))),
(max (h,f)))
= max (
(max ((min (f,g)),(min (g,h)))),
(min (h,f)))