:: FUZZY_3 semantic presentation

registration

let C be non empty set ;
cluster -> quasi_total Membership_Func of C;
coherence

proof end;

end;

definition

let C1, C2 be non empty set ;
mode RMembership_Func of C1,C2 is Membership_Func of [:C1,C2:];

end;

definition

let C1, C2 be non empty set ;
func Zmf C1,C2 -> RMembership_Func of C1,C2 equals :: FUZZY_3:def 1
chi {} ,[:C1,C2:];
correctness by FUZZY_1:13;
func Umf C1,C2 -> RMembership_Func of C1,C2 equals :: FUZZY_3:def 2
chi [:C1,C2:],[:C1,C2:];
correctness by FUZZY_1:2;

end;

:: deftheorem defines Zmf FUZZY_3:def 1 :

:: deftheorem defines Umf FUZZY_3:def 2 :

theorem Th1: :: FUZZY_3:1

for C1, C2 being non empty set holds Zmf C1,C2 = EMF [:C1,C2:] by FUZZY_1:def 7;

theorem Th2: :: FUZZY_3:2

for C1, C2 being non empty set holds Umf C1,C2 = UMF [:C1,C2:] by FUZZY_1:def 8;

theorem :: FUZZY_3:3

for C1, C2 being non empty set
for x being Element of [:C1,C2:]
for h being RMembership_Func of C1,C2 holds
( (Zmf C1,C2) . x <= h . x & h . x <= (Umf C1,C2) . x )

proof end;

theorem :: FUZZY_3:4

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 )

proof end;

theorem :: FUZZY_3:5

for C1, C2 being non empty set holds
( 1_minus (Zmf C1,C2) = Umf C1,C2 & 1_minus (Umf C1,C2) = Zmf C1,C2 )

proof end;

theorem :: FUZZY_3:6

for C1, C2 being non empty set
for f, g being RMembership_Func of C1,C2 st f \ g = Zmf C1,C2 holds
g c=

proof end;

theorem :: FUZZY_3:7

for C1, C2 being non empty set
for f, g being RMembership_Func of C1,C2 st min f,g = Zmf C1,C2 holds
f \ g = f

proof end;