:: 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 C be non empty set ;

ex b_{1} being Function of C,REAL st b_{1} is [.0,1.] -valued

end;
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 b

proof end;

definition
end;

registration

let X be non empty set ;

coherence

for b_{1} being Membership_Func of X holds b_{1} is real-valued
;

end;
coherence

for b

definition

let f, g be real-valued Function;

for f being real-valued Function holds

( dom f c= dom f & ( for x being set st x in dom f holds

f . x <= f . x ) ) ;

end;
pred f 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 ( dom f c= dom g & ( for x being set st x in dom f holds

f . x <= g . x ) );

for f being real-valued Function holds

( dom f c= dom f & ( for x being set st x in dom f holds

f . x <= f . x ) ) ;

:: 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 & ( for x being set st x in dom f holds

f . x <= g . x ) ) );

for f, g being real-valued Function holds

( f is_less_than g iff ( dom f c= dom g & ( for x being set st x in dom f holds

f . x <= g . x ) ) );

notation
end;

definition

let X be non empty set ;

let f, g be Membership_Func of X;

( f is_less_than g iff for x being Element of X holds f . x <= g . x )

end;
let f, g be Membership_Func of X;

:: original: is_less_than

redefine pred f is_less_than g means :Def2: :: FUZZY_1:def 2

for x being Element of X holds f . x <= g . x;

compatibility redefine pred f is_less_than g means :Def2: :: FUZZY_1:def 2

for x being Element of X holds f . x <= g . x;

( f is_less_than g iff for x being Element of X holds f . x <= g . x )

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

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= & f c= holds

f = g

proof end;

theorem :: FUZZY_1:2

theorem :: FUZZY_1:4

begin

:: Intersection,Union and Complement

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 = min ((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 = min ((h . c),(g . c)) ) & ( for c being Element of C holds b_{2} . c = min ((h . c),(g . c)) ) holds

b_{1} = b_{2}

for h being Membership_Func of C

for c being Element of C holds h . c = min ((h . c),(h . c)) ;

commutativity

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

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

end;
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 for c being Element of C holds it . c = min ((h . c),(g . c));

ex b

for c being Element of C holds b

proof end;

uniqueness for b

b

proof end;

idempotence for h being Membership_Func of C

for c being Element of C holds h . c = min ((h . c),(h . c)) ;

commutativity

for b

for c being Element of C holds b

:: deftheorem Def3 defines min FUZZY_1:def 3 :

for C being non empty set

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

( b_{4} = min (h,g) iff for c being Element of C holds b_{4} . c = min ((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 = max ((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 = max ((h . c),(g . c)) ) & ( for c being Element of C holds b_{2} . c = max ((h . c),(g . c)) ) holds

b_{1} = b_{2}

for h being Membership_Func of C

for c being Element of C holds h . c = max ((h . c),(h . c)) ;

commutativity

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

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

end;
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 for c being Element of C holds it . c = max ((h . c),(g . c));

ex b

for c being Element of C holds b

proof end;

uniqueness for b

b

proof end;

idempotence for h being Membership_Func of C

for c being Element of C holds h . c = max ((h . c),(h . c)) ;

commutativity

for b

for c being Element of C holds b

:: deftheorem Def4 defines max FUZZY_1:def 4 :

for C being non empty set

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

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

for C being non empty set

for h, g, b

( b

definition

let C be non empty set ;

let h be Membership_Func of C;

ex b_{1} being Membership_Func of C st

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

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

b_{1} = b_{2}

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

for c being Element of C holds b_{2} . c = 1 - (b_{1} . c)

end;
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 for c being Element of C holds it . c = 1 - (h . c);

ex b

for c being Element of C holds b

proof end;

uniqueness for b

b

proof end;

involutiveness for b

for c being Element of C holds b

proof end;

:: deftheorem Def5 defines 1_minus FUZZY_1:def 5 :

for C being non empty set

for h, b_{3} being Membership_Func of C holds

( b_{3} = 1_minus h iff for c being Element of C holds b_{3} . c = 1 - (h . c) );

for C being non empty set

for h, b

( b

theorem :: FUZZY_1:5

theorem :: FUZZY_1:6

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))) & min ((min (f,g)),h) = min (f,(min (g,h))) )

for f, g, h being Membership_Func of C holds

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

proof end;

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 & min (f,(max (f,g))) = f )

for f, g being Membership_Func of C holds

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

proof end;

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))) & max (f,(min (g,h))) = min ((max (f,g)),(max (f,h))) )

