:: Basic Properties of Fuzzy Set Operation and Membership Function
:: by Takashi Mitsuishi , Katsumi Wasaki and Yasunari Shidama
::
:: Received May 22, 2000
:: Copyright (c) 2000-2012 Association of Mizar Users


begin

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 )
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)
proof end;

definition
let C be non empty set ;
let f, g be Membership_Func of C;
func f \ g -> Membership_Func of C equals :: FUZZY_2:def 1
 min (f,(1_minus g));
correctness
coherence
min (f,(1_minus g)) is Membership_Func of C;
;
end;

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

theorem Th4: :: FUZZY_2:4
for C being non empty set
for f, g, h being Membership_Func of C st g c= holds
g \ h c=
proof end;

theorem :: FUZZY_2:5
for C being non empty set
for f, g, h being Membership_Func of C st g c= holds
h \ f c=
proof end;

theorem :: FUZZY_2:6
for C being non empty set
for f, g, h, h1 being Membership_Func of C st g c= & h1 c= holds
g \ h c=
proof end;

theorem :: FUZZY_2:7
for C being non empty set
for f being Membership_Func of C holds f \ (EMF C) = f
proof end;

theorem :: FUZZY_2:8
for C being non empty set
for f, g being Membership_Func of C holds f \ (min (f,g)) c=
proof end;

theorem :: FUZZY_2:9
for C being non empty set
for f, g being Membership_Func of C holds f c=
proof end;

theorem :: FUZZY_2:10
for C being non empty set
for f, g being Membership_Func of C holds max (f,g) c=
proof end;

theorem :: FUZZY_2:11
for C being non empty set
for f, g, h being Membership_Func of C holds f \ (g \ h) = max ((f \ g),(min (f,h)))
proof end;

theorem :: FUZZY_2:12
for C being non empty set
for f, g being Membership_Func of C holds f \ (f \ g) c=
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=
proof end;

theorem :: FUZZY_2:14
for C being non empty set
for f, g, h 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, g, h 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, g, h being Membership_Func of C holds (f \ g) \ h = f \ (max (g,h))
proof end;

theorem :: FUZZY_2:17
for C being non empty set
for f, g being Membership_Func of C holds (max (f,g)) \ (min (f,g)) c=
proof end;

theorem :: FUZZY_2:18
for C being non empty set
for f, g, h being Membership_Func of C st h c= & h c= holds
h c=
proof end;

theorem :: FUZZY_2:19
for C being non empty set
for f, g, h being Membership_Func of C holds (min (f,g)) \ (min (f,h)) c=
proof end;

theorem Th20: :: FUZZY_2:20
for C being non empty set
for f, g being Membership_Func of C holds (max (f,g)) \ (min (f,g)) c=
proof end;

theorem Th21: :: FUZZY_2:21
for C being non empty set
for f, g being Membership_Func of C holds 1_minus (f \+\ g) c=
proof end;

theorem :: FUZZY_2:22
for C being non empty set
for f, g, h being Membership_Func of C holds (f \+\ g) \ h = max ((f \ (max (g,h))),(g \ (max (f,h))))
proof end;

theorem :: FUZZY_2:23
for C being non empty set
for f, g, h being Membership_Func of C holds f \ (g \+\ h) c=
proof end;

theorem :: FUZZY_2:24
for C being non empty set
for f, g being Membership_Func of C st g c= holds
g c=
proof end;

theorem :: FUZZY_2:25
for C being non empty set
for f, g being Membership_Func of C holds max (f,g) c=
proof end;

theorem Th26: :: FUZZY_2:26
for C being non empty set
for f, g being Membership_Func of C st f \ g = EMF C holds
g c=
proof end;

theorem Th27: :: FUZZY_2:27
for C being non empty set
for f, g being Membership_Func of C st min (f,g) = EMF C holds
f \ g = f
proof end;

begin

