:: by Noboru Endou , Takashi Mitsuishi and Keiji Ohkubo

::

:: Received June 25, 2001

:: Copyright (c) 2001-2019 Association of Mizar Users

registration
end;

reconsider jj = 1 as Real ;

theorem Th1: :: FUZZY_4:1

for C1 being non empty set

for F being Membership_Func of C1 holds

( rng F is real-bounded & ( for x being set st x in dom F holds

F . x <= upper_bound (rng F) ) & ( for x being set st x in dom F holds

F . x >= lower_bound (rng F) ) )

for F being Membership_Func of C1 holds

( rng F is real-bounded & ( for x being set st x in dom F holds

F . x <= upper_bound (rng F) ) & ( for x being set st x in dom F holds

F . x >= lower_bound (rng F) ) )

proof end;

theorem :: FUZZY_4:2

for C1 being non empty set

for F, G being Membership_Func of C1 st ( for x being set st x in C1 holds

F . x <= G . x ) holds

upper_bound (rng F) <= upper_bound (rng G)

for F, G being Membership_Func of C1 st ( for x being set st x in C1 holds

F . x <= G . x ) holds

upper_bound (rng F) <= upper_bound (rng G)

proof end;

theorem Th3: :: FUZZY_4:3

for C1, C2 being non empty set

for f being RMembership_Func of C1,C2

for c being set holds

( 0 <= f . c & f . c <= 1 )

for f being RMembership_Func of C1,C2

for c being set holds

( 0 <= f . c & f . c <= 1 )

proof end;

theorem :: FUZZY_4:4

notation
end;

definition

let C1, C2 be non empty set ;

let h be RMembership_Func of C2,C1;

converse is RMembership_Func of C1,C2

for b_{1} being RMembership_Func of C1,C2 holds

( b_{1} = converse iff for x, y being object st [x,y] in [:C1,C2:] holds

b_{1} . (x,y) = h . (y,x) )

end;
let h be RMembership_Func of C2,C1;

:: original: converse

redefine func converse h -> RMembership_Func of C1,C2 means :Def1: :: FUZZY_4:def 1

for x, y being object st [x,y] in [:C1,C2:] holds

it . (x,y) = h . (y,x);

coherence redefine func converse h -> RMembership_Func of C1,C2 means :Def1: :: FUZZY_4:def 1

for x, y being object st [x,y] in [:C1,C2:] holds

it . (x,y) = h . (y,x);

converse is RMembership_Func of C1,C2

proof end;

compatibility for b

