environ
vocabularies HIDDEN, NUMBERS, XBOOLE_0, SUBSET_1, PARTFUN1, PROB_1, FUNCT_1, RAT_1, REAL_1, NAT_1, VALUED_0, RELAT_1, COMPLEX1, ARYTM_3, XXREAL_0, TARSKI, VALUED_1, ARYTM_1, MESFUNC1, SUPINF_2, RFUNCT_3, CARD_1, FUNCT_3, PROB_2, FINSEQ_1, FUNCOP_1, MEASURE1, SUPINF_1, ORDINAL4, MESFUNC2;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XXREAL_3, XCMPLX_0, XREAL_0, VALUED_0, REAL_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, NAT_1, WELLORD2, RAT_1, FINSEQ_1, PROB_1, XXREAL_0, SUPINF_1, FUNCOP_1, SUPINF_2, FUNCT_3, PROB_2, MEASURE1, MEASURE2, MEASURE3, MEASURE6, EXTREAL1, MESFUNC1;
definitions TARSKI, XBOOLE_0, VALUED_0;
theorems MEASURE1, TARSKI, SUBSET_1, PARTFUN1, FUNCT_1, FUNCT_2, NAT_1, SUPINF_2, WELLORD2, RAT_1, RELSET_1, EXTREAL1, MESFUNC1, ZFMISC_1, FINSEQ_1, FINSEQ_3, FINSEQ_5, XREAL_0, PROB_2, FUNCT_3, XBOOLE_0, XBOOLE_1, RELAT_1, FUNCOP_1, XREAL_1, FINSUB_1, PROB_1, XXREAL_0, ORDINAL1, XXREAL_3;
schemes FUNCT_2, SEQ_1, NAT_1;
registrations ORDINAL1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0, RAT_1, MEMBERED, FINSEQ_1, MEASURE1, VALUED_0, FUNCT_2, CARD_1, XXREAL_3;
constructors HIDDEN, PARTFUN1, WELLORD2, FUNCT_3, FUNCOP_1, REAL_1, NAT_1, RAT_1, FINSEQ_1, PROB_2, MEASURE3, MEASURE6, EXTREAL1, MESFUNC1, SUPINF_1, RELSET_1, BINOP_2, NUMBERS;
requirements HIDDEN, NUMERALS, REAL, BOOLE, SUBSET;
equalities XBOOLE_0, XXREAL_3, MESFUNC1, ORDINAL1, SUPINF_2;
expansions TARSKI, XBOOLE_0, VALUED_0, MESFUNC1;
reconsider jj = 1 as Element of REAL by XREAL_0:def 1;
definition
let C be non
empty set ;
let f be
PartFunc of
C,
ExtREAL;
deffunc H1(
Element of
C)
-> Element of
ExtREAL =
max (
(f . $1),
0.);
existence
ex b1 being PartFunc of C,ExtREAL st
( dom b1 = dom f & ( for x being Element of C st x in dom b1 holds
b1 . x = max ((f . x),0.) ) )
uniqueness
for b1, b2 being PartFunc of C,ExtREAL st dom b1 = dom f & ( for x being Element of C st x in dom b1 holds
b1 . x = max ((f . x),0.) ) & dom b2 = dom f & ( for x being Element of C st x in dom b2 holds
b2 . x = max ((f . x),0.) ) holds
b1 = b2
deffunc H2(
Element of
C)
-> Element of
ExtREAL =
max (
(- (f . $1)),
0.);
existence
ex b1 being PartFunc of C,ExtREAL st
( dom b1 = dom f & ( for x being Element of C st x in dom b1 holds
b1 . x = max ((- (f . x)),0.) ) )
uniqueness
for b1, b2 being PartFunc of C,ExtREAL st dom b1 = dom f & ( for x being Element of C st x in dom b1 holds
b1 . x = max ((- (f . x)),0.) ) & dom b2 = dom f & ( for x being Element of C st x in dom b2 holds
b2 . x = max ((- (f . x)),0.) ) holds
b1 = b2
end;