let A be non empty closed_interval Subset of REAL; :: thesis: for f being PartFunc of REAL,REAL st f | A is non-decreasing & A c= dom f holds
( lower_bound (rng (f | A)) = f . (lower_bound A) & upper_bound (rng (f | A)) = f . (upper_bound A) )
let f be PartFunc of REAL,REAL; :: thesis: ( f | A is non-decreasing & A c= dom f implies ( lower_bound (rng (f | A)) = f . (lower_bound A) & upper_bound (rng (f | A)) = f . (upper_bound A) ) )
assume that
A1: f | A is non-decreasing and
A2: A c= dom f ; :: thesis: ( lower_bound (rng (f | A)) = f . (lower_bound A) & upper_bound (rng (f | A)) = f . (upper_bound A) )
A3: dom (f | A) = (dom f) /\ A by RELAT_1:61
.= A by A2, XBOOLE_1:28 ;
then A4: rng (f | A) <> {} by RELAT_1:42;
A5: lower_bound A <= upper_bound A by SEQ_4:11;
then A6: upper_bound A in dom (f | A) by A3, INTEGRA2:1;
then A7: upper_bound A in (dom f) /\ A by RELAT_1:61;
A8: for x being Real st x in rng (f | A) holds
x <= f . (upper_bound A)
proof
let y be Real; :: thesis: ( y in rng (f | A) implies y <= f . (upper_bound A) )
assume y in rng (f | A) ; :: thesis: y <= f . (upper_bound A)
then consider x being Element of REAL such that
A9: x in dom (f | A) and
A10: y = (f | A) . x by PARTFUN1:3;
( x in (dom f) /\ A & upper_bound A >= x ) by A9, INTEGRA2:1, RELAT_1:61;
then f . (upper_bound A) >= f . x by A1, A7, RFUNCT_2:24;
hence y <= f . (upper_bound A) by A9, A10, FUNCT_1:47; :: thesis: verum
end;
A11: lower_bound A in dom (f | A) by A3, A5, INTEGRA2:1;
then A12: lower_bound A in (dom f) /\ A by RELAT_1:61;
A13: for y being Real st y in rng (f | A) holds
y >= f . (lower_bound A)
proof
let y be Real; :: thesis: ( y in rng (f | A) implies y >= f . (lower_bound A) )
assume y in rng (f | A) ; :: thesis: y >= f . (lower_bound A)
then consider x being Element of REAL such that
A14: x in dom (f | A) and
A15: y = (f | A) . x by PARTFUN1:3;
( x in (dom f) /\ A & lower_bound A <= x ) by A14, INTEGRA2:1, RELAT_1:61;
then f . (lower_bound A) <= f . x by A1, A12, RFUNCT_2:24;
hence y >= f . (lower_bound A) by A14, A15, FUNCT_1:47; :: thesis: verum
end;
for a being Real st ( for x being Real st x in rng (f | A) holds
x >= a ) holds
f . (lower_bound A) >= a
proof
let a be Real; :: thesis: ( ( for x being Real st x in rng (f | A) holds
x >= a ) implies f . (lower_bound A) >= a )
assume A16: for x being Real st x in rng (f | A) holds
x >= a ; :: thesis: f . (lower_bound A) >= a
( f . (lower_bound A) = (f | A) . (lower_bound A) & (f | A) . (lower_bound A) in rng (f | A) ) by A11, FUNCT_1:47, FUNCT_1:def 3;
hence f . (lower_bound A) >= a by A16; :: thesis: verum
end;
hence lower_bound (rng (f | A)) = f . (lower_bound A) by A4, A13, SEQ_4:44; :: thesis: upper_bound (rng (f | A)) = f . (upper_bound A)
for a being Real st ( for x being Real st x in rng (f | A) holds
x <= a ) holds
f . (upper_bound A) <= a
proof
let a be Real; :: thesis: ( ( for x being Real st x in rng (f | A) holds
x <= a ) implies f . (upper_bound A) <= a )
assume A17: for x being Real st x in rng (f | A) holds
x <= a ; :: thesis: f . (upper_bound A) <= a
( f . (upper_bound A) = (f | A) . (upper_bound A) & (f | A) . (upper_bound A) in rng (f | A) ) by A6, FUNCT_1:47, FUNCT_1:def 3;
hence f . (upper_bound A) <= a by A17; :: thesis: verum
end;
hence upper_bound (rng (f | A)) = f . (upper_bound A) by A4, A8, SEQ_4:46; :: thesis: verum