( b

b

proof end;

:: deftheorem Def1 defines converse FUZZY_4:def 1 :

for C1, C2 being non empty set

for h being RMembership_Func of C2,C1

for b_{4} being RMembership_Func of C1,C2 holds

( b_{4} = converse h iff for x, y being object st [x,y] in [:C1,C2:] holds

b_{4} . (x,y) = h . (y,x) );

for C1, C2 being non empty set

for h being RMembership_Func of C2,C1

for b

( b

b

theorem :: FUZZY_4:5

for C1, C2 being non empty set

for f being RMembership_Func of C1,C2 holds converse (converse f) = f

for f being RMembership_Func of C1,C2 holds converse (converse f) = f

proof end;

theorem Th6: :: FUZZY_4:6

for C1, C2 being non empty set

for f being RMembership_Func of C1,C2 holds 1_minus (converse f) = converse (1_minus f)

for f being RMembership_Func of C1,C2 holds 1_minus (converse f) = converse (1_minus f)

proof end;

theorem Th7: :: FUZZY_4:7

for C1, C2 being non empty set

for f, g being RMembership_Func of C1,C2 holds converse (max (f,g)) = max ((converse f),(converse g))

for f, g being RMembership_Func of C1,C2 holds converse (max (f,g)) = max ((converse f),(converse g))

proof end;

theorem Th8: :: FUZZY_4:8

for C1, C2 being non empty set

for f, g being RMembership_Func of C1,C2 holds converse (min (f,g)) = min ((converse f),(converse g))

for f, g being RMembership_Func of C1,C2 holds converse (min (f,g)) = min ((converse f),(converse g))

proof end;

theorem Th9: :: FUZZY_4:9

for C1, C2 being non empty set

for f, g being RMembership_Func of C1,C2

for x, y being set st x in C1 & y in C2 & f . [x,y] <= g . [x,y] holds

(converse f) . [y,x] <= (converse g) . [y,x]

for f, g being RMembership_Func of C1,C2

for x, y being set st x in C1 & y in C2 & f . [x,y] <= g . [x,y] holds

(converse f) . [y,x] <= (converse g) . [y,x]

proof end;

theorem :: FUZZY_4:11

for C1, C2 being non empty set

for f, g being RMembership_Func of C1,C2 holds converse (f \ g) = (converse f) \ (converse g)

for f, g being RMembership_Func of C1,C2 holds converse (f \ g) = (converse f) \ (converse g)

proof end;

theorem :: FUZZY_4:12

for C1, C2 being non empty set

for f, g being RMembership_Func of C1,C2 holds converse (f \+\ g) = (converse f) \+\ (converse g)

for f, g being RMembership_Func of C1,C2 holds converse (f \+\ g) = (converse f) \+\ (converse g)

proof end;

:: Definition and properties of the composition

definition

let C1, C2, C3 be non empty set ;

let h be RMembership_Func of C1,C2;

let g be RMembership_Func of C2,C3;

let x, z be object ;

assume that

A1: x in C1 and

A2: z in C3 ;

ex b_{1} being Membership_Func of C2 st

for y being Element of C2 holds b_{1} . y = min ((h . [x,y]),(g . [y,z]))

for b_{1}, b_{2} being Membership_Func of C2 st ( for y being Element of C2 holds b_{1} . y = min ((h . [x,y]),(g . [y,z])) ) & ( for y being Element of C2 holds b_{2} . y = min ((h . [x,y]),(g . [y,z])) ) holds

b_{1} = b_{2}

end;
let h be RMembership_Func of C1,C2;

let g be RMembership_Func of C2,C3;

let x, z be object ;

assume that

A1: x in C1 and

A2: z in C3 ;

func min (h,g,x,z) -> Membership_Func of C2 means :Def2: :: FUZZY_4:def 2

for y being Element of C2 holds it . y = min ((h . [x,y]),(g . [y,z]));

existence for y being Element of C2 holds it . y = min ((h . [x,y]),(g . [y,z]));

ex b

for y being Element of C2 holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def2 defines min FUZZY_4:def 2 :

for C1, C2, C3 being non empty set

for h being RMembership_Func of C1,C2

for g being RMembership_Func of C2,C3

for x, z being object st x in C1 & z in C3 holds

for b_{8} being Membership_Func of C2 holds

( b_{8} = min (h,g,x,z) iff for y being Element of C2 holds b_{8} . y = min ((h . [x,y]),(g . [y,z])) );

for C1, C2, C3 being non empty set

for h being RMembership_Func of C1,C2

for g being RMembership_Func of C2,C3

for x, z being object st x in C1 & z in C3 holds

for b

( b

definition

let C1, C2, C3 be non empty set ;

let h be RMembership_Func of C1,C2;

let g be RMembership_Func of C2,C3;

ex b_{1} being RMembership_Func of C1,C3 st

for x, z being object st [x,z] in [:C1,C3:] holds

b_{1} . (x,z) = upper_bound (rng (min (h,g,x,z)))

for b_{1}, b_{2} being RMembership_Func of C1,C3 st ( for x, z being object st [x,z] in [:C1,C3:] holds

b_{1} . (x,z) = upper_bound (rng (min (h,g,x,z))) ) & ( for x, z being object st [x,z] in [:C1,C3:] holds

b_{2} . (x,z) = upper_bound (rng (min (h,g,x,z))) ) holds

b_{1} = b_{2}

end;
let h be RMembership_Func of C1,C2;

let g be RMembership_Func of C2,C3;

func h (#) g -> RMembership_Func of C1,C3 means :Def3: :: FUZZY_4:def 3

for x, z being object st [x,z] in [:C1,C3:] holds

it . (x,z) = upper_bound (rng (min (h,g,x,z)));

existence for x, z being object st [x,z] in [:C1,C3:] holds

it . (x,z) = upper_bound (rng (min (h,g,x,z)));

ex b

for x, z being object st [x,z] in [:C1,C3:] holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def3 defines (#) FUZZY_4:def 3 :

for C1, C2, C3 being non empty set

for h being RMembership_Func of C1,C2

for g being RMembership_Func of C2,C3

for b_{6} being RMembership_Func of C1,C3 holds

( b_{6} = h (#) g iff for x, z being object st [x,z] in [:C1,C3:] holds

b_{6} . (x,z) = upper_bound (rng (min (h,g,x,z))) );

for C1, C2, C3 being non empty set

for h being RMembership_Func of C1,C2

for g being RMembership_Func of C2,C3

for b

( b

b

Lm1: for C1, C2, C3 being non empty set

for f being RMembership_Func of C1,C2

for g, h being RMembership_Func of C2,C3

for x, z being set st x in C1 & z in C3 holds

upper_bound (rng (min (f,(max (g,h)),x,z))) = max ((upper_bound (rng (min (f,g,x,z)))),(upper_bound (rng (min (f,h,x,z)))))

proof end;

theorem :: FUZZY_4:13

for C1, C2, C3 being non empty set

for f being RMembership_Func of C1,C2

for g, h being RMembership_Func of C2,C3 holds f (#) (max (g,h)) = max ((f (#) g),(f (#) h))

for f being RMembership_Func of C1,C2

for g, h being RMembership_Func of C2,C3 holds f (#) (max (g,h)) = max ((f (#) g),(f (#) h))

proof end;

Lm2: for C1, C2, C3 being non empty set

for f, g being RMembership_Func of C1,C2

for h being RMembership_Func of C2,C3

for x, z being set st x in C1 & z in C3 holds

upper_bound (rng (min ((max (f,g)),h,x,z))) = max ((upper_bound (rng (min (f,h,x,z)))),(upper_bound (rng (min (g,h,x,z)))))

proof end;

theorem :: FUZZY_4:14

for C1, C2, C3 being non empty set

for f, g being RMembership_Func of C1,C2

for h being RMembership_Func of C2,C3 holds (max (f,g)) (#) h = max ((f (#) h),(g (#) h))

for f, g being RMembership_Func of C1,C2

for h being RMembership_Func of C2,C3 holds (max (f,g)) (#) h = max ((f (#) h),(g (#) h))

proof end;

Lm3: for C1, C2, C3 being non empty set

for f being RMembership_Func of C1,C2

for g, h being RMembership_Func of C2,C3

for x, z being set st x in C1 & z in C3 holds

upper_bound (rng (min (f,(min (g,h)),x,z))) <= min ((upper_bound (rng (min (f,g,x,z)))),(upper_bound (rng (min (f,h,x,z)))))

proof end;

theorem :: FUZZY_4:15

for C1, C2, C3 being non empty set

for f being RMembership_Func of C1,C2

for g, h being RMembership_Func of C2,C3 holds min ((f (#) g),(f (#) h)) c=

for f being RMembership_Func of C1,C2

for g, h being RMembership_Func of C2,C3 holds min ((f (#) g),(f (#) h)) c=

proof end;

Lm4: for C1, C2, C3 being non empty set

for f, g being RMembership_Func of C1,C2

for h being RMembership_Func of C2,C3

for x, z being set st x in C1 & z in C3 holds

upper_bound (rng (min ((min (f,g)),h,x,z))) <= min ((upper_bound (rng (min (f,h,x,z)))),(upper_bound (rng (min (g,h,x,z)))))

proof end;

theorem :: FUZZY_4:16

for C1, C2, C3 being non empty set

for f, g being RMembership_Func of C1,C2

for h being RMembership_Func of C2,C3 holds min ((f (#) h),(g (#) h)) c=

for f, g being RMembership_Func of C1,C2

for h being RMembership_Func of C2,C3 holds min ((f (#) h),(g (#) h)) c=

proof end;

Lm5: for C1, C2, C3 being non empty set

for f being RMembership_Func of C1,C2

for g being RMembership_Func of C2,C3

for x, z being set st x in C1 & z in C3 holds

upper_bound (rng (min ((converse g),(converse f),z,x))) = upper_bound (rng (min (f,g,x,z)))

proof end;

theorem :: FUZZY_4:17

for C1, C2, C3 being non empty set

for f being RMembership_Func of C1,C2

for g being RMembership_Func of C2,C3 holds converse (f (#) g) = (converse g) (#) (converse f)

for f being RMembership_Func of C1,C2

for g being RMembership_Func of C2,C3 holds converse (f (#) g) = (converse g) (#) (converse f)

proof end;

theorem Th18: :: FUZZY_4:18

for C1, C2, C3 being non empty set

for f, g being RMembership_Func of C1,C2

for h, k being RMembership_Func of C2,C3

for x, z being set st x in C1 & z in C3 & ( for y being set st y in C2 holds

( f . [x,y] <= g . [x,y] & h . [y,z] <= k . [y,z] ) ) holds

(f (#) h) . [x,z] <= (g (#) k) . [x,z]

for f, g being RMembership_Func of C1,C2

for h, k being RMembership_Func of C2,C3

for x, z being set st x in C1 & z in C3 & ( for y being set st y in C2 holds

( f . [x,y] <= g . [x,y] & h . [y,z] <= k . [y,z] ) ) holds

(f (#) h) . [x,z] <= (g (#) k) . [x,z]

proof end;

theorem :: FUZZY_4:19

for C1, C2, C3 being non empty set

for f, g being RMembership_Func of C1,C2

for h, k being RMembership_Func of C2,C3 st g c= & k c= holds

g (#) k c=

for f, g being RMembership_Func of C1,C2

for h, k being RMembership_Func of C2,C3 st g c= & k c= holds

g (#) k c=

proof end;

Lm6: ( 1 in REAL & 0 in REAL )

by XREAL_0:def 1;

definition

let C1, C2 be non empty set ;

ex b_{1} being RMembership_Func of C1,C2 st

for x, y being object st [x,y] in [:C1,C2:] holds

( ( x = y implies b_{1} . (x,y) = 1 ) & ( x <> y implies b_{1} . (x,y) = 0 ) )

for b_{1}, b_{2} being RMembership_Func of C1,C2 st ( for x, y being object st [x,y] in [:C1,C2:] holds

( ( x = y implies b_{1} . (x,y) = 1 ) & ( x <> y implies b_{1} . (x,y) = 0 ) ) ) & ( for x, y being object st [x,y] in [:C1,C2:] holds

( ( x = y implies b_{2} . (x,y) = 1 ) & ( x <> y implies b_{2} . (x,y) = 0 ) ) ) holds

b_{1} = b_{2}

end;
func Imf (C1,C2) -> RMembership_Func of C1,C2 means :Def4: :: FUZZY_4:def 4

for x, y being object st [x,y] in [:C1,C2:] holds

( ( x = y implies it . (x,y) = 1 ) & ( x <> y implies it . (x,y) = 0 ) );

existence for x, y being object st [x,y] in [:C1,C2:] holds

( ( x = y implies it . (x,y) = 1 ) & ( x <> y implies it . (x,y) = 0 ) );

ex b

for x, y being object st [x,y] in [:C1,C2:] holds

( ( x = y implies b

proof end;

uniqueness for b

( ( x = y implies b

( ( x = y implies b

b

proof end;

:: deftheorem Def4 defines Imf FUZZY_4:def 4 :

for C1, C2 being non empty set

for b_{3} being RMembership_Func of C1,C2 holds

( b_{3} = Imf (C1,C2) iff for x, y being object st [x,y] in [:C1,C2:] holds

( ( x = y implies b_{3} . (x,y) = 1 ) & ( x <> y implies b_{3} . (x,y) = 0 ) ) );

for C1, C2 being non empty set

for b

( b

( ( x = y implies b

theorem :: FUZZY_4:20

theorem :: FUZZY_4:21

Lm7: for C1, C2, C3 being non empty set

for f being RMembership_Func of C2,C3

for x, z being set st x in C1 & z in C3 holds

upper_bound (rng (min ((Zmf (C1,C2)),f,x,z))) = (Zmf (C1,C3)) . [x,z]

proof end;

theorem Th22: :: FUZZY_4:22

for C1, C2, C3 being non empty set

for f being RMembership_Func of C2,C3 holds (Zmf (C1,C2)) (#) f = Zmf (C1,C3)

for f being RMembership_Func of C2,C3 holds (Zmf (C1,C2)) (#) f = Zmf (C1,C3)

proof end;

Lm8: for C1, C2, C3 being non empty set

for f being RMembership_Func of C1,C2

for x, z being set st x in C1 & z in C3 holds

upper_bound (rng (min (f,(Zmf (C2,C3)),x,z))) = (Zmf (C1,C3)) . [x,z]

proof end;

theorem Th23: :: FUZZY_4:23

for C1, C2, C3 being non empty set

for f being RMembership_Func of C1,C2 holds f (#) (Zmf (C2,C3)) = Zmf (C1,C3)

for f being RMembership_Func of C1,C2 holds f (#) (Zmf (C2,C3)) = Zmf (C1,C3)

proof end;

theorem :: FUZZY_4:24

for C1 being non empty set

for f being RMembership_Func of C1,C1 holds f (#) (Zmf (C1,C1)) = (Zmf (C1,C1)) (#) f

for f being RMembership_Func of C1,C1 holds f (#) (Zmf (C1,C1)) = (Zmf (C1,C1)) (#) f

proof end;

:: missing, 2006.12.03, AT

theorem :: FUZZY_4:25

for X, Y being non empty set

for x being Element of X

for y being Element of Y holds

( ( x = y implies (Imf (X,Y)) . (x,y) = 1 ) & ( x <> y implies (Imf (X,Y)) . (x,y) = 0 ) )

for x being Element of X

for y being Element of Y holds

( ( x = y implies (Imf (X,Y)) . (x,y) = 1 ) & ( x <> y implies (Imf (X,Y)) . (x,y) = 0 ) )

proof end;

theorem :: FUZZY_4:26