:: by Takashi Mitsuishi , Katsumi Wasaki and Yasunari Shidama

::

:: Received May 22, 2000

:: Copyright (c) 2000-2016 Association of Mizar Users

theorem Th1: :: FUZZY_2:1

for C being non empty set

for x being Element of C

for h being Membership_Func of C holds

( 0 <= h . x & h . x <= 1 )

for x being Element of C

for h being Membership_Func of C holds

( 0 <= h . x & h . x <= 1 )

proof end;

theorem :: FUZZY_2:2

for C being non empty set

for f, h, g being Membership_Func of C st h c= holds

max (f,(min (g,h))) = min ((max (f,g)),h)

for f, h, g being Membership_Func of C st h c= holds

max (f,(min (g,h))) = min ((max (f,g)),h)

proof end;

definition

let C be non empty set ;

let f, g be Membership_Func of C;

correctness

coherence

min (f,(1_minus g)) is Membership_Func of C;

;

end;
let f, g be Membership_Func of C;

correctness

coherence

min (f,(1_minus g)) is Membership_Func of C;

;

:: 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));

for C being non empty set

for f, g being Membership_Func of C holds f \ g = min (f,(1_minus g));

theorem :: FUZZY_2:3

for C being non empty set

for f, g being Membership_Func of C holds 1_minus (f \ g) = max ((1_minus f),g)

for f, g being Membership_Func of C holds 1_minus (f \ g) = max ((1_minus f),g)

proof end;

theorem :: FUZZY_2:11

for C being non empty set

for f, h, g being Membership_Func of C holds f \ (g \ h) = max ((f \ g),(min (f,h)))

for f, h, g being Membership_Func of C holds f \ (g \ h) = max ((f \ g),(min (f,h)))

proof end;

theorem :: FUZZY_2:13

for C being non empty set

for f, g being Membership_Func of C holds (max (f,g)) \ g c= by Th4, FUZZY_1:17;

for f, g being Membership_Func of C holds (max (f,g)) \ g c= by Th4, FUZZY_1:17;

theorem :: FUZZY_2:14

for C being non empty set

for f, h, g being Membership_Func of C holds f \ (max (g,h)) = min ((f \ g),(f \ h))

for f, h, g being Membership_Func of C holds f \ (max (g,h)) = min ((f \ g),(f \ h))

proof end;

theorem :: FUZZY_2:15

for C being non empty set

for f, h, g being Membership_Func of C holds f \ (min (g,h)) = max ((f \ g),(f \ h))

for f, h, g being Membership_Func of C holds f \ (min (g,h)) = max ((f \ g),(f \ h))

proof end;

theorem :: FUZZY_2:16

for C being non empty set

for f, h, g being Membership_Func of C holds (f \ g) \ h = f \ (max (g,h))

for f, h, g being Membership_Func of C holds (f \ g) \ h = f \ (max (g,h))

proof end;

theorem :: FUZZY_2:22

for C being non empty set

for f, h, g being Membership_Func of C holds (f \+\ g) \ h = max ((f \ (max (g,h))),(g \ (max (f,h))))

for f, h, g being Membership_Func of C holds (f \+\ g) \ h = max ((f \ (max (g,h))),(g \ (max (f,h))))

proof end;

reconsider jj = 1 as Real ;

definition

let C be non empty set ;

let h, g be Membership_Func of C;

ex b_{1} being Membership_Func of C st

for c being Element of C holds b_{1} . c = (h . c) * (g . c)

for b_{1}, b_{2} being Membership_Func of C st ( for c being Element of C holds b_{1} . c = (h . c) * (g . c) ) & ( for c being Element of C holds b_{2} . c = (h . c) * (g . c) ) holds

b_{1} = b_{2}

for b_{1}, h, g being Membership_Func of C st ( for c being Element of C holds b_{1} . c = (h . c) * (g . c) ) holds

for c being Element of C holds b_{1} . c = (g . c) * (h . c)
;

end;
let h, g be Membership_Func of C;

func h * g -> Membership_Func of C means :Def2: :: FUZZY_2:def 2

for c being Element of C holds it . c = (h . c) * (g . c);

existence for c being Element of C holds it . c = (h . c) * (g . c);

ex b

