let C be non empty set ; :: thesis: for X being set
for f being PartFunc of C,REAL st f | X is bounded_above holds
(max+ f) | X is bounded_above
let X be set ; :: thesis: for f being PartFunc of C,REAL st f | X is bounded_above holds
(max+ f) | X is bounded_above
let f be PartFunc of C,REAL; :: thesis: ( f | X is bounded_above implies (max+ f) | X is bounded_above )
assume f | X is bounded_above ; :: thesis: (max+ f) | X is bounded_above
then consider b being Real such that
A1: for c being object st c in X /\ (dom f) holds
f . c <= b by RFUNCT_1:70;
A2: dom (max+ f) = dom f by RFUNCT_3:def 10;
ex r being Real st
for c being object st c in X /\ (dom (max+ f)) holds
(max+ f) . c <= r
proof
now :: thesis: ex r being Real st
for c being object st c in X /\ (dom (max+ f)) holds
(max+ f) . c <= r
per cases ( b < 0 or b >= 0 ) ;
suppose A3: b < 0 ; :: thesis: ex r being Real st
for c being object st c in X /\ (dom (max+ f)) holds
(max+ f) . c <= r
for c being object st c in X /\ (dom (max+ f)) holds
(max+ f) . c <= 0
proof
let c be object ; :: thesis: ( c in X /\ (dom (max+ f)) implies (max+ f) . c <= 0 )
assume c in X /\ (dom (max+ f)) ; :: thesis: (max+ f) . c <= 0
then A4: c in X /\ (dom f) by RFUNCT_3:def 10;
then f . c <= b by A1;
then max ((f . c),0) = 0 by A3, XXREAL_0:def 10;
then A5: max+ (f . c) = 0 by RFUNCT_3:def 1;
c in dom f by A4, XBOOLE_0:def 4;
hence (max+ f) . c <= 0 by A2, A5, RFUNCT_3:def 10; :: thesis: verum
end;
hence ex r being Real st
for c being object st c in X /\ (dom (max+ f)) holds
(max+ f) . c <= r ; :: thesis: verum
end;
suppose A6: b >= 0 ; :: thesis: ex r being Real st
for c being object st c in X /\ (dom (max+ f)) holds
(max+ f) . c <= r
for c being object st c in X /\ (dom (max+ f)) holds
(max+ f) . c <= b
proof
let c be object ; :: thesis: ( c in X /\ (dom (max+ f)) implies (max+ f) . c <= b )
assume c in X /\ (dom (max+ f)) ; :: thesis: (max+ f) . c <= b
then A7: c in X /\ (dom f) by RFUNCT_3:def 10;
then f . c <= b by A1;
then max ((f . c),0) <= b by A6, XXREAL_0:28;
then A8: max+ (f . c) <= b by RFUNCT_3:def 1;
c in dom f by A7, XBOOLE_0:def 4;
hence (max+ f) . c <= b by A2, A8, RFUNCT_3:def 10; :: thesis: verum
end;
then consider r being Real such that
r = b and
A9: for c being object st c in X /\ (dom (max+ f)) holds
(max+ f) . c <= r ;
thus ex r being Real st
for c being object st c in X /\ (dom (max+ f)) holds
(max+ f) . c <= r by A9; :: thesis: verum
end;
end;
end;
hence ex r being Real st
for c being object st c in X /\ (dom (max+ f)) holds
(max+ f) . c <= r ; :: thesis: verum
end;
hence (max+ f) | X is bounded_above by RFUNCT_1:70; :: thesis: verum