begin
theorem Th1:
theorem
:: deftheorem defines \ FUZZY_2:def 1 :
for C being non empty set
for f, g being Membership_Func of C holds f \ g = min f,(1_minus g);
theorem
theorem Th4:
theorem
theorem
theorem
canceled;
theorem
canceled;
theorem
theorem
canceled;
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
canceled;
theorem
theorem
canceled;
theorem
theorem Th25:
theorem Th26:
theorem
theorem
theorem
theorem
theorem Th31:
theorem Th32:
begin
:: deftheorem Def2 defines * FUZZY_2:def 2 :
for C being non empty set
for h, g, b4 being Membership_Func of C holds
( b4 = h * g iff for c being Element of C holds b4 . c = (h . c) * (g . c) );
:: deftheorem Def3 defines ++ FUZZY_2:def 3 :
for C being non empty set
for h, g, b4 being Membership_Func of C holds
( b4 = h ++ g iff for c being Element of C holds b4 . c = ((h . c) + (g . c)) - ((h . c) * (g . c)) );
theorem Th33:
theorem Th34:
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th41:
theorem
theorem
theorem
theorem
Lm1:
for a, b, c being Real st 0 <= c holds
c * (min a,b) = min (c * a),(c * b)
Lm2:
for a, b, c being Real st 0 <= c holds
c * (max a,b) = max (c * a),(c * b)
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th54:
theorem
theorem
begin
definition
let C1,
C2 be non
empty set ;
func Zmf C1,
C2 -> RMembership_Func of
C1,
C2 equals
chi {} ,
[:C1,C2:];
correctness
coherence
chi {} ,[:C1,C2:] is RMembership_Func of C1,C2;
by FUZZY_1:13;
func Umf C1,
C2 -> RMembership_Func of
C1,
C2 equals
chi [:C1,C2:],
[:C1,C2:];
correctness
coherence
chi [:C1,C2:],[:C1,C2:] is RMembership_Func of C1,C2;
by FUZZY_1:2;
end;
:: deftheorem defines Zmf FUZZY_2:def 4 :
for C1, C2 being non empty set holds Zmf C1,C2 = chi {} ,[:C1,C2:];
:: deftheorem defines Umf FUZZY_2:def 5 :
for C1, C2 being non empty set holds Umf C1,C2 = chi [:C1,C2:],[:C1,C2:];
theorem
theorem
for
C1,
C2 being non
empty set for
f being
RMembership_Func of
C1,
C2 holds
(
max f,
(Umf C1,C2) = Umf C1,
C2 &
min f,
(Umf C1,C2) = f &
max f,
(Zmf C1,C2) = f &
min f,
(Zmf C1,C2) = Zmf C1,
C2 )
theorem
theorem
theorem