:: FUZZY_3 semantic presentation

registration

let c₁ be non empty set ;
cluster -> quasi_total Membership_Func of a₁;
coherence

proof end;

end;

definition

let c₁, c₂ be non empty set ;
mode RMembership_Func of a₁,a₂ is Membership_Func of [:a₁,a₂:];

end;

definition

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

end;

:: deftheorem Def1 defines Zmf FUZZY_3:def 1 :

:: deftheorem Def2 defines Umf FUZZY_3:def 2 :

theorem Th1: :: FUZZY_3:1

for b₁, b₂ being non empty set holds Zmf b₁,b₂ = EMF [:b₁,b₂:] by FUZZY_1:def 7;

theorem Th2: :: FUZZY_3:2

for b₁, b₂ being non empty set holds Umf b₁,b₂ = UMF [:b₁,b₂:] by FUZZY_1:def 8;

theorem Th3: :: FUZZY_3:3

for b₁, b₂ being non empty set
for b₃ being Element of [:b₁,b₂:]
for b₄ being RMembership_Func of b₁,b₂ holds
( (Zmf b₁,b₂) . b₃ <= b₄ . b₃ & b₄ . b₃ <= (Umf b₁,b₂) . b₃ )

proof end;

theorem Th4: :: FUZZY_3:4

for b₁, b₂ being non empty set
for b₃ being RMembership_Func of b₁,b₂ holds
( max b₃,(Umf b₁,b₂) = Umf b₁,b₂ & min b₃,(Umf b₁,b₂) = b₃ & max b₃,(Zmf b₁,b₂) = b₃ & min b₃,(Zmf b₁,b₂) = Zmf b₁,b₂ )

proof end;

theorem Th5: :: FUZZY_3:5

for b₁, b₂ being non empty set holds
( 1_minus (Zmf b₁,b₂) = Umf b₁,b₂ & 1_minus (Umf b₁,b₂) = Zmf b₁,b₂ )

proof end;

theorem Th6: :: FUZZY_3:6

for b₁, b₂ being non empty set
for b₃, b₄ being RMembership_Func of b₁,b₂ st b₃ \ b₄ = Zmf b₁,b₂ holds
b₄ c=

proof end;

theorem Th7: :: FUZZY_3:7

for b₁, b₂ being non empty set
for b₃, b₄ being RMembership_Func of b₁,b₂ st min b₃,b₄ = Zmf b₁,b₂ holds
b₃ \ b₄ = b₃

proof end;