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

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

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

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, h, g 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, h, g 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, h, g 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, h, g 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;

reconsider jj = 1 as Real ;

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 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, h, g 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, h, g 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, h, g 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, h, g 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, 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))

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

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

proof end;

theorem :: FUZZY_2:47

for C being non empty set
for f, h, g 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, h, g 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, 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=

proof end;

registration

let C be non empty set ;

cluster V5([.0,1.]) Function-like quasi_total -> for 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: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;