:: FUZZY_2 semantic presentation

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 ;

end;

:: deftheorem defines \ FUZZY_2:def 1 :

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, g being Membership_Func of C holds f c= by FUZZY_1:18;

theorem :: FUZZY_2:8

for C being non empty set
for f, g being Membership_Func of C holds f \+\ g c= by FUZZY_1:18;

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

for C being non empty set
for f being Membership_Func of C holds (EMF C) \ f = EMF C by FUZZY_1:19;

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

for C being non empty set
for f, g, h being Membership_Func of C holds (max f,g) \ h = max (f \ h),(g \ h) by FUZZY_1:10;

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

for C being non empty set
for f, g, h being Membership_Func of C holds min f,(g \ h) = (min f,g) \ h by FUZZY_1:8;

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

proof end;

uniqueness

proof end;

commutativity ;

end;

:: deftheorem Def2 defines * FUZZY_2:def 2 :

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

proof end;

uniqueness

proof end;

commutativity ;

end;

:: deftheorem Def3 defines ++ FUZZY_2:def 3 :

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;