:: Basic Properties of Fuzzy Set Operation and Membership Function
:: by Takashi Mitsuishi , Katsumi Wasaki and Yasunari Shidama
::
:: Received May 22, 2000
:: Copyright (c) 2000 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 )

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

canceled;

theorem :: FUZZY_2:8

canceled;

theorem :: FUZZY_2:9

for C being non empty set
for f being Membership_Func of C holds f \ (EMF C) = f

proof end;

theorem :: FUZZY_2:10

canceled;

theorem :: FUZZY_2:11

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

for C being non empty set
for f, g being Membership_Func of C holds f 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 c=

proof end;

theorem :: FUZZY_2:14

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

for C being non empty set
for f, g being Membership_Func of C holds f \ (f \ g) c=

proof end;

theorem :: FUZZY_2:16

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

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

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

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: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 :: FUZZY_2:21

canceled;

theorem :: FUZZY_2:22

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

canceled;

theorem :: FUZZY_2:24

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 Th25: :: FUZZY_2:25

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 Th26: :: FUZZY_2:26

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

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

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

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

for C being non empty set
for f, g being Membership_Func of C holds max f,g c=

proof end;

theorem Th31: :: FUZZY_2:31

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 Th32: :: FUZZY_2:32

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;

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 b₁ being Membership_Func of C st
for c being Element of C holds b₁ . c = (h . c) * (g . c)

proof end;

uniqueness
for b₁, b₂ being Membership_Func of C st ( for c being Element of C holds b₁ . c = (h . c) * (g . c) ) & ( for c being Element of C holds b₂ . c = (h . c) * (g . c) ) holds
b₁ = b₂

proof end;

commutativity
for b₁, h, g being Membership_Func of C st ( for c being Element of C holds b₁ . c = (h . c) * (g . c) ) holds
for c being Element of C holds b₁ . c = (g . c) * (h . c) ;

end;

:: deftheorem Def2 defines * FUZZY_2:def 2 :

for C being non empty set
for h, g, b₄ being Membership_Func of C holds
( b₄ = h * g iff for c being Element of C holds b₄ . 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 b₁ being Membership_Func of C st
for c being Element of C holds b₁ . c = ((h . c) + (g . c)) - ((h . c) * (g . c))

proof end;

uniqueness
for b₁, b₂ being Membership_Func of C st ( for c being Element of C holds b₁ . c = ((h . c) + (g . c)) - ((h . c) * (g . c)) ) & ( for c being Element of C holds b₂ . c = ((h . c) + (g . c)) - ((h . c) * (g . c)) ) holds
b₁ = b₂

proof end;

commutativity
for b₁, h, g being Membership_Func of C st ( for c being Element of C holds b₁ . c = ((h . c) + (g . c)) - ((h . c) * (g . c)) ) holds
for c being Element of C holds b₁ . 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, b₄ being Membership_Func of C holds
( b₄ = h ++ g iff for c being Element of C holds b₄ . c = ((h . c) + (g . c)) - ((h . c) * (g . c)) );

theorem Th33: :: FUZZY_2:33

for C being non empty set
for f being Membership_Func of C holds
( f c= & f ++ f c= )

proof end;

theorem Th34: :: FUZZY_2:34

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

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

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

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

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

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

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 Th41: :: FUZZY_2:41

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

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

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

for C being non empty set
for f, g being Membership_Func of C holds min f,g c=

proof end;

theorem :: FUZZY_2:45

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

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

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

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

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

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

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

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

for C being non empty set
for f, g, h being Membership_Func of C holds min f,(g * h) c=

proof end;

theorem Th54: :: FUZZY_2:54

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

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

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;

registration

let C be non empty set ;
cluster -> Element of bool [:C,REAL :];
coherence
for b₁ being Membership_Func of C holds b₁ 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:13;
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:2;

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

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

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

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

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

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;