for c being Element of C holds b

proof end;

uniqueness for b

b

proof end;

commutativity for b

for c being Element of C holds b

:: deftheorem Def2 defines * FUZZY_2:def 2 :

for C being non empty set

for h, g, b_{4} being Membership_Func of C holds

( b_{4} = h * g iff for c being Element of C holds b_{4} . c = (h . c) * (g . c) );

for C being non empty set

for h, g, b

( b

definition

let C be non empty set ;

let h, g be Membership_Func of C;

ex b_{1} being Membership_Func of C st

for c being Element of C holds b_{1} . c = ((h . c) + (g . c)) - ((h . c) * (g . c))

for b_{1}, b_{2} being Membership_Func of C st ( for c being Element of C holds b_{1} . c = ((h . c) + (g . c)) - ((h . c) * (g . c)) ) & ( for c being Element of C holds b_{2} . c = ((h . c) + (g . c)) - ((h . c) * (g . c)) ) holds

b_{1} = b_{2}

for b_{1}, h, g being Membership_Func of C st ( for c being Element of C holds b_{1} . c = ((h . c) + (g . c)) - ((h . c) * (g . c)) ) holds

for c being Element of C holds b_{1} . c = ((g . c) + (h . c)) - ((g . c) * (h . c))
;

end;
let h, g be Membership_Func of C;

func h ++ g -> Membership_Func of C means :Def3: :: FUZZY_2:def 3

for c being Element of C holds it . c = ((h . c) + (g . c)) - ((h . c) * (g . c));

existence for c being Element of C holds it . c = ((h . c) + (g . c)) - ((h . c) * (g . c));

ex b

for c being Element of C holds b

proof end;

uniqueness for b

b

proof end;

commutativity for b

for c being Element of C holds b

:: deftheorem Def3 defines ++ FUZZY_2:def 3 :

for C being non empty set

for h, g, b_{4} being Membership_Func of C holds

( b_{4} = h ++ g iff for c being Element of C holds b_{4} . c = ((h . c) + (g . c)) - ((h . c) * (g . c)) );

for C being non empty set

for h, g, b

( b

theorem :: FUZZY_2:30

for C being non empty set

for f, h, g being Membership_Func of C holds (f ++ g) ++ h = f ++ (g ++ h)

for f, h, g being Membership_Func of C holds (f ++ g) ++ h = f ++ (g ++ h)

proof end;

theorem :: FUZZY_2:34

for C being non empty set

for f, g being Membership_Func of C holds 1_minus (f * g) = (1_minus f) ++ (1_minus g)

for f, g being Membership_Func of C holds 1_minus (f * g) = (1_minus f) ++ (1_minus g)

proof end;

theorem :: FUZZY_2:35

for C being non empty set

for f, g being Membership_Func of C holds 1_minus (f ++ g) = (1_minus f) * (1_minus g)

for f, g being Membership_Func of C holds 1_minus (f ++ g) = (1_minus f) * (1_minus g)

proof end;

theorem Th36: :: FUZZY_2:36

for C being non empty set

for f, g being Membership_Func of C holds f ++ g = 1_minus ((1_minus f) * (1_minus g))

for f, g being Membership_Func of C holds f ++ g = 1_minus ((1_minus f) * (1_minus g))

proof end;

theorem :: FUZZY_2:37

for C being non empty set

for f being Membership_Func of C holds

( f * (EMF C) = EMF C & f * (UMF C) = f )

for f being Membership_Func of C holds

( f * (EMF C) = EMF C & f * (UMF C) = f )

proof end;

theorem :: FUZZY_2:38

for C being non empty set

for f being Membership_Func of C holds

( f ++ (EMF C) = f & f ++ (UMF C) = UMF C )

for f being Membership_Func of C holds

( f ++ (EMF C) = f & f ++ (UMF C) = UMF C )

proof end;

Lm1: for a, b, c being Real st 0 <= c holds

c * (min (a,b)) = min ((c * a),(c * b))

proof end;

Lm2: for a, b, c being Real st 0 <= c holds

c * (max (a,b)) = max ((c * a),(c * b))

proof end;

theorem :: FUZZY_2:41

theorem :: FUZZY_2:42

for a, b, c being Real holds

( c + (max (a,b)) = max ((c + a),(c + b)) & c + (min (a,b)) = min ((c + a),(c + b)) )

( c + (max (a,b)) = max ((c + a),(c + b)) & c + (min (a,b)) = min ((c + a),(c + b)) )

proof end;

theorem :: FUZZY_2:43

for C being non empty set

for f, h, g being Membership_Func of C holds f * (max (g,h)) = max ((f * g),(f * h))

for f, h, g being Membership_Func of C holds f * (max (g,h)) = max ((f * g),(f * h))

proof end;

theorem :: FUZZY_2:44

for C being non empty set

for f, h, g being Membership_Func of C holds f * (min (g,h)) = min ((f * g),(f * h))

for f, h, g being Membership_Func of C holds f * (min (g,h)) = min ((f * g),(f * h))

proof end;

theorem :: FUZZY_2:45

for C being non empty set

for f, h, g being Membership_Func of C holds f ++ (max (g,h)) = max ((f ++ g),(f ++ h))

for f, h, g being Membership_Func of C holds f ++ (max (g,h)) = max ((f ++ g),(f ++ h))

proof end;

theorem :: FUZZY_2:46

for C being non empty set

for f, h, g being Membership_Func of C holds f ++ (min (g,h)) = min ((f ++ g),(f ++ h))

for f, h, g being Membership_Func of C holds f ++ (min (g,h)) = min ((f ++ g),(f ++ h))

proof end;

theorem Th49: :: FUZZY_2:49

for C being non empty set

for c being Element of C

for f, g being Membership_Func of C holds (f ++ g) . c = 1 - ((1 - (f . c)) * (1 - (g . c)))

for c being Element of C

for f, g being Membership_Func of C holds (f ++ g) . c = 1 - ((1 - (f . c)) * (1 - (g . c)))

proof end;

theorem :: FUZZY_2:50

for C being non empty set

for f, h, g being Membership_Func of C holds (max (f,g)) ++ (max (f,h)) c=

for f, h, g being Membership_Func of C holds (max (f,g)) ++ (max (f,h)) c=

proof end;

theorem :: FUZZY_2:51

for C being non empty set

for f, h, g being Membership_Func of C holds (min (f,g)) ++ (min (f,h)) c=

for f, h, g being Membership_Func of C holds (min (f,g)) ++ (min (f,h)) c=

proof end;

registration

let C be non empty set ;

coherence

for b_{1} being Membership_Func of C holds b_{1} is quasi_total
;

end;
coherence

for b

definition
end;

definition

let C1, C2 be non empty set ;

correctness

coherence

chi ({},[:C1,C2:]) is RMembership_Func of C1,C2;

by FUZZY_1:12;

correctness

coherence

chi ([:C1,C2:],[:C1,C2:]) is RMembership_Func of C1,C2;

by FUZZY_1:1;

end;
correctness

coherence

chi ({},[:C1,C2:]) is RMembership_Func of C1,C2;

by FUZZY_1:12;

correctness

coherence

chi ([:C1,C2:],[:C1,C2:]) is RMembership_Func of C1,C2;

by FUZZY_1:1;

:: deftheorem defines Zmf FUZZY_2:def 4 :

for C1, C2 being non empty set holds Zmf (C1,C2) = chi ({},[:C1,C2:]);

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:]);

for C1, C2 being non empty set holds Umf (C1,C2) = chi ([:C1,C2:],[:C1,C2:]);

theorem :: FUZZY_2:52

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 )

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_2:53

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) )

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_2:54

for C1, C2 being non empty set holds

( 1_minus (Zmf (C1,C2)) = Umf (C1,C2) & 1_minus (Umf (C1,C2)) = Zmf (C1,C2) )

( 1_minus (Zmf (C1,C2)) = Umf (C1,C2) & 1_minus (Umf (C1,C2)) = Zmf (C1,C2) )

proof end;

theorem :: FUZZY_2:55

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=

for f, g being RMembership_Func of C1,C2 st f \ g = Zmf (C1,C2) holds

g c=

proof end;

theorem :: FUZZY_2:56

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

for f, g being RMembership_Func of C1,C2 st min (f,g) = Zmf (C1,C2) holds

f \ g = f

proof end;