let a be Real; :: thesis: for A being non empty closed_interval Subset of REAL
for f, g being Function of A,REAL st f | A is bounded & a >= 0 & ( for x, y being Real st x in A & y in A holds
|.((g . x) - (g . y)).| <= a * |.((f . x) - (f . y)).| ) holds
(upper_bound (rng g)) - (lower_bound (rng g)) <= a * ((upper_bound (rng f)) - (lower_bound (rng f)))
let A be non empty closed_interval Subset of REAL; :: thesis: for f, g being Function of A,REAL st f | A is bounded & a >= 0 & ( for x, y being Real st x in A & y in A holds
|.((g . x) - (g . y)).| <= a * |.((f . x) - (f . y)).| ) holds
(upper_bound (rng g)) - (lower_bound (rng g)) <= a * ((upper_bound (rng f)) - (lower_bound (rng f)))
let f, g be Function of A,REAL; :: thesis: ( f | A is bounded & a >= 0 & ( for x, y being Real st x in A & y in A holds
|.((g . x) - (g . y)).| <= a * |.((f . x) - (f . y)).| ) implies (upper_bound (rng g)) - (lower_bound (rng g)) <= a * ((upper_bound (rng f)) - (lower_bound (rng f))) )
assume that
A1: f | A is bounded and
A2: a >= 0 and
A3: for x, y being Real st x in A & y in A holds
|.((g . x) - (g . y)).| <= a * |.((f . x) - (f . y)).| ; :: thesis: (upper_bound (rng g)) - (lower_bound (rng g)) <= a * ((upper_bound (rng f)) - (lower_bound (rng f)))
A4: rng f is bounded_above by A1, INTEGRA1:13;
A5: dom f = A by FUNCT_2:def 1;
A6: rng f is bounded_below by A1, INTEGRA1:11;
A7: for x, y being Real st x in A & y in A holds
|.((f . x) - (f . y)).| <= (upper_bound (rng f)) - (lower_bound (rng f))
proof
let x, y be Real; :: thesis: ( x in A & y in A implies |.((f . x) - (f . y)).| <= (upper_bound (rng f)) - (lower_bound (rng f)) )
assume that
A8: x in A and
A9: y in A ; :: thesis: |.((f . x) - (f . y)).| <= (upper_bound (rng f)) - (lower_bound (rng f))
now :: thesis: |.((f . x) - (f . y)).| <= (upper_bound (rng f)) - (lower_bound (rng f))
per cases ( f . x >= f . y or f . x < f . y ) ;
suppose f . x >= f . y ; :: thesis: |.((f . x) - (f . y)).| <= (upper_bound (rng f)) - (lower_bound (rng f))
then (f . x) - (f . y) >= 0 by XREAL_1:48;
then |.((f . x) - (f . y)).| = (f . x) - (f . y) by ABSVALUE:def 1;
then A10: |.((f . x) - (f . y)).| + (f . y) = f . x ;
f . y in rng f by A5, A9, FUNCT_1:def 3;
then A11: lower_bound (rng f) <= f . y by A6, SEQ_4:def 2;
f . x in rng f by A5, A8, FUNCT_1:def 3;
then f . x <= upper_bound (rng f) by A4, SEQ_4:def 1;
then f . y <= (upper_bound (rng f)) - |.((f . x) - (f . y)).| by A10, XREAL_1:19;
then lower_bound (rng f) <= (upper_bound (rng f)) - |.((f . x) - (f . y)).| by A11, XXREAL_0:2;
then (lower_bound (rng f)) + |.((f . x) - (f . y)).| <= upper_bound (rng f) by XREAL_1:19;
hence |.((f . x) - (f . y)).| <= (upper_bound (rng f)) - (lower_bound (rng f)) by XREAL_1:19; :: thesis: verum
end;
suppose f . x < f . y ; :: thesis: |.((f . x) - (f . y)).| <= (upper_bound (rng f)) - (lower_bound (rng f))
then (f . x) - (f . y) < 0 by XREAL_1:49;
then |.((f . x) - (f . y)).| = - ((f . x) - (f . y)) by ABSVALUE:def 1
.= (f . y) - (f . x) ;
then A12: |.((f . x) - (f . y)).| + (f . x) = f . y ;
f . x in rng f by A5, A8, FUNCT_1:def 3;
then A13: lower_bound (rng f) <= f . x by A6, SEQ_4:def 2;
f . y in rng f by A5, A9, FUNCT_1:def 3;
then f . y <= upper_bound (rng f) by A4, SEQ_4:def 1;
then f . x <= (upper_bound (rng f)) - |.((f . x) - (f . y)).| by A12, XREAL_1:19;
then lower_bound (rng f) <= (upper_bound (rng f)) - |.((f . x) - (f . y)).| by A13, XXREAL_0:2;
then (lower_bound (rng f)) + |.((f . x) - (f . y)).| <= upper_bound (rng f) by XREAL_1:19;
hence |.((f . x) - (f . y)).| <= (upper_bound (rng f)) - (lower_bound (rng f)) by XREAL_1:19; :: thesis: verum
end;
end;
end;
hence |.((f . x) - (f . y)).| <= (upper_bound (rng f)) - (lower_bound (rng f)) ; :: thesis: verum
end;
for x, y being Real st x in A & y in A holds
|.((g . x) - (g . y)).| <= a * ((upper_bound (rng f)) - (lower_bound (rng f)))
proof
let x, y be Real; :: thesis: ( x in A & y in A implies |.((g . x) - (g . y)).| <= a * ((upper_bound (rng f)) - (lower_bound (rng f))) )
assume that
A14: x in A and
A15: y in A ; :: thesis: |.((g . x) - (g . y)).| <= a * ((upper_bound (rng f)) - (lower_bound (rng f)))
A16: |.((g . x) - (g . y)).| <= a * |.((f . x) - (f . y)).| by A3, A14, A15;
a * |.((f . x) - (f . y)).| <= a * ((upper_bound (rng f)) - (lower_bound (rng f))) by A2, A7, A14, A15, XREAL_1:64;
hence |.((g . x) - (g . y)).| <= a * ((upper_bound (rng f)) - (lower_bound (rng f))) by A16, XXREAL_0:2; :: thesis: verum
end;
hence (upper_bound (rng g)) - (lower_bound (rng g)) <= a * ((upper_bound (rng f)) - (lower_bound (rng f))) by Th24; :: thesis: verum