begin
theorem
canceled;
theorem
:: deftheorem FUZZY_1:def 1 :
canceled;
:: deftheorem Def2 defines is_less_than FUZZY_1:def 2 :
:: deftheorem Def3 defines is_less_than FUZZY_1:def 3 :
Lm1:
for C being non empty set
for f, g being Membership_Func of C st g c= & f c= holds
f = g
theorem
theorem
theorem
begin
definition
let C be non
empty set ;
let h,
g be
Membership_Func of
C;
func min h,
g -> Membership_Func of
C means :
Def4:
for
c being
Element of
C holds
it . c = min (h . c),
(g . 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;
:: deftheorem Def4 defines min FUZZY_1:def 4 :
definition
let C be non
empty set ;
let h,
g be
Membership_Func of
C;
func max h,
g -> Membership_Func of
C means :
Def5:
for
c being
Element of
C holds
it . c = max (h . c),
(g . 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;
:: deftheorem Def5 defines max FUZZY_1:def 5 :
:: deftheorem Def6 defines 1_minus FUZZY_1:def 6 :
theorem
theorem
for
C being non
empty set for
h,
f,
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 Th8:
for
C being non
empty set for
f,
g,
h 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:
theorem Th10:
for
C being non
empty set for
f,
g,
h 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) )
theorem
theorem Th12:
begin
theorem
:: deftheorem defines EMF FUZZY_1:def 7 :
:: deftheorem defines UMF FUZZY_1:def 8 :
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem
theorem
theorem
theorem
theorem Th25:
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem Th30:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
Lm2:
for C being non empty set
for f, g being Membership_Func of C st g c= holds
1_minus f c=
theorem Th39:
theorem
theorem
theorem
theorem
canceled;
theorem Th44:
definition
let C be non
empty set ;
let h,
g be
Membership_Func of
C;
func h \+\ g -> Membership_Func of
C equals
max (min h,(1_minus g)),
(min (1_minus h),g);
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;
:: deftheorem defines \+\ FUZZY_1:def 9 :
theorem
theorem
theorem
for
C being non
empty set for
f,
g,
h 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)
theorem
theorem
theorem
:: deftheorem defines ab_difMF FUZZY_1:def 10 :