environ
vocabularies HIDDEN, NUMBERS, XBOOLE_0, SUBSET_1, FUZZY_1, CARD_1, XXREAL_0, FUNCT_1, TARSKI, ARYTM_1, RELAT_1, PARTFUN1, XXREAL_1, SEQ_4, MEMBER_1, ARYTM_3, REAL_1, FUNCT_2, ZFMISC_1, FUNCT_3, FUZZY_2, MEASURE5;
notations HIDDEN, TARSKI, XBOOLE_0, ORDINAL1, SUBSET_1, ZFMISC_1, NUMBERS, XXREAL_0, XCMPLX_0, XREAL_0, REAL_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FUNCT_3, INTEGRA1, RCOMP_1, SEQ_4, FUZZY_1, MEASURE5;
definitions FUZZY_1;
theorems TARSKI, FUNCT_1, PARTFUN1, INTEGRA1, INTEGRA2, FUZZY_1, XBOOLE_0, XREAL_1, XXREAL_0, FUNCT_3, FUNCT_2, RELAT_1, MEASURE5, XREAL_0;
schemes PARTFUN1;
registrations RELSET_1, NUMBERS, MEMBERED, XBOOLE_0, SUBSET_1, VALUED_0, MEASURE5, XREAL_0;
constructors HIDDEN, REAL_1, SQUARE_1, RFUNCT_1, INTEGRA1, FUZZY_1, SEQ_4, RELSET_1;
requirements HIDDEN, NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
equalities FUZZY_1, ORDINAL1;
expansions FUZZY_1;
reconsider jj = 1 as Real ;
Lm1:
for a, b, c being Real st 0 <= c holds
c * (min (a,b)) = min ((c * a),(c * b))
Lm2:
for a, b, c being Real st 0 <= c holds
c * (max (a,b)) = max ((c * a),(c * b))
theorem
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) )