environ
vocabularies HIDDEN, NUMBERS, XBOOLE_0, FUZZY_1, RELAT_1, SUBSET_1, FUNCT_1, XXREAL_2, XXREAL_0, XXREAL_1, CARD_1, TARSKI, ARYTM_3, ARYTM_1, FUZZY_2, ZFMISC_1, PARTFUN1, VALUED_1, SEQ_4, FUZZY_4, MEASURE5, REAL_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, REAL_1, FUNCT_1, BINOP_1, RELAT_1, RELSET_1, PARTFUN1, XXREAL_2, FUNCT_4, INTEGRA1, RCOMP_1, MEASURE6, FUZZY_1, FUZZY_2, SEQ_4, MEASURE5;
definitions TARSKI, FUZZY_1, RELAT_1;
theorems FUZZY_1, FUNCT_3, PARTFUN1, FUNCT_1, INTEGRA1, INTEGRA2, ZFMISC_1, SEQ_4, SUBSET_1, XBOOLE_0, FUZZY_2, XXREAL_0, FUNCT_4, XXREAL_2, XREAL_1, RELSET_1, MEMBERED, FUNCT_2, RELAT_1, MEASURE5, XREAL_0, TARSKI;
schemes PARTFUN1, BINOP_1;
registrations XBOOLE_0, SUBSET_1, NUMBERS, XXREAL_0, XREAL_0, MEMBERED, INTEGRA1, RELAT_1, VALUED_0, RELSET_1, MEASURE5, BINOP_2, ORDINAL1;
constructors HIDDEN, FUNCT_4, REAL_1, SQUARE_1, RFUNCT_1, MEASURE6, INTEGRA1, FUZZY_2, XXREAL_2, SEQ_4, RELSET_1, RELAT_1, FUZZY_1, BINOP_2, RVSUM_1, BINOP_1, NUMBERS;
requirements HIDDEN, NUMERALS, REAL, SUBSET, BOOLE;
equalities TARSKI, FUZZY_1, FUZZY_2, BINOP_1, ORDINAL1;
expansions FUZZY_1, BINOP_1, RELAT_1;
reconsider jj = 1 as Real ;
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
;
existence
ex b1 being Membership_Func of C2 st
for y being Element of C2 holds b1 . y = min ((h . [x,y]),(g . [y,z]))
uniqueness
for b1, b2 being Membership_Func of C2 st ( for y being Element of C2 holds b1 . y = min ((h . [x,y]),(g . [y,z])) ) & ( for y being Element of C2 holds b2 . y = min ((h . [x,y]),(g . [y,z])) ) holds
b1 = b2
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 b8 being Membership_Func of C2 holds
( b8 = min (h,g,x,z) iff for y being Element of C2 holds b8 . y = min ((h . [x,y]),(g . [y,z])) );
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;
existence
ex b1 being RMembership_Func of C1,C3 st
for x, z being object st [x,z] in [:C1,C3:] holds
b1 . (x,z) = upper_bound (rng (min (h,g,x,z)))
uniqueness
for b1, b2 being RMembership_Func of C1,C3 st ( for x, z being object st [x,z] in [:C1,C3:] holds
b1 . (x,z) = upper_bound (rng (min (h,g,x,z))) ) & ( for x, z being object st [x,z] in [:C1,C3:] holds
b2 . (x,z) = upper_bound (rng (min (h,g,x,z))) ) holds
b1 = b2
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 b6 being RMembership_Func of C1,C3 holds
( b6 = h (#) g iff for x, z being object st [x,z] in [:C1,C3:] holds
b6 . (x,z) = upper_bound (rng (min (h,g,x,z))) );
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)))))
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)))))
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)))))
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)))))
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)))
theorem Th18:
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]
Lm6:
( 1 in REAL & 0 in REAL )
by XREAL_0:def 1;
definition
let C1,
C2 be non
empty set ;
existence
ex b1 being RMembership_Func of C1,C2 st
for x, y being object st [x,y] in [:C1,C2:] holds
( ( x = y implies b1 . (x,y) = 1 ) & ( x <> y implies b1 . (x,y) = 0 ) )
uniqueness
for b1, b2 being RMembership_Func of C1,C2 st ( for x, y being object st [x,y] in [:C1,C2:] holds
( ( x = y implies b1 . (x,y) = 1 ) & ( x <> y implies b1 . (x,y) = 0 ) ) ) & ( for x, y being object st [x,y] in [:C1,C2:] holds
( ( x = y implies b2 . (x,y) = 1 ) & ( x <> y implies b2 . (x,y) = 0 ) ) ) holds
b1 = b2
end;
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]
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]