begin
:: deftheorem Def1 defines real-valued MESFUNC2:def 1 :
theorem
theorem Th2:
theorem Th3:
begin
theorem
theorem Th5:
theorem Th6:
theorem Th7:
theorem
canceled;
theorem Th9:
theorem
canceled;
theorem Th11:
theorem Th12:
theorem
begin
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. ;
func max+ f -> PartFunc of
C,
ExtREAL means :
Def2:
(
dom it = dom f & ( for
x being
Element of
C st
x in dom it holds
it . x = max (f . x),
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. ;
func max- f -> PartFunc of
C,
ExtREAL means :
Def3:
(
dom it = dom f & ( for
x being
Element of
C st
x in dom it holds
it . x = max (- (f . x)),
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;
:: deftheorem Def2 defines max+ MESFUNC2:def 2 :
:: deftheorem Def3 defines max- MESFUNC2:def 3 :
theorem Th14:
theorem Th15:
theorem
theorem Th17:
theorem
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
theorem
theorem
theorem
theorem
begin
theorem
theorem
theorem
begin
theorem
canceled;
theorem
theorem
begin
theorem Th33:
theorem
:: deftheorem MESFUNC2:def 4 :
canceled;
:: deftheorem Def5 defines is_simple_func_in MESFUNC2:def 5 :
theorem
theorem
theorem