definition
let C be non empty set ;
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
ex b1 being Membership_Func of C st
for c being Element of C holds b1 . c = (h . c) * (g . c)
proof end;
uniqueness
for b1, b2 being Membership_Func of C st ( for c being Element of C holds b1 . c = (h . c) * (g . c) ) & ( for c being Element of C holds b2 . c = (h . c) * (g . c) ) holds
b1 = b2
proof end;
commutativity
for b1, h, g being Membership_Func of C st ( for c being Element of C holds b1 . c = (h . c) * (g . c) ) holds
for c being Element of C holds b1 . c = (g . c) * (h . c) ;
end;

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

definition
let C be non empty set ;
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
ex b1 being Membership_Func of C st
for c being Element of C holds b1 . c = ((h . c) + (g . c)) - ((h . c) * (g . c))
proof end;
uniqueness
for b1, b2 being Membership_Func of C st ( for c being Element of C holds b1 . c = ((h . c) + (g . c)) - ((h . c) * (g . c)) ) & ( for c being Element of C holds b2 . c = ((h . c) + (g . c)) - ((h . c) * (g . c)) ) holds
b1 = b2
proof end;
commutativity
for b1, h, g being Membership_Func of C st ( for c being Element of C holds b1 . c = ((h . c) + (g . c)) - ((h . c) * (g . c)) ) holds
for c being Element of C holds b1 . c = ((g . c) + (h . c)) - ((g . c) * (h . c)) ;
end;

:: 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 Th28: :: FUZZY_2:28
for C being non empty set
for f being Membership_Func of C holds
( f c= & f ++ f c= )
proof end;

theorem Th29: :: FUZZY_2:29
for C being non empty set
for f, g, h being Membership_Func of C holds (f * g) * h = f * (g * h)
proof end;

theorem :: FUZZY_2:30
for C being non empty set
for f, g, h being Membership_Func of C holds (f ++ g) ++ h = f ++ (g ++ h)
proof end;

theorem :: FUZZY_2:31
for C being non empty set
for f, g being Membership_Func of C holds
( f c= & f ++ (f * g) c= )
proof end;

theorem :: FUZZY_2:32
for C being non empty set
for f, g, h being Membership_Func of C holds (f * g) ++ (f * h) c=
proof end;

theorem :: FUZZY_2:33
for C being non empty set
for f, g, h being Membership_Func of C holds f ++ (g * h) c=
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)
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)
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))
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 )
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 )
proof end;

theorem :: FUZZY_2:39
for C being non empty set
for f, g being Membership_Func of C holds min (f,g) c=
proof end;

theorem :: FUZZY_2:40
for C being non empty set
for f, g being Membership_Func of C holds f ++ g 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
for a, b, c being Real st 0 <= c holds
( c * (max (a,b)) = max ((c * a),(c * b)) & c * (min (a,b)) = min ((c * a),(c * b)) ) by Lm1, Lm2;

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)) )
proof end;

theorem :: FUZZY_2:43
for C being non empty set
for f, g, h 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, g, h 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, g, h 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, g, h being Membership_Func of C holds f ++ (min (g,h)) = min ((f ++ g),(f ++ h))
proof end;

theorem :: FUZZY_2:47
for C being non empty set
for f, g, h being Membership_Func of C holds max (f,(g * h)) c=
proof end;

theorem :: FUZZY_2:48
for C being non empty set
for f, g, h being Membership_Func of C holds min (f,(g * h)) c=
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)))
proof end;

theorem :: FUZZY_2:50
for C being non empty set
for f, g, h 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, g, h being Membership_Func of C holds (min (f,g)) ++ (min (f,h)) c=
proof end;

begin

registration
let C be non empty set ;
cluster V20([.0,1.]) V21() quasi_total -> for Element of bool [:C,REAL:];
coherence
for b1 being Membership_Func of C holds b1 is quasi_total ;
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_2:def 4
 chi ({},[:C1,C2:]);
correctness
coherence
chi ({},[:C1,C2:]) is RMembership_Func of C1,C2;
by FUZZY_1:12;
func Umf (C1,C2) -> RMembership_Func of C1,C2 equals :: FUZZY_2:def 5
 chi ([:C1,C2:],[:C1,C2:]);
correctness
coherence
chi ([:C1,C2:],[:C1,C2:]) is RMembership_Func of C1,C2;
by FUZZY_1:1;
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 :: 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 )
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) )
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) )
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=
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
proof end;