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


begin

:: Definition of Membership Function and Fuzzy Set
registration
let x, y be set ;
clusterK146(x,y) -> [.0,1.] -valued ;
coherence
 chi (x,y) is [.0,1.] -valued
proofend;
end;

registration
let C be non empty set ;
cluster non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued for Element of K6(K7(C,REAL));
existence
 ex b1 being Function of C,REAL st b1 is [.0,1.] -valued
proofend;
end;

definition
let C be non empty set ;
mode Membership_Func of C is [.0,1.] -valued Function of C,REAL;
end;

theorem :: FUZZY_1:1
for C being non empty set holds chi (C,C) is Membership_Func of C ;

registration
let X be non empty set ;
cluster[.0,1.] -valued Function-like V30(X, REAL )  ->  real-valued for Element of K6(K7(X,REAL));
coherence
 for b1 being Membership_Func of X holds b1 is real-valued ;
end;

definition
let f, g be real-valued Function;
predf is_less_than g means :Def1: :: FUZZY_1:def 1
( dom f c= dom g & ( for x being set st x in dom f holds
f . x <= g . x ) );
reflexivity
 for f being real-valued Function holds
( dom f c= dom f &amp; ( for x being set st x in dom f holds
f . x <= f . x ) ) ;
end;

:: deftheorem Def1 defines is_less_than FUZZY_1:def_1_:_
 for f, g being real-valued Function holds
( f is_less_than g iff ( dom f c= dom g &amp; ( for x being set st x in dom f holds
f . x <= g . x ) ) );

notation
let X be non empty set ;
let f, g be Membership_Func of X;
synonym f c= g for X is_less_than f;
end;

definition
let X be non empty set ;
let f, g be Membership_Func of X;
:: original:is_less_than
redefine predf is_less_than g means :Def2: :: FUZZY_1:def 2
 for x being Element of X holds f . x <= g . x;
compatibility
 ( f is_less_than g iff for x being Element of X holds f . x <= g . x )
proofend;
end;

:: deftheorem Def2 defines is_less_than FUZZY_1:def_2_:_
 for X being non empty set
for f, g being Membership_Func of X holds
( f is_less_than g iff for x being Element of X holds f . x <= g . x );

Lm1:  for C being non empty set
for f, g being Membership_Func of C st g c= &amp; f c= holds
f = g
proofend;

theorem :: FUZZY_1:2
for C being non empty set
for f, g being Membership_Func of C holds
( f = g iff ( g c= &amp; f c= ) ) by Lm1;

theorem :: FUZZY_1:3
for C being non empty set
for f being Membership_Func of C holds f c= ;

theorem :: FUZZY_1:4
for C being non empty set
for f, g, h being Membership_Func of C st g c= &amp; h c= holds
h c= ;

begin

:: Intersection,Union and Complement
definition
let C be non empty set ;
let h, g be Membership_Func of C;
func min (h,g) ->  Membership_Func of C means :Def3: :: FUZZY_1:def 3
 for c being Element of C holds it . c = min ((h . c),(g . c));
existence
 ex b1 being Membership_Func of C st
for c being Element of C holds b1 . c = min ((h . c),(g . c))
proofend;
uniqueness
 for b1, b2 being Membership_Func of C st ( for c being Element of C holds b1 . c = min ((h . c),(g . c)) ) &amp; ( for c being Element of C holds b2 . c = min ((h . c),(g . c)) ) holds
b1 = b2
proofend;
idempotence
 for h being Membership_Func of C
for c being Element of C holds h . c = min ((h . c),(h . c)) ;
commutativity
 for b1, h, g being Membership_Func of C st ( for c being Element of C holds b1 . c = min ((h . c),(g . c)) ) holds
for c being Element of C holds b1 . c = min ((g . c),(h . c)) ;
end;

:: deftheorem Def3 defines min FUZZY_1:def_3_:_
 for C being non empty set
for h, g, b4 being Membership_Func of C holds
( b4 = min (h,g) iff for c being Element of C holds b4 . c = min ((h . c),(g . c)) );

definition
let C be non empty set ;
let h, g be Membership_Func of C;
func max (h,g) ->  Membership_Func of C means :Def4: :: FUZZY_1:def 4
 for c being Element of C holds it . c = max ((h . c),(g . c));
existence
 ex b1 being Membership_Func of C st
for c being Element of C holds b1 . c = max ((h . c),(g . c))
proofend;
uniqueness
 for b1, b2 being Membership_Func of C st ( for c being Element of C holds b1 . c = max ((h . c),(g . c)) ) &amp; ( for c being Element of C holds b2 . c = max ((h . c),(g . c)) ) holds
b1 = b2
proofend;
idempotence
 for h being Membership_Func of C
for c being Element of C holds h . c = max ((h . c),(h . c)) ;
commutativity
 for b1, h, g being Membership_Func of C st ( for c being Element of C holds b1 . c = max ((h . c),(g . c)) ) holds
for c being Element of C holds b1 . c = max ((g . c),(h . c)) ;
end;

:: deftheorem Def4 defines max FUZZY_1:def_4_:_
 for C being non empty set
for h, g, b4 being Membership_Func of C holds
( b4 = max (h,g) iff for c being Element of C holds b4 . c = max ((h . c),(g . c)) );

definition
let C be non empty set ;
let h be Membership_Func of C;
func 1_minus h ->  Membership_Func of C means :Def5: :: FUZZY_1:def 5
 for c being Element of C holds it . c = 1 - (h . c);
existence
 ex b1 being Membership_Func of C st
for c being Element of C holds b1 . c = 1 - (h . c)
proofend;
uniqueness
 for b1, b2 being Membership_Func of C st ( for c being Element of C holds b1 . c = 1 - (h . c) ) &amp; ( for c being Element of C holds b2 . c = 1 - (h . c) ) holds
b1 = b2
proofend;
involutiveness
 for b1, b2 being Membership_Func of C st ( for c being Element of C holds b1 . c = 1 - (b2 . c) ) holds
for c being Element of C holds b2 . c = 1 - (b1 . c)
proofend;
end;

:: deftheorem Def5 defines 1_minus FUZZY_1:def_5_:_
 for C being non empty set
for h, b3 being Membership_Func of C holds
( b3 = 1_minus h iff for c being Element of C holds b3 . c = 1 - (h . c) );

theorem :: FUZZY_1:5
for C being non empty set
for c being Element of C
for h, g being Membership_Func of C holds
( min ((h . c),(g . c)) = (min (h,g)) . c &amp; max ((h . c),(g . c)) = (max (h,g)) . c ) by Def3, Def4;

theorem :: FUZZY_1:6
for C being non empty set
for h, f, g being Membership_Func of C holds
( max (h,h) = h &amp; min (h,h) = h &amp; max (h,h) = min (h,h) &amp; min (f,g) = min (g,f) &amp; max (f,g) = max (g,f) ) ;

theorem Th7: :: FUZZY_1:7
for C being non empty set
for f, g, h being Membership_Func of C holds
( max ((max (f,g)),h) = max (f,(max (g,h))) &amp; min ((min (f,g)),h) = min (f,(min (g,h))) )
proofend;

theorem Th8: :: FUZZY_1:8
for C being non empty set
for f, g being Membership_Func of C holds
( max (f,(min (f,g))) = f &amp; min (f,(max (f,g))) = f )
proofend;

theorem Th9: :: FUZZY_1:9
for C being non empty set
for f, g, h being Membership_Func of C holds
( min (f,(max (g,h))) = max ((min (f,g)),(min (f,h))) &amp; max (f,(min (g,h))) = min ((max (f,g)),(max (f,h))) )
proofend;

theorem :: FUZZY_1:10
canceled;

theorem Th11: :: FUZZY_1:11
for C being non empty set
for f, g being Membership_Func of C holds
( 1_minus (max (f,g)) = min ((1_minus f),(1_minus g)) &amp; 1_minus (min (f,g)) = max ((1_minus f),(1_minus g)) )
proofend;

begin

:: Empty Fuzzy Set and Universal Fuzzy Set
theorem :: FUZZY_1:12
for C being non empty set holds chi ({},C) is Membership_Func of C ;

definition
let C be non empty set ;
func EMF C ->  Membership_Func of C equals :: FUZZY_1:def 6
 chi ({},C);
correctness
coherence
chi ({},C) is Membership_Func of C;
;
end;