for f, g, h being Membership_Func of C holds

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

proof end;

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)) & 1_minus (min (f,g)) = max ((1_minus f),(1_minus g)) )

for f, g being Membership_Func of C holds

( 1_minus (max (f,g)) = min ((1_minus f),(1_minus g)) & 1_minus (min (f,g)) = max ((1_minus f),(1_minus g)) )

proof end;

begin

:: Empty Fuzzy Set and Universal Fuzzy Set

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.] & a <= b holds

for x being Element of C st x in dom f holds

( a <= f . x & f . x <= b )

for a, b being Element of REAL

for f being PartFunc of C,REAL st rng f c= [.a,b.] & a <= b holds

for x being Element of C st x in dom f holds

( a <= f . x & f . x <= b )

proof end;

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 & h . x <= (UMF C) . x )

for x being Element of C

for h being Membership_Func of C holds

( (EMF C) . x <= h . x & h . x <= (UMF C) . x )

proof end;

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 & min (f,(UMF C)) = f & max (f,(EMF C)) = f & min (f,(EMF C)) = EMF C )

for f being Membership_Func of C holds

( max (f,(UMF C)) = UMF C & min (f,(UMF C)) = f & max (f,(EMF C)) = f & min (f,(EMF C)) = EMF C )

proof end;

theorem :: FUZZY_1:21

for C being non empty set

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

max (g,h1) c=

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

max (g,h1) c=

proof end;

theorem :: FUZZY_1:26

for C being non empty set

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

min (g,h1) c=

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

min (g,h1) c=

proof end;

theorem :: FUZZY_1:28

for C being non empty set

for f, g, h being Membership_Func of C st g c= & h c= & min (g,h) = EMF C holds

f = EMF C

for f, g, h being Membership_Func of C st g c= & h c= & min (g,h) = EMF C holds

f = EMF C

proof end;

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=

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

max (g,h) c=

proof end;

theorem :: FUZZY_1:30

for C being non empty set

for f, g, h being Membership_Func of C st g c= & min (g,h) = EMF C holds

min (f,h) = EMF C

for f, g, h being Membership_Func of C st g c= & min (g,h) = EMF C holds

min (f,h) = EMF C

proof end;

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 & g = EMF C ) )

for f, g being Membership_Func of C holds

( max (f,g) = EMF C iff ( f = EMF C & g = EMF C ) )

proof end;

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= & f c= & ( for h1 being Membership_Func of C st h1 c= & h1 c= holds

h1 c= ) ) )

for f, g, h being Membership_Func of C holds

( f = max (g,h) iff ( f c= & f c= & ( for h1 being Membership_Func of C st h1 c= & h1 c= holds

h1 c= ) ) )

proof end;

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= & h c= & ( for h1 being Membership_Func of C st g c= & h c= holds

f c= ) ) )

for f, g, h being Membership_Func of C holds

( f = min (g,h) iff ( g c= & h c= & ( for h1 being Membership_Func of C st g c= & h c= holds

f c= ) ) )

proof end;

theorem :: FUZZY_1:35

for C being non empty set

for f, g, h being Membership_Func of C st max (g,h) c= & min (f,h) = EMF C holds

g c=

for f, g, h being Membership_Func of C st max (g,h) c= & min (f,h) = EMF C holds

g c=

proof end;

Lm2: for C being non empty set

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

1_minus f c=

proof end;

:: Exclusive Sum, Absolute Difference

definition

let C be non empty set ;

let h, g be Membership_Func of C;

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

commutativity

for b_{1}, h, g being Membership_Func of C st b_{1} = max ((min (h,(1_minus g))),(min ((1_minus h),g))) holds

b_{1} = max ((min (g,(1_minus h))),(min ((1_minus g),h)))
;

end;
let h, g be Membership_Func of C;

func h \+\ 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)));

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

commutativity

for b

b

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

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

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

proof end;

theorem :: FUZZY_1:46

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 = abs ((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 = abs ((h . c) - (g . c)) ) & ( for c being Element of C holds b_{2} . c = abs ((h . c) - (g . c)) ) holds

b_{1} = b_{2}

end;
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 for c being Element of C holds it . c = abs ((h . c) - (g . c));

ex b

for c being Element of C holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem defines ab_difMF FUZZY_1:def 9 :

for C being non empty set

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

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

for C being non empty set

for h, g, b

( b