begin
theorem Th1:
theorem
:: deftheorem defines \ FUZZY_2:def 1 :
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 :
:: deftheorem Def3 defines ++ FUZZY_2:def 3 :
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 :
:: deftheorem defines Umf FUZZY_2:def 5 :
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