:: deftheorem  defines EMF FUZZY_1:def_6_:_
 for C being non empty set holds EMF C = chi ({},C);

definition
let C be non empty set ;
func UMF C ->  Membership_Func of C equals :: FUZZY_1:def 7
 chi (C,C);
correctness
coherence
chi (C,C) is Membership_Func of C;
;
end;

:: deftheorem  defines UMF FUZZY_1:def_7_:_
 for C being non empty set holds UMF C = chi (C,C);

theorem Th13: :: FUZZY_1:13
for C being non empty set
for a, b being Element of REAL
for f being PartFunc of C,REAL st rng f c= [.a,b.] &amp; a <= b holds
for x being Element of C st x in dom f holds
( a <= f . x &amp; f . x <= b )
proofend;

theorem Th14: :: FUZZY_1:14
for C being non empty set
for f being Membership_Func of C holds f c=
proofend;

theorem Th15: :: FUZZY_1:15
for C being non empty set
for f being Membership_Func of C holds UMF C c=
proofend;

theorem Th16: :: FUZZY_1:16
for C being non empty set
for x being Element of C
for h being Membership_Func of C holds
( (EMF C) . x <= h . x &amp; h . x <= (UMF C) . x )
proofend;

theorem Th17: :: FUZZY_1:17
for C being non empty set
for f, g being Membership_Func of C holds
( f c= &amp; max (f,g) c= )
proofend;

theorem Th18: :: FUZZY_1:18
for C being non empty set
for f being Membership_Func of C holds
( max (f,(UMF C)) = UMF C &amp; min (f,(UMF C)) = f &amp; max (f,(EMF C)) = f &amp; min (f,(EMF C)) = EMF C )
proofend;

theorem Th19: :: FUZZY_1:19
for C being non empty set
for f, h, g being Membership_Func of C st h c= &amp; h c= holds
h c=
proofend;

theorem :: FUZZY_1:20
for C being non empty set
for f, g, h being Membership_Func of C st g c= holds
max (g,h) c=
proofend;

theorem :: FUZZY_1:21
for C being non empty set
for f, g, h, h1 being Membership_Func of C st g c= &amp; h1 c= holds
max (g,h1) c=
proofend;

theorem :: FUZZY_1:22
for C being non empty set
for f, g being Membership_Func of C st g c= holds
max (f,g) = g
proofend;

theorem :: FUZZY_1:23
for C being non empty set
for f, g being Membership_Func of C holds max (f,g) c=
proofend;

theorem Th24: :: FUZZY_1:24
for C being non empty set
for h, f, g being Membership_Func of C st f c= &amp; g c= holds
min (f,g) c=
proofend;

theorem :: FUZZY_1:25
for C being non empty set
for f, g, h being Membership_Func of C st g c= holds
min (g,h) c=
proofend;

theorem :: FUZZY_1:26
for C being non empty set
for f, g, h, h1 being Membership_Func of C st g c= &amp; h1 c= holds
min (g,h1) c=
proofend;

theorem Th27: :: FUZZY_1:27
for C being non empty set
for f, g being Membership_Func of C st g c= holds
min (f,g) = f
proofend;

theorem :: FUZZY_1:28
for C being non empty set
for f, g, h being Membership_Func of C st g c= &amp; h c= &amp; min (g,h) = EMF C holds
f = EMF C
proofend;

theorem :: FUZZY_1:29
for C being non empty set
for f, g, h being Membership_Func of C st max ((min (f,g)),(min (f,h))) = f holds
max (g,h) c=
proofend;

theorem :: FUZZY_1:30
for C being non empty set
for f, g, h being Membership_Func of C st g c= &amp; min (g,h) = EMF C holds
min (f,h) = EMF C
proofend;

theorem :: FUZZY_1:31
for C being non empty set
for f being Membership_Func of C st EMF C c= holds
f = EMF C
proofend;

theorem :: FUZZY_1:32
for C being non empty set
for f, g being Membership_Func of C holds
( max (f,g) = EMF C iff ( f = EMF C &amp; g = EMF C ) )
proofend;

theorem :: FUZZY_1:33
for C being non empty set
for f, g, h being Membership_Func of C holds
( f = max (g,h) iff ( f c= &amp; f c= &amp; ( for h1 being Membership_Func of C st h1 c= &amp; h1 c= holds
h1 c= ) ) )
proofend;

theorem :: FUZZY_1:34
for C being non empty set
for f, g, h being Membership_Func of C holds
( f = min (g,h) iff ( g c= &amp; h c= &amp; ( for h1 being Membership_Func of C st g c= &amp; h c= holds
f c= ) ) )
proofend;

theorem :: FUZZY_1:35
for C being non empty set
for f, g, h being Membership_Func of C st max (g,h) c= &amp; min (f,h) = EMF C holds
g c=
proofend;

Lm2:  for C being non empty set
for f, g being Membership_Func of C st g c= holds
1_minus f c=
proofend;

theorem Th36: :: FUZZY_1:36
for C being non empty set
for f, g being Membership_Func of C holds
( g c= iff 1_minus f c= )
proofend;

theorem :: FUZZY_1:37
for C being non empty set
for f, g being Membership_Func of C st 1_minus g c= holds
1_minus f c=
proofend;

theorem :: FUZZY_1:38
for C being non empty set
for f, g being Membership_Func of C holds 1_minus f c=
proofend;

theorem :: FUZZY_1:39
for C being non empty set
for f, g being Membership_Func of C holds 1_minus (min (f,g)) c=
proofend;

theorem Th40: :: FUZZY_1:40
for C being non empty set holds
( 1_minus (EMF C) = UMF C &amp; 1_minus (UMF C) = EMF C )
proofend;

:: Exclusive Sum, Absolute Difference
definition
let C be non empty set ;
let h, g be Membership_Func of C;
funch \+\ g ->  Membership_Func of C equals :: FUZZY_1:def 8
 max ((min (h,(1_minus g))),(min ((1_minus h),g)));
coherence
 max ((min (h,(1_minus g))),(min ((1_minus h),g))) is Membership_Func of C ;
commutativity
 for b1, h, g being Membership_Func of C st b1 = max ((min (h,(1_minus g))),(min ((1_minus h),g))) holds
b1 = max ((min (g,(1_minus h))),(min ((1_minus g),h))) ;
end;

:: deftheorem  defines \+\ FUZZY_1:def_8_:_
 for C being non empty set
for h, g being Membership_Func of C holds h \+\ g = max ((min (h,(1_minus g))),(min ((1_minus h),g)));

theorem :: FUZZY_1:41
for C being non empty set
for f being Membership_Func of C holds f \+\ (EMF C) = f
proofend;

theorem :: FUZZY_1:42
for C being non empty set
for f being Membership_Func of C holds f \+\ (UMF C) = 1_minus f
proofend;

theorem :: FUZZY_1:43
for C being non empty set
for f, g, h being Membership_Func of C holds min ((min ((max (f,g)),(max (g,h)))),(max (h,f))) = max ((max ((min (f,g)),(min (g,h)))),(min (h,f)))
proofend;

theorem :: FUZZY_1:44
for C being non empty set
for f, g being Membership_Func of C holds 1_minus (f \+\ g) c=
proofend;

theorem :: FUZZY_1:45
for C being non empty set
for f, g being Membership_Func of C holds max (f,g) c=
proofend;

theorem :: FUZZY_1:46
for C being non empty set
for f being Membership_Func of C holds f \+\ f = min (f,(1_minus f)) ;

definition
let C be non empty set ;
let h, g be Membership_Func of C;
func ab_difMF (h,g) ->  Membership_Func of C means :: FUZZY_1:def 9
 for c being Element of C holds it . c = abs ((h . c) - (g . c));
existence
 ex b1 being Membership_Func of C st
for c being Element of C holds b1 . c = abs ((h . c) - (g . c))
proofend;
uniqueness
 for b1, b2 being Membership_Func of C st ( for c being Element of C holds b1 . c = abs ((h . c) - (g . c)) ) &amp; ( for c being Element of C holds b2 . c = abs ((h . c) - (g . c)) ) holds
b1 = b2
proofend;
end;

:: deftheorem  defines ab_difMF FUZZY_1:def_9_:_
 for C being non empty set
for h, g, b4 being Membership_Func of C holds
( b4 = ab_difMF (h,g) iff for c being Element of C holds b4 . c = abs ((h . c) - (g . c)) );