:: FCONT_2 semantic presentation
begin
definition
let f be PartFunc of REAL,REAL;
attrf is uniformly_continuous means :Def1: :: FCONT_2:def 1
for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1, x2 being Real st x1 in dom f & x2 in dom f & abs (x1 - x2) < s holds
abs ((f . x1) - (f . x2)) < r ) );
end;
:: deftheorem Def1 defines uniformly_continuous FCONT_2:def_1_:_
for f being PartFunc of REAL,REAL holds
( f is uniformly_continuous iff for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1, x2 being Real st x1 in dom f & x2 in dom f & abs (x1 - x2) < s holds
abs ((f . x1) - (f . x2)) < r ) ) );
theorem Th1: :: FCONT_2:1
for X being set
for f being PartFunc of REAL,REAL holds
( f | X is uniformly_continuous iff for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) & abs (x1 - x2) < s holds
abs ((f . x1) - (f . x2)) < r ) ) )
proof
let X be set ; ::_thesis: for f being PartFunc of REAL,REAL holds
( f | X is uniformly_continuous iff for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) & abs (x1 - x2) < s holds
abs ((f . x1) - (f . x2)) < r ) ) )
let f be PartFunc of REAL,REAL; ::_thesis: ( f | X is uniformly_continuous iff for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) & abs (x1 - x2) < s holds
abs ((f . x1) - (f . x2)) < r ) ) )
thus ( f | X is uniformly_continuous implies for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) & abs (x1 - x2) < s holds
abs ((f . x1) - (f . x2)) < r ) ) ) ::_thesis: ( ( for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) & abs (x1 - x2) < s holds
abs ((f . x1) - (f . x2)) < r ) ) ) implies f | X is uniformly_continuous )
proof
assume A1: f | X is uniformly_continuous ; ::_thesis: for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) & abs (x1 - x2) < s holds
abs ((f . x1) - (f . x2)) < r ) )
let r be Real; ::_thesis: ( 0 < r implies ex s being Real st
( 0 < s & ( for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) & abs (x1 - x2) < s holds
abs ((f . x1) - (f . x2)) < r ) ) )
assume 0 < r ; ::_thesis: ex s being Real st
( 0 < s & ( for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) & abs (x1 - x2) < s holds
abs ((f . x1) - (f . x2)) < r ) )
then consider s being Real such that
A2: 0 < s and
A3: for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) & abs (x1 - x2) < s holds
abs (((f | X) . x1) - ((f | X) . x2)) < r by A1, Def1;
take s ; ::_thesis: ( 0 < s & ( for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) & abs (x1 - x2) < s holds
abs ((f . x1) - (f . x2)) < r ) )
thus 0 < s by A2; ::_thesis: for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) & abs (x1 - x2) < s holds
abs ((f . x1) - (f . x2)) < r
let x1, x2 be Real; ::_thesis: ( x1 in dom (f | X) & x2 in dom (f | X) & abs (x1 - x2) < s implies abs ((f . x1) - (f . x2)) < r )
assume that
A4: x1 in dom (f | X) and
A5: x2 in dom (f | X) ; ::_thesis: ( not abs (x1 - x2) < s or abs ((f . x1) - (f . x2)) < r )
A6: (f | X) . x2 = f . x2 by A5, FUNCT_1:47;
(f | X) . x1 = f . x1 by A4, FUNCT_1:47;
hence ( not abs (x1 - x2) < s or abs ((f . x1) - (f . x2)) < r ) by A3, A4, A5, A6; ::_thesis: verum
end;
assume A7: for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) & abs (x1 - x2) < s holds
abs ((f . x1) - (f . x2)) < r ) ) ; ::_thesis: f | X is uniformly_continuous
let r be Real; :: according to FCONT_2:def_1 ::_thesis: ( 0 < r implies ex s being Real st
( 0 < s & ( for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) & abs (x1 - x2) < s holds
abs (((f | X) . x1) - ((f | X) . x2)) < r ) ) )
assume 0 < r ; ::_thesis: ex s being Real st
( 0 < s & ( for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) & abs (x1 - x2) < s holds
abs (((f | X) . x1) - ((f | X) . x2)) < r ) )
then consider s being Real such that
A8: 0 < s and
A9: for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) & abs (x1 - x2) < s holds
abs ((f . x1) - (f . x2)) < r by A7;
take s ; ::_thesis: ( 0 < s & ( for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) & abs (x1 - x2) < s holds
abs (((f | X) . x1) - ((f | X) . x2)) < r ) )
thus 0 < s by A8; ::_thesis: for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) & abs (x1 - x2) < s holds
abs (((f | X) . x1) - ((f | X) . x2)) < r
let x1, x2 be Real; ::_thesis: ( x1 in dom (f | X) & x2 in dom (f | X) & abs (x1 - x2) < s implies abs (((f | X) . x1) - ((f | X) . x2)) < r )
assume that
A10: x1 in dom (f | X) and
A11: x2 in dom (f | X) ; ::_thesis: ( not abs (x1 - x2) < s or abs (((f | X) . x1) - ((f | X) . x2)) < r )
A12: (f | X) . x2 = f . x2 by A11, FUNCT_1:47;
(f | X) . x1 = f . x1 by A10, FUNCT_1:47;
hence ( not abs (x1 - x2) < s or abs (((f | X) . x1) - ((f | X) . x2)) < r ) by A9, A10, A11, A12; ::_thesis: verum
end;
theorem Th2: :: FCONT_2:2
for X, X1 being set
for f being PartFunc of REAL,REAL st f | X is uniformly_continuous & X1 c= X holds
f | X1 is uniformly_continuous
proof
let X, X1 be set ; ::_thesis: for f being PartFunc of REAL,REAL st f | X is uniformly_continuous & X1 c= X holds
f | X1 is uniformly_continuous
let f be PartFunc of REAL,REAL; ::_thesis: ( f | X is uniformly_continuous & X1 c= X implies f | X1 is uniformly_continuous )
assume that
A1: f | X is uniformly_continuous and
A2: X1 c= X ; ::_thesis: f | X1 is uniformly_continuous
now__::_thesis:_for_r_being_Real_st_0_<_r_holds_
ex_s_being_Real_st_
(_0_<_s_&_(_for_x1,_x2_being_Real_st_x1_in_dom_(f_|_X1)_&_x2_in_dom_(f_|_X1)_&_abs_(x1_-_x2)_<_s_holds_
abs_((f_._x1)_-_(f_._x2))_<_r_)_)
let r be Real; ::_thesis: ( 0 < r implies ex s being Real st
( 0 < s & ( for x1, x2 being Real st x1 in dom (f | X1) & x2 in dom (f | X1) & abs (x1 - x2) < s holds
abs ((f . x1) - (f . x2)) < r ) ) )
assume 0 < r ; ::_thesis: ex s being Real st
( 0 < s & ( for x1, x2 being Real st x1 in dom (f | X1) & x2 in dom (f | X1) & abs (x1 - x2) < s holds
abs ((f . x1) - (f . x2)) < r ) )
then consider s being Real such that
A3: 0 < s and
A4: for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) & abs (x1 - x2) < s holds
abs ((f . x1) - (f . x2)) < r by A1, Th1;
take s = s; ::_thesis: ( 0 < s & ( for x1, x2 being Real st x1 in dom (f | X1) & x2 in dom (f | X1) & abs (x1 - x2) < s holds
abs ((f . x1) - (f . x2)) < r ) )
thus 0 < s by A3; ::_thesis: for x1, x2 being Real st x1 in dom (f | X1) & x2 in dom (f | X1) & abs (x1 - x2) < s holds
abs ((f . x1) - (f . x2)) < r
let x1, x2 be Real; ::_thesis: ( x1 in dom (f | X1) & x2 in dom (f | X1) & abs (x1 - x2) < s implies abs ((f . x1) - (f . x2)) < r )
assume that
A5: x1 in dom (f | X1) and
A6: x2 in dom (f | X1) and
A7: abs (x1 - x2) < s ; ::_thesis: abs ((f . x1) - (f . x2)) < r
f | X1 c= f | X by A2, RELAT_1:75;
then dom (f | X1) c= dom (f | X) by RELAT_1:11;
hence abs ((f . x1) - (f . x2)) < r by A4, A5, A6, A7; ::_thesis: verum
end;
hence f | X1 is uniformly_continuous by Th1; ::_thesis: verum
end;
theorem :: FCONT_2:3
for X, X1 being set
for f1, f2 being PartFunc of REAL,REAL st X c= dom f1 & X1 c= dom f2 & f1 | X is uniformly_continuous & f2 | X1 is uniformly_continuous holds
(f1 + f2) | (X /\ X1) is uniformly_continuous
proof
let X, X1 be set ; ::_thesis: for f1, f2 being PartFunc of REAL,REAL st X c= dom f1 & X1 c= dom f2 & f1 | X is uniformly_continuous & f2 | X1 is uniformly_continuous holds
(f1 + f2) | (X /\ X1) is uniformly_continuous
let f1, f2 be PartFunc of REAL,REAL; ::_thesis: ( X c= dom f1 & X1 c= dom f2 & f1 | X is uniformly_continuous & f2 | X1 is uniformly_continuous implies (f1 + f2) | (X /\ X1) is uniformly_continuous )
assume that
A1: X c= dom f1 and
A2: X1 c= dom f2 ; ::_thesis: ( not f1 | X is uniformly_continuous or not f2 | X1 is uniformly_continuous or (f1 + f2) | (X /\ X1) is uniformly_continuous )
A3: X /\ X1 c= dom f2 by A2, XBOOLE_1:108;
X /\ X1 c= dom f1 by A1, XBOOLE_1:108;
then X /\ X1 c= (dom f1) /\ (dom f2) by A3, XBOOLE_1:19;
then A4: X /\ X1 c= dom (f1 + f2) by VALUED_1:def_1;
assume that
A5: f1 | X is uniformly_continuous and
A6: f2 | X1 is uniformly_continuous ; ::_thesis: (f1 + f2) | (X /\ X1) is uniformly_continuous
A7: f2 | (X /\ X1) is uniformly_continuous by A6, Th2, XBOOLE_1:17;
A8: f1 | (X /\ X1) is uniformly_continuous by A5, Th2, XBOOLE_1:17;
now__::_thesis:_for_r_being_Real_st_0_<_r_holds_
ex_p_being_Element_of_REAL_st_
(_0_<_p_&_(_for_x1,_x2_being_Real_st_x1_in_dom_((f1_+_f2)_|_(X_/\_X1))_&_x2_in_dom_((f1_+_f2)_|_(X_/\_X1))_&_abs_(x1_-_x2)_<_p_holds_
abs_(((f1_+_f2)_._x1)_-_((f1_+_f2)_._x2))_<_r_)_)
let r be Real; ::_thesis: ( 0 < r implies ex p being Element of REAL st
( 0 < p & ( for x1, x2 being Real st x1 in dom ((f1 + f2) | (X /\ X1)) & x2 in dom ((f1 + f2) | (X /\ X1)) & abs (x1 - x2) < p holds
abs (((f1 + f2) . x1) - ((f1 + f2) . x2)) < r ) ) )
A9: dom (f1 + f2) = (dom f1) /\ (dom f2) by VALUED_1:def_1;
assume 0 < r ; ::_thesis: ex p being Element of REAL st
( 0 < p & ( for x1, x2 being Real st x1 in dom ((f1 + f2) | (X /\ X1)) & x2 in dom ((f1 + f2) | (X /\ X1)) & abs (x1 - x2) < p holds
abs (((f1 + f2) . x1) - ((f1 + f2) . x2)) < r ) )
then A10: 0 < r / 2 by XREAL_1:215;
then consider s being Real such that
A11: 0 < s and
A12: for x1, x2 being Real st x1 in dom (f1 | (X /\ X1)) & x2 in dom (f1 | (X /\ X1)) & abs (x1 - x2) < s holds
abs ((f1 . x1) - (f1 . x2)) < r / 2 by A8, Th1;
consider g being Real such that
A13: 0 < g and
A14: for x1, x2 being Real st x1 in dom (f2 | (X /\ X1)) & x2 in dom (f2 | (X /\ X1)) & abs (x1 - x2) < g holds
abs ((f2 . x1) - (f2 . x2)) < r / 2 by A7, A10, Th1;
take p = min (s,g); ::_thesis: ( 0 < p & ( for x1, x2 being Real st x1 in dom ((f1 + f2) | (X /\ X1)) & x2 in dom ((f1 + f2) | (X /\ X1)) & abs (x1 - x2) < p holds
abs (((f1 + f2) . x1) - ((f1 + f2) . x2)) < r ) )
thus 0 < p by A11, A13, XXREAL_0:15; ::_thesis: for x1, x2 being Real st x1 in dom ((f1 + f2) | (X /\ X1)) & x2 in dom ((f1 + f2) | (X /\ X1)) & abs (x1 - x2) < p holds
abs (((f1 + f2) . x1) - ((f1 + f2) . x2)) < r
let x1, x2 be Real; ::_thesis: ( x1 in dom ((f1 + f2) | (X /\ X1)) & x2 in dom ((f1 + f2) | (X /\ X1)) & abs (x1 - x2) < p implies abs (((f1 + f2) . x1) - ((f1 + f2) . x2)) < r )
assume that
A15: x1 in dom ((f1 + f2) | (X /\ X1)) and
A16: x2 in dom ((f1 + f2) | (X /\ X1)) and
A17: abs (x1 - x2) < p ; ::_thesis: abs (((f1 + f2) . x1) - ((f1 + f2) . x2)) < r
A18: x2 in X /\ X1 by A16, RELAT_1:57;
A19: x2 in dom (f1 + f2) by A16, RELAT_1:57;
then x2 in dom f2 by A9, XBOOLE_0:def_4;
then A20: x2 in dom (f2 | (X /\ X1)) by A18, RELAT_1:57;
p <= g by XXREAL_0:17;
then A21: abs (x1 - x2) < g by A17, XXREAL_0:2;
A22: x1 in X /\ X1 by A15, RELAT_1:57;
x2 in dom f1 by A9, A19, XBOOLE_0:def_4;
then A23: x2 in dom (f1 | (X /\ X1)) by A18, RELAT_1:57;
p <= s by XXREAL_0:17;
then A24: abs (x1 - x2) < s by A17, XXREAL_0:2;
A25: x1 in dom (f1 + f2) by A15, RELAT_1:57;
then x1 in dom f2 by A9, XBOOLE_0:def_4;
then x1 in dom (f2 | (X /\ X1)) by A22, RELAT_1:57;
then A26: abs ((f2 . x1) - (f2 . x2)) < r / 2 by A14, A21, A20;
x1 in dom f1 by A9, A25, XBOOLE_0:def_4;
then x1 in dom (f1 | (X /\ X1)) by A22, RELAT_1:57;
then abs ((f1 . x1) - (f1 . x2)) < r / 2 by A12, A24, A23;
then A27: (abs ((f1 . x1) - (f1 . x2))) + (abs ((f2 . x1) - (f2 . x2))) < (r / 2) + (r / 2) by A26, XREAL_1:8;
A28: abs (((f1 . x1) - (f1 . x2)) + ((f2 . x1) - (f2 . x2))) <= (abs ((f1 . x1) - (f1 . x2))) + (abs ((f2 . x1) - (f2 . x2))) by COMPLEX1:56;
abs (((f1 + f2) . x1) - ((f1 + f2) . x2)) = abs (((f1 . x1) + (f2 . x1)) - ((f1 + f2) . x2)) by A4, A22, VALUED_1:def_1
.= abs (((f1 . x1) + (f2 . x1)) - ((f1 . x2) + (f2 . x2))) by A4, A18, VALUED_1:def_1
.= abs (((f1 . x1) - (f1 . x2)) + ((f2 . x1) - (f2 . x2))) ;
hence abs (((f1 + f2) . x1) - ((f1 + f2) . x2)) < r by A27, A28, XXREAL_0:2; ::_thesis: verum
end;
hence (f1 + f2) | (X /\ X1) is uniformly_continuous by Th1; ::_thesis: verum
end;
theorem :: FCONT_2:4
for X, X1 being set
for f1, f2 being PartFunc of REAL,REAL st X c= dom f1 & X1 c= dom f2 & f1 | X is uniformly_continuous & f2 | X1 is uniformly_continuous holds
(f1 - f2) | (X /\ X1) is uniformly_continuous
proof
let X, X1 be set ; ::_thesis: for f1, f2 being PartFunc of REAL,REAL st X c= dom f1 & X1 c= dom f2 & f1 | X is uniformly_continuous & f2 | X1 is uniformly_continuous holds
(f1 - f2) | (X /\ X1) is uniformly_continuous
let f1, f2 be PartFunc of REAL,REAL; ::_thesis: ( X c= dom f1 & X1 c= dom f2 & f1 | X is uniformly_continuous & f2 | X1 is uniformly_continuous implies (f1 - f2) | (X /\ X1) is uniformly_continuous )
assume that
A1: X c= dom f1 and
A2: X1 c= dom f2 ; ::_thesis: ( not f1 | X is uniformly_continuous or not f2 | X1 is uniformly_continuous or (f1 - f2) | (X /\ X1) is uniformly_continuous )
A3: X /\ X1 c= dom f2 by A2, XBOOLE_1:108;
X /\ X1 c= dom f1 by A1, XBOOLE_1:108;
then X /\ X1 c= (dom f1) /\ (dom f2) by A3, XBOOLE_1:19;
then A4: X /\ X1 c= dom (f1 - f2) by VALUED_1:12;
assume that
A5: f1 | X is uniformly_continuous and
A6: f2 | X1 is uniformly_continuous ; ::_thesis: (f1 - f2) | (X /\ X1) is uniformly_continuous
A7: f2 | (X /\ X1) is uniformly_continuous by A6, Th2, XBOOLE_1:17;
A8: f1 | (X /\ X1) is uniformly_continuous by A5, Th2, XBOOLE_1:17;
now__::_thesis:_for_r_being_Real_st_0_<_r_holds_
ex_p_being_Element_of_REAL_st_
(_0_<_p_&_(_for_x1,_x2_being_Real_st_x1_in_dom_((f1_-_f2)_|_(X_/\_X1))_&_x2_in_dom_((f1_-_f2)_|_(X_/\_X1))_&_abs_(x1_-_x2)_<_p_holds_
abs_(((f1_-_f2)_._x1)_-_((f1_-_f2)_._x2))_<_r_)_)
let r be Real; ::_thesis: ( 0 < r implies ex p being Element of REAL st
( 0 < p & ( for x1, x2 being Real st x1 in dom ((f1 - f2) | (X /\ X1)) & x2 in dom ((f1 - f2) | (X /\ X1)) & abs (x1 - x2) < p holds
abs (((f1 - f2) . x1) - ((f1 - f2) . x2)) < r ) ) )
A9: dom (f1 - f2) = (dom f1) /\ (dom f2) by VALUED_1:12;
assume 0 < r ; ::_thesis: ex p being Element of REAL st
( 0 < p & ( for x1, x2 being Real st x1 in dom ((f1 - f2) | (X /\ X1)) & x2 in dom ((f1 - f2) | (X /\ X1)) & abs (x1 - x2) < p holds
abs (((f1 - f2) . x1) - ((f1 - f2) . x2)) < r ) )
then A10: 0 < r / 2 by XREAL_1:215;
then consider s being Real such that
A11: 0 < s and
A12: for x1, x2 being Real st x1 in dom (f1 | (X /\ X1)) & x2 in dom (f1 | (X /\ X1)) & abs (x1 - x2) < s holds
abs ((f1 . x1) - (f1 . x2)) < r / 2 by A8, Th1;
consider g being Real such that
A13: 0 < g and
A14: for x1, x2 being Real st x1 in dom (f2 | (X /\ X1)) & x2 in dom (f2 | (X /\ X1)) & abs (x1 - x2) < g holds
abs ((f2 . x1) - (f2 . x2)) < r / 2 by A7, A10, Th1;
take p = min (s,g); ::_thesis: ( 0 < p & ( for x1, x2 being Real st x1 in dom ((f1 - f2) | (X /\ X1)) & x2 in dom ((f1 - f2) | (X /\ X1)) & abs (x1 - x2) < p holds
abs (((f1 - f2) . x1) - ((f1 - f2) . x2)) < r ) )
thus 0 < p by A11, A13, XXREAL_0:15; ::_thesis: for x1, x2 being Real st x1 in dom ((f1 - f2) | (X /\ X1)) & x2 in dom ((f1 - f2) | (X /\ X1)) & abs (x1 - x2) < p holds
abs (((f1 - f2) . x1) - ((f1 - f2) . x2)) < r
let x1, x2 be Real; ::_thesis: ( x1 in dom ((f1 - f2) | (X /\ X1)) & x2 in dom ((f1 - f2) | (X /\ X1)) & abs (x1 - x2) < p implies abs (((f1 - f2) . x1) - ((f1 - f2) . x2)) < r )
assume that
A15: x1 in dom ((f1 - f2) | (X /\ X1)) and
A16: x2 in dom ((f1 - f2) | (X /\ X1)) and
A17: abs (x1 - x2) < p ; ::_thesis: abs (((f1 - f2) . x1) - ((f1 - f2) . x2)) < r
A18: x2 in X /\ X1 by A16, RELAT_1:57;
A19: x2 in dom (f1 - f2) by A16, RELAT_1:57;
then x2 in dom f2 by A9, XBOOLE_0:def_4;
then A20: x2 in dom (f2 | (X /\ X1)) by A18, RELAT_1:57;
p <= g by XXREAL_0:17;
then A21: abs (x1 - x2) < g by A17, XXREAL_0:2;
A22: x1 in X /\ X1 by A15, RELAT_1:57;
x2 in dom f1 by A9, A19, XBOOLE_0:def_4;
then A23: x2 in dom (f1 | (X /\ X1)) by A18, RELAT_1:57;
p <= s by XXREAL_0:17;
then A24: abs (x1 - x2) < s by A17, XXREAL_0:2;
A25: x1 in dom (f1 - f2) by A15, RELAT_1:57;
then x1 in dom f2 by A9, XBOOLE_0:def_4;
then x1 in dom (f2 | (X /\ X1)) by A22, RELAT_1:57;
then A26: abs ((f2 . x1) - (f2 . x2)) < r / 2 by A14, A21, A20;
x1 in dom f1 by A9, A25, XBOOLE_0:def_4;
then x1 in dom (f1 | (X /\ X1)) by A22, RELAT_1:57;
then abs ((f1 . x1) - (f1 . x2)) < r / 2 by A12, A24, A23;
then A27: (abs ((f1 . x1) - (f1 . x2))) + (abs ((f2 . x1) - (f2 . x2))) < (r / 2) + (r / 2) by A26, XREAL_1:8;
A28: abs (((f1 . x1) - (f1 . x2)) - ((f2 . x1) - (f2 . x2))) <= (abs ((f1 . x1) - (f1 . x2))) + (abs ((f2 . x1) - (f2 . x2))) by COMPLEX1:57;
abs (((f1 - f2) . x1) - ((f1 - f2) . x2)) = abs (((f1 . x1) - (f2 . x1)) - ((f1 - f2) . x2)) by A4, A22, VALUED_1:13
.= abs (((f1 . x1) - (f2 . x1)) - ((f1 . x2) - (f2 . x2))) by A4, A18, VALUED_1:13
.= abs (((f1 . x1) - (f1 . x2)) - ((f2 . x1) - (f2 . x2))) ;
hence abs (((f1 - f2) . x1) - ((f1 - f2) . x2)) < r by A27, A28, XXREAL_0:2; ::_thesis: verum
end;
hence (f1 - f2) | (X /\ X1) is uniformly_continuous by Th1; ::_thesis: verum
end;
theorem Th5: :: FCONT_2:5
for X being set
for p being Real
for f being PartFunc of REAL,REAL st X c= dom f & f | X is uniformly_continuous holds
(p (#) f) | X is uniformly_continuous
proof
let X be set ; ::_thesis: for p being Real
for f being PartFunc of REAL,REAL st X c= dom f & f | X is uniformly_continuous holds
(p (#) f) | X is uniformly_continuous
let p be Real; ::_thesis: for f being PartFunc of REAL,REAL st X c= dom f & f | X is uniformly_continuous holds
(p (#) f) | X is uniformly_continuous
let f be PartFunc of REAL,REAL; ::_thesis: ( X c= dom f & f | X is uniformly_continuous implies (p (#) f) | X is uniformly_continuous )
assume X c= dom f ; ::_thesis: ( not f | X is uniformly_continuous or (p (#) f) | X is uniformly_continuous )
then A1: X c= dom (p (#) f) by VALUED_1:def_5;
assume A2: f | X is uniformly_continuous ; ::_thesis: (p (#) f) | X is uniformly_continuous
percases ( p = 0 or p <> 0 ) ;
supposeA3: p = 0 ; ::_thesis: (p (#) f) | X is uniformly_continuous
now__::_thesis:_for_r_being_Real_st_0_<_r_holds_
ex_s_being_Real_st_
(_0_<_s_&_(_for_x1,_x2_being_Real_st_x1_in_dom_((p_(#)_f)_|_X)_&_x2_in_dom_((p_(#)_f)_|_X)_&_abs_(x1_-_x2)_<_s_holds_
abs_(((p_(#)_f)_._x1)_-_((p_(#)_f)_._x2))_<_r_)_)
let r be Real; ::_thesis: ( 0 < r implies ex s being Real st
( 0 < s & ( for x1, x2 being Real st x1 in dom ((p (#) f) | X) & x2 in dom ((p (#) f) | X) & abs (x1 - x2) < s holds
abs (((p (#) f) . x1) - ((p (#) f) . x2)) < r ) ) )
assume A4: 0 < r ; ::_thesis: ex s being Real st
( 0 < s & ( for x1, x2 being Real st x1 in dom ((p (#) f) | X) & x2 in dom ((p (#) f) | X) & abs (x1 - x2) < s holds
abs (((p (#) f) . x1) - ((p (#) f) . x2)) < r ) )
then consider s being Real such that
A5: 0 < s and
for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) & abs (x1 - x2) < s holds
abs ((f . x1) - (f . x2)) < r by A2, Th1;
take s = s; ::_thesis: ( 0 < s & ( for x1, x2 being Real st x1 in dom ((p (#) f) | X) & x2 in dom ((p (#) f) | X) & abs (x1 - x2) < s holds
abs (((p (#) f) . x1) - ((p (#) f) . x2)) < r ) )
thus 0 < s by A5; ::_thesis: for x1, x2 being Real st x1 in dom ((p (#) f) | X) & x2 in dom ((p (#) f) | X) & abs (x1 - x2) < s holds
abs (((p (#) f) . x1) - ((p (#) f) . x2)) < r
let x1, x2 be Real; ::_thesis: ( x1 in dom ((p (#) f) | X) & x2 in dom ((p (#) f) | X) & abs (x1 - x2) < s implies abs (((p (#) f) . x1) - ((p (#) f) . x2)) < r )
assume that
A6: x1 in dom ((p (#) f) | X) and
A7: x2 in dom ((p (#) f) | X) and
abs (x1 - x2) < s ; ::_thesis: abs (((p (#) f) . x1) - ((p (#) f) . x2)) < r
A8: x2 in X by A7, RELAT_1:57;
x1 in X by A6, RELAT_1:57;
then abs (((p (#) f) . x1) - ((p (#) f) . x2)) = abs ((p * (f . x1)) - ((p (#) f) . x2)) by A1, VALUED_1:def_5
.= abs (0 - (p * (f . x2))) by A1, A3, A8, VALUED_1:def_5
.= 0 by A3, ABSVALUE:2 ;
hence abs (((p (#) f) . x1) - ((p (#) f) . x2)) < r by A4; ::_thesis: verum
end;
hence (p (#) f) | X is uniformly_continuous by Th1; ::_thesis: verum
end;
supposeA9: p <> 0 ; ::_thesis: (p (#) f) | X is uniformly_continuous
then A10: 0 < abs p by COMPLEX1:47;
A11: 0 <> abs p by A9, COMPLEX1:47;
now__::_thesis:_for_r_being_Real_st_0_<_r_holds_
ex_s_being_Real_st_
(_0_<_s_&_(_for_x1,_x2_being_Real_st_x1_in_dom_((p_(#)_f)_|_X)_&_x2_in_dom_((p_(#)_f)_|_X)_&_abs_(x1_-_x2)_<_s_holds_
abs_(((p_(#)_f)_._x1)_-_((p_(#)_f)_._x2))_<_r_)_)
let r be Real; ::_thesis: ( 0 < r implies ex s being Real st
( 0 < s & ( for x1, x2 being Real st x1 in dom ((p (#) f) | X) & x2 in dom ((p (#) f) | X) & abs (x1 - x2) < s holds
abs (((p (#) f) . x1) - ((p (#) f) . x2)) < r ) ) )
assume 0 < r ; ::_thesis: ex s being Real st
( 0 < s & ( for x1, x2 being Real st x1 in dom ((p (#) f) | X) & x2 in dom ((p (#) f) | X) & abs (x1 - x2) < s holds
abs (((p (#) f) . x1) - ((p (#) f) . x2)) < r ) )
then 0 < r / (abs p) by A10, XREAL_1:139;
then consider s being Real such that
A12: 0 < s and
A13: for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) & abs (x1 - x2) < s holds
abs ((f . x1) - (f . x2)) < r / (abs p) by A2, Th1;
take s = s; ::_thesis: ( 0 < s & ( for x1, x2 being Real st x1 in dom ((p (#) f) | X) & x2 in dom ((p (#) f) | X) & abs (x1 - x2) < s holds
abs (((p (#) f) . x1) - ((p (#) f) . x2)) < r ) )
thus 0 < s by A12; ::_thesis: for x1, x2 being Real st x1 in dom ((p (#) f) | X) & x2 in dom ((p (#) f) | X) & abs (x1 - x2) < s holds
abs (((p (#) f) . x1) - ((p (#) f) . x2)) < r
let x1, x2 be Real; ::_thesis: ( x1 in dom ((p (#) f) | X) & x2 in dom ((p (#) f) | X) & abs (x1 - x2) < s implies abs (((p (#) f) . x1) - ((p (#) f) . x2)) < r )
assume that
A14: x1 in dom ((p (#) f) | X) and
A15: x2 in dom ((p (#) f) | X) and
A16: abs (x1 - x2) < s ; ::_thesis: abs (((p (#) f) . x1) - ((p (#) f) . x2)) < r
A17: x2 in X by A15, RELAT_1:57;
A18: x1 in X by A14, RELAT_1:57;
then A19: abs (((p (#) f) . x1) - ((p (#) f) . x2)) = abs ((p * (f . x1)) - ((p (#) f) . x2)) by A1, VALUED_1:def_5
.= abs ((p * (f . x1)) - (p * (f . x2))) by A1, A17, VALUED_1:def_5
.= abs (p * ((f . x1) - (f . x2)))
.= (abs p) * (abs ((f . x1) - (f . x2))) by COMPLEX1:65 ;
x2 in dom (p (#) f) by A15, RELAT_1:57;
then x2 in dom f by VALUED_1:def_5;
then A20: x2 in dom (f | X) by A17, RELAT_1:57;
x1 in dom (p (#) f) by A14, RELAT_1:57;
then x1 in dom f by VALUED_1:def_5;
then x1 in dom (f | X) by A18, RELAT_1:57;
then (abs p) * (abs ((f . x1) - (f . x2))) < (r / (abs p)) * (abs p) by A10, A13, A16, A20, XREAL_1:68;
hence abs (((p (#) f) . x1) - ((p (#) f) . x2)) < r by A11, A19, XCMPLX_1:87; ::_thesis: verum
end;
hence (p (#) f) | X is uniformly_continuous by Th1; ::_thesis: verum
end;
end;
end;
theorem :: FCONT_2:6
for X being set
for f being PartFunc of REAL,REAL st X c= dom f & f | X is uniformly_continuous holds
(- f) | X is uniformly_continuous
proof
let X be set ; ::_thesis: for f being PartFunc of REAL,REAL st X c= dom f & f | X is uniformly_continuous holds
(- f) | X is uniformly_continuous
let f be PartFunc of REAL,REAL; ::_thesis: ( X c= dom f & f | X is uniformly_continuous implies (- f) | X is uniformly_continuous )
assume A1: X c= dom f ; ::_thesis: ( not f | X is uniformly_continuous or (- f) | X is uniformly_continuous )
A2: - f = (- 1) (#) f ;
assume f | X is uniformly_continuous ; ::_thesis: (- f) | X is uniformly_continuous
hence (- f) | X is uniformly_continuous by A1, A2, Th5; ::_thesis: verum
end;
theorem :: FCONT_2:7
for X being set
for f being PartFunc of REAL,REAL st f | X is uniformly_continuous holds
(abs f) | X is uniformly_continuous
proof
let X be set ; ::_thesis: for f being PartFunc of REAL,REAL st f | X is uniformly_continuous holds
(abs f) | X is uniformly_continuous
let f be PartFunc of REAL,REAL; ::_thesis: ( f | X is uniformly_continuous implies (abs f) | X is uniformly_continuous )
assume A1: f | X is uniformly_continuous ; ::_thesis: (abs f) | X is uniformly_continuous
now__::_thesis:_for_r_being_Real_st_0_<_r_holds_
ex_s_being_Real_st_
(_0_<_s_&_(_for_x1,_x2_being_Real_st_x1_in_dom_((abs_f)_|_X)_&_x2_in_dom_((abs_f)_|_X)_&_abs_(x1_-_x2)_<_s_holds_
abs_(((abs_f)_._x1)_-_((abs_f)_._x2))_<_r_)_)
let r be Real; ::_thesis: ( 0 < r implies ex s being Real st
( 0 < s & ( for x1, x2 being Real st x1 in dom ((abs f) | X) & x2 in dom ((abs f) | X) & abs (x1 - x2) < s holds
abs (((abs f) . x1) - ((abs f) . x2)) < r ) ) )
assume 0 < r ; ::_thesis: ex s being Real st
( 0 < s & ( for x1, x2 being Real st x1 in dom ((abs f) | X) & x2 in dom ((abs f) | X) & abs (x1 - x2) < s holds
abs (((abs f) . x1) - ((abs f) . x2)) < r ) )
then consider s being Real such that
A2: 0 < s and
A3: for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) & abs (x1 - x2) < s holds
abs ((f . x1) - (f . x2)) < r by A1, Th1;
take s = s; ::_thesis: ( 0 < s & ( for x1, x2 being Real st x1 in dom ((abs f) | X) & x2 in dom ((abs f) | X) & abs (x1 - x2) < s holds
abs (((abs f) . x1) - ((abs f) . x2)) < r ) )
thus 0 < s by A2; ::_thesis: for x1, x2 being Real st x1 in dom ((abs f) | X) & x2 in dom ((abs f) | X) & abs (x1 - x2) < s holds
abs (((abs f) . x1) - ((abs f) . x2)) < r
let x1, x2 be Real; ::_thesis: ( x1 in dom ((abs f) | X) & x2 in dom ((abs f) | X) & abs (x1 - x2) < s implies abs (((abs f) . x1) - ((abs f) . x2)) < r )
assume that
A4: x1 in dom ((abs f) | X) and
A5: x2 in dom ((abs f) | X) and
A6: abs (x1 - x2) < s ; ::_thesis: abs (((abs f) . x1) - ((abs f) . x2)) < r
x2 in dom (abs f) by A5, RELAT_1:57;
then A7: x2 in dom f by VALUED_1:def_11;
x2 in X by A5, RELAT_1:57;
then A8: x2 in dom (f | X) by A7, RELAT_1:57;
abs (((abs f) . x1) - ((abs f) . x2)) = abs ((abs (f . x1)) - ((abs f) . x2)) by VALUED_1:18
.= abs ((abs (f . x1)) - (abs (f . x2))) by VALUED_1:18 ;
then A9: abs (((abs f) . x1) - ((abs f) . x2)) <= abs ((f . x1) - (f . x2)) by COMPLEX1:64;
x1 in dom (abs f) by A4, RELAT_1:57;
then A10: x1 in dom f by VALUED_1:def_11;
x1 in X by A4, RELAT_1:57;
then x1 in dom (f | X) by A10, RELAT_1:57;
then abs ((f . x1) - (f . x2)) < r by A3, A6, A8;
hence abs (((abs f) . x1) - ((abs f) . x2)) < r by A9, XXREAL_0:2; ::_thesis: verum
end;
hence (abs f) | X is uniformly_continuous by Th1; ::_thesis: verum
end;
theorem :: FCONT_2:8
for X, X1, Z, Z1 being set
for f1, f2 being PartFunc of REAL,REAL st X c= dom f1 & X1 c= dom f2 & f1 | X is uniformly_continuous & f2 | X1 is uniformly_continuous & f1 | Z is bounded & f2 | Z1 is bounded holds
(f1 (#) f2) | (((X /\ Z) /\ X1) /\ Z1) is uniformly_continuous
proof
let X, X1, Z, Z1 be set ; ::_thesis: for f1, f2 being PartFunc of REAL,REAL st X c= dom f1 & X1 c= dom f2 & f1 | X is uniformly_continuous & f2 | X1 is uniformly_continuous & f1 | Z is bounded & f2 | Z1 is bounded holds
(f1 (#) f2) | (((X /\ Z) /\ X1) /\ Z1) is uniformly_continuous
let f1, f2 be PartFunc of REAL,REAL; ::_thesis: ( X c= dom f1 & X1 c= dom f2 & f1 | X is uniformly_continuous & f2 | X1 is uniformly_continuous & f1 | Z is bounded & f2 | Z1 is bounded implies (f1 (#) f2) | (((X /\ Z) /\ X1) /\ Z1) is uniformly_continuous )
assume that
A1: X c= dom f1 and
A2: X1 c= dom f2 ; ::_thesis: ( not f1 | X is uniformly_continuous or not f2 | X1 is uniformly_continuous or not f1 | Z is bounded or not f2 | Z1 is bounded or (f1 (#) f2) | (((X /\ Z) /\ X1) /\ Z1) is uniformly_continuous )
assume that
A3: f1 | X is uniformly_continuous and
A4: f2 | X1 is uniformly_continuous and
A5: f1 | Z is bounded and
A6: f2 | Z1 is bounded ; ::_thesis: (f1 (#) f2) | (((X /\ Z) /\ X1) /\ Z1) is uniformly_continuous
consider x1 being real number such that
A7: for r being set st r in Z /\ (dom f1) holds
abs (f1 . r) <= x1 by A5, RFUNCT_1:73;
consider x2 being real number such that
A8: for r being set st r in Z1 /\ (dom f2) holds
abs (f2 . r) <= x2 by A6, RFUNCT_1:73;
reconsider x1 = x1, x2 = x2 as Real by XREAL_0:def_1;
set M1 = (abs x1) + 1;
set M2 = (abs x2) + 1;
set M = max (((abs x1) + 1),((abs x2) + 1));
A9: now__::_thesis:_for_r_being_Real_st_r_in_((X_/\_Z)_/\_X1)_/\_Z1_holds_
(_abs_(f1_._r)_<_max_(((abs_x1)_+_1),((abs_x2)_+_1))_&_abs_(f2_._r)_<_max_(((abs_x1)_+_1),((abs_x2)_+_1))_)
let r be Real; ::_thesis: ( r in ((X /\ Z) /\ X1) /\ Z1 implies ( abs (f1 . r) < max (((abs x1) + 1),((abs x2) + 1)) & abs (f2 . r) < max (((abs x1) + 1),((abs x2) + 1)) ) )
A10: (abs x1) + 1 <= max (((abs x1) + 1),((abs x2) + 1)) by XXREAL_0:25;
assume r in ((X /\ Z) /\ X1) /\ Z1 ; ::_thesis: ( abs (f1 . r) < max (((abs x1) + 1),((abs x2) + 1)) & abs (f2 . r) < max (((abs x1) + 1),((abs x2) + 1)) )
then A11: r in (X /\ Z) /\ (X1 /\ Z1) by XBOOLE_1:16;
then A12: r in X /\ Z by XBOOLE_0:def_4;
then A13: r in Z by XBOOLE_0:def_4;
r in X by A12, XBOOLE_0:def_4;
then r in Z /\ (dom f1) by A1, A13, XBOOLE_0:def_4;
then A14: abs (f1 . r) <= x1 by A7;
x1 + 0 < (abs x1) + 1 by ABSVALUE:4, XREAL_1:8;
then abs (f1 . r) < (abs x1) + 1 by A14, XXREAL_0:2;
hence abs (f1 . r) < max (((abs x1) + 1),((abs x2) + 1)) by A10, XXREAL_0:2; ::_thesis: abs (f2 . r) < max (((abs x1) + 1),((abs x2) + 1))
A15: (abs x2) + 1 <= max (((abs x1) + 1),((abs x2) + 1)) by XXREAL_0:25;
A16: r in X1 /\ Z1 by A11, XBOOLE_0:def_4;
then A17: r in Z1 by XBOOLE_0:def_4;
r in X1 by A16, XBOOLE_0:def_4;
then r in Z1 /\ (dom f2) by A2, A17, XBOOLE_0:def_4;
then A18: abs (f2 . r) <= x2 by A8;
x2 + 0 < (abs x2) + 1 by ABSVALUE:4, XREAL_1:8;
then abs (f2 . r) < (abs x2) + 1 by A18, XXREAL_0:2;
hence abs (f2 . r) < max (((abs x1) + 1),((abs x2) + 1)) by A15, XXREAL_0:2; ::_thesis: verum
end;
A19: 0 + 0 < (abs x2) + 1 by COMPLEX1:46, XREAL_1:8;
0 + 0 < (abs x1) + 1 by COMPLEX1:46, XREAL_1:8;
then A20: 0 < max (((abs x1) + 1),((abs x2) + 1)) by A19, XXREAL_0:16;
then A21: 0 < 2 * (max (((abs x1) + 1),((abs x2) + 1))) by XREAL_1:129;
for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1, x2 being Real st x1 in dom ((f1 (#) f2) | (((X /\ Z) /\ X1) /\ Z1)) & x2 in dom ((f1 (#) f2) | (((X /\ Z) /\ X1) /\ Z1)) & abs (x1 - x2) < s holds
abs (((f1 (#) f2) . x1) - ((f1 (#) f2) . x2)) < r ) )
proof
let r be Real; ::_thesis: ( 0 < r implies ex s being Real st
( 0 < s & ( for x1, x2 being Real st x1 in dom ((f1 (#) f2) | (((X /\ Z) /\ X1) /\ Z1)) & x2 in dom ((f1 (#) f2) | (((X /\ Z) /\ X1) /\ Z1)) & abs (x1 - x2) < s holds
abs (((f1 (#) f2) . x1) - ((f1 (#) f2) . x2)) < r ) ) )
assume 0 < r ; ::_thesis: ex s being Real st
( 0 < s & ( for x1, x2 being Real st x1 in dom ((f1 (#) f2) | (((X /\ Z) /\ X1) /\ Z1)) & x2 in dom ((f1 (#) f2) | (((X /\ Z) /\ X1) /\ Z1)) & abs (x1 - x2) < s holds
abs (((f1 (#) f2) . x1) - ((f1 (#) f2) . x2)) < r ) )
then A22: 0 < r / (2 * (max (((abs x1) + 1),((abs x2) + 1)))) by A21, XREAL_1:139;
then consider s being Real such that
A23: 0 < s and
A24: for x1, x2 being Real st x1 in dom (f1 | X) & x2 in dom (f1 | X) & abs (x1 - x2) < s holds
abs ((f1 . x1) - (f1 . x2)) < r / (2 * (max (((abs x1) + 1),((abs x2) + 1)))) by A3, Th1;
consider g being Real such that
A25: 0 < g and
A26: for x1, x2 being Real st x1 in dom (f2 | X1) & x2 in dom (f2 | X1) & abs (x1 - x2) < g holds
abs ((f2 . x1) - (f2 . x2)) < r / (2 * (max (((abs x1) + 1),((abs x2) + 1)))) by A4, A22, Th1;
take p = min (s,g); ::_thesis: ( 0 < p & ( for x1, x2 being Real st x1 in dom ((f1 (#) f2) | (((X /\ Z) /\ X1) /\ Z1)) & x2 in dom ((f1 (#) f2) | (((X /\ Z) /\ X1) /\ Z1)) & abs (x1 - x2) < p holds
abs (((f1 (#) f2) . x1) - ((f1 (#) f2) . x2)) < r ) )
thus 0 < p by A23, A25, XXREAL_0:15; ::_thesis: for x1, x2 being Real st x1 in dom ((f1 (#) f2) | (((X /\ Z) /\ X1) /\ Z1)) & x2 in dom ((f1 (#) f2) | (((X /\ Z) /\ X1) /\ Z1)) & abs (x1 - x2) < p holds
abs (((f1 (#) f2) . x1) - ((f1 (#) f2) . x2)) < r
let y1, y2 be Real; ::_thesis: ( y1 in dom ((f1 (#) f2) | (((X /\ Z) /\ X1) /\ Z1)) & y2 in dom ((f1 (#) f2) | (((X /\ Z) /\ X1) /\ Z1)) & abs (y1 - y2) < p implies abs (((f1 (#) f2) . y1) - ((f1 (#) f2) . y2)) < r )
assume that
A27: y1 in dom ((f1 (#) f2) | (((X /\ Z) /\ X1) /\ Z1)) and
A28: y2 in dom ((f1 (#) f2) | (((X /\ Z) /\ X1) /\ Z1)) ; ::_thesis: ( not abs (y1 - y2) < p or abs (((f1 (#) f2) . y1) - ((f1 (#) f2) . y2)) < r )
assume A29: abs (y1 - y2) < p ; ::_thesis: abs (((f1 (#) f2) . y1) - ((f1 (#) f2) . y2)) < r
A30: y2 in ((X /\ Z) /\ X1) /\ Z1 by A28, RELAT_1:57;
then A31: y2 in (X /\ Z) /\ (X1 /\ Z1) by XBOOLE_1:16;
then y2 in X /\ Z by XBOOLE_0:def_4;
then y2 in X by XBOOLE_0:def_4;
then A32: y2 in dom (f1 | X) by A1, RELAT_1:62;
A33: y1 in ((X /\ Z) /\ X1) /\ Z1 by A27, RELAT_1:57;
then A34: y1 in (X /\ Z) /\ (X1 /\ Z1) by XBOOLE_1:16;
then y1 in X /\ Z by XBOOLE_0:def_4;
then y1 in X by XBOOLE_0:def_4;
then A35: y1 in dom (f1 | X) by A1, RELAT_1:62;
y2 in X1 /\ Z1 by A31, XBOOLE_0:def_4;
then y2 in X1 by XBOOLE_0:def_4;
then A36: y2 in dom (f2 | X1) by A2, RELAT_1:62;
y1 in X1 /\ Z1 by A34, XBOOLE_0:def_4;
then y1 in X1 by XBOOLE_0:def_4;
then A37: y1 in dom (f2 | X1) by A2, RELAT_1:62;
p <= g by XXREAL_0:17;
then abs (y1 - y2) < g by A29, XXREAL_0:2;
then A38: abs ((f2 . y1) - (f2 . y2)) < r / (2 * (max (((abs x1) + 1),((abs x2) + 1)))) by A26, A37, A36;
abs (((f1 (#) f2) . y1) - ((f1 (#) f2) . y2)) = abs (((f1 . y1) * (f2 . y1)) - ((f1 (#) f2) . y2)) by VALUED_1:5
.= abs ((((f1 . y1) * (f2 . y1)) + (((f1 . y1) * (f2 . y2)) - ((f1 . y1) * (f2 . y2)))) - ((f1 . y2) * (f2 . y2))) by VALUED_1:5
.= abs (((f1 . y1) * ((f2 . y1) - (f2 . y2))) + (((f1 . y1) - (f1 . y2)) * (f2 . y2))) ;
then A39: abs (((f1 (#) f2) . y1) - ((f1 (#) f2) . y2)) <= (abs ((f1 . y1) * ((f2 . y1) - (f2 . y2)))) + (abs (((f1 . y1) - (f1 . y2)) * (f2 . y2))) by COMPLEX1:56;
A40: abs ((f1 . y1) * ((f2 . y1) - (f2 . y2))) = (abs (f1 . y1)) * (abs ((f2 . y1) - (f2 . y2))) by COMPLEX1:65;
A41: abs (f2 . y2) < max (((abs x1) + 1),((abs x2) + 1)) by A9, A30;
A42: 0 <= abs (f2 . y2) by COMPLEX1:46;
A43: 0 <= abs ((f1 . y1) - (f1 . y2)) by COMPLEX1:46;
A44: abs (((f1 . y1) - (f1 . y2)) * (f2 . y2)) = (abs (f2 . y2)) * (abs ((f1 . y1) - (f1 . y2))) by COMPLEX1:65;
p <= s by XXREAL_0:17;
then abs (y1 - y2) < s by A29, XXREAL_0:2;
then abs ((f1 . y1) - (f1 . y2)) < r / (2 * (max (((abs x1) + 1),((abs x2) + 1)))) by A24, A35, A32;
then A45: abs (((f1 . y1) - (f1 . y2)) * (f2 . y2)) < (max (((abs x1) + 1),((abs x2) + 1))) * (r / (2 * (max (((abs x1) + 1),((abs x2) + 1))))) by A44, A41, A43, A42, XREAL_1:96;
A46: 0 <= abs (f1 . y1) by COMPLEX1:46;
A47: 0 <= abs ((f2 . y1) - (f2 . y2)) by COMPLEX1:46;
abs (f1 . y1) < max (((abs x1) + 1),((abs x2) + 1)) by A9, A33;
then abs ((f1 . y1) * ((f2 . y1) - (f2 . y2))) < (max (((abs x1) + 1),((abs x2) + 1))) * (r / (2 * (max (((abs x1) + 1),((abs x2) + 1))))) by A40, A38, A47, A46, XREAL_1:96;
then A48: (abs ((f1 . y1) * ((f2 . y1) - (f2 . y2)))) + (abs (((f1 . y1) - (f1 . y2)) * (f2 . y2))) < ((max (((abs x1) + 1),((abs x2) + 1))) * (r / (2 * (max (((abs x1) + 1),((abs x2) + 1)))))) + ((max (((abs x1) + 1),((abs x2) + 1))) * (r / (2 * (max (((abs x1) + 1),((abs x2) + 1)))))) by A45, XREAL_1:8;
((max (((abs x1) + 1),((abs x2) + 1))) * (r / (2 * (max (((abs x1) + 1),((abs x2) + 1)))))) + ((max (((abs x1) + 1),((abs x2) + 1))) * (r / (2 * (max (((abs x1) + 1),((abs x2) + 1)))))) = (max (((abs x1) + 1),((abs x2) + 1))) * ((r / ((max (((abs x1) + 1),((abs x2) + 1))) * 2)) + (r / ((max (((abs x1) + 1),((abs x2) + 1))) * 2)))
.= (r / (max (((abs x1) + 1),((abs x2) + 1)))) * (max (((abs x1) + 1),((abs x2) + 1))) by XCMPLX_1:118
.= r by A20, XCMPLX_1:87 ;
hence abs (((f1 (#) f2) . y1) - ((f1 (#) f2) . y2)) < r by A39, A48, XXREAL_0:2; ::_thesis: verum
end;
hence (f1 (#) f2) | (((X /\ Z) /\ X1) /\ Z1) is uniformly_continuous by Th1; ::_thesis: verum
end;
theorem Th9: :: FCONT_2:9
for X being set
for f being PartFunc of REAL,REAL st X c= dom f & f | X is uniformly_continuous holds
f | X is continuous
proof
let X be set ; ::_thesis: for f being PartFunc of REAL,REAL st X c= dom f & f | X is uniformly_continuous holds
f | X is continuous
let f be PartFunc of REAL,REAL; ::_thesis: ( X c= dom f & f | X is uniformly_continuous implies f | X is continuous )
assume A1: X c= dom f ; ::_thesis: ( not f | X is uniformly_continuous or f | X is continuous )
assume A2: f | X is uniformly_continuous ; ::_thesis: f | X is continuous
now__::_thesis:_for_x0,_r_being_real_number_st_x0_in_X_&_0_<_r_holds_
ex_s_being_real_number_st_
(_0_<_s_&_(_for_x1_being_real_number_st_x1_in_X_&_abs_(x1_-_x0)_<_s_holds_
abs_((f_._x1)_-_(f_._x0))_<_r_)_)
let x0, r be real number ; ::_thesis: ( x0 in X & 0 < r implies ex s being real number st
( 0 < s & ( for x1 being real number st x1 in X & abs (x1 - x0) < s holds
abs ((f . x1) - (f . x0)) < r ) ) )
assume that
A3: x0 in X and
A4: 0 < r ; ::_thesis: ex s being real number st
( 0 < s & ( for x1 being real number st x1 in X & abs (x1 - x0) < s holds
abs ((f . x1) - (f . x0)) < r ) )
A5: x0 in dom (f | X) by A1, A3, RELAT_1:62;
r is Real by XREAL_0:def_1;
then consider s being Real such that
A6: 0 < s and
A7: for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) & abs (x1 - x2) < s holds
abs ((f . x1) - (f . x2)) < r by A2, A4, Th1;
reconsider s = s as real number ;
take s = s; ::_thesis: ( 0 < s & ( for x1 being real number st x1 in X & abs (x1 - x0) < s holds
abs ((f . x1) - (f . x0)) < r ) )
thus 0 < s by A6; ::_thesis: for x1 being real number st x1 in X & abs (x1 - x0) < s holds
abs ((f . x1) - (f . x0)) < r
let x1 be real number ; ::_thesis: ( x1 in X & abs (x1 - x0) < s implies abs ((f . x1) - (f . x0)) < r )
assume that
A8: x1 in X and
A9: abs (x1 - x0) < s ; ::_thesis: abs ((f . x1) - (f . x0)) < r
x1 in dom (f | X) by A1, A8, RELAT_1:62;
hence abs ((f . x1) - (f . x0)) < r by A7, A9, A5; ::_thesis: verum
end;
hence f | X is continuous by A1, FCONT_1:14; ::_thesis: verum
end;
theorem Th10: :: FCONT_2:10
for X being set
for f being PartFunc of REAL,REAL st f | X is Lipschitzian holds
f | X is uniformly_continuous
proof
let X be set ; ::_thesis: for f being PartFunc of REAL,REAL st f | X is Lipschitzian holds
f | X is uniformly_continuous
let f be PartFunc of REAL,REAL; ::_thesis: ( f | X is Lipschitzian implies f | X is uniformly_continuous )
assume f | X is Lipschitzian ; ::_thesis: f | X is uniformly_continuous
then consider r being real number such that
A1: 0 < r and
A2: for x1, x2 being real number st x1 in dom (f | X) & x2 in dom (f | X) holds
abs ((f . x1) - (f . x2)) <= r * (abs (x1 - x2)) by FCONT_1:32;
now__::_thesis:_for_p_being_Real_st_0_<_p_holds_
ex_s_being_Element_of_REAL_st_
(_0_<_s_&_(_for_x1,_x2_being_Real_st_x1_in_dom_(f_|_X)_&_x2_in_dom_(f_|_X)_&_abs_(x1_-_x2)_<_s_holds_
abs_((f_._x1)_-_(f_._x2))_<_p_)_)
reconsider r = r as Real by XREAL_0:def_1;
let p be Real; ::_thesis: ( 0 < p implies ex s being Element of REAL st
( 0 < s & ( for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) & abs (x1 - x2) < s holds
abs ((f . x1) - (f . x2)) < p ) ) )
assume A3: 0 < p ; ::_thesis: ex s being Element of REAL st
( 0 < s & ( for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) & abs (x1 - x2) < s holds
abs ((f . x1) - (f . x2)) < p ) )
take s = p / r; ::_thesis: ( 0 < s & ( for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) & abs (x1 - x2) < s holds
abs ((f . x1) - (f . x2)) < p ) )
thus 0 < s by A1, A3, XREAL_1:139; ::_thesis: for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) & abs (x1 - x2) < s holds
abs ((f . x1) - (f . x2)) < p
let x1, x2 be Real; ::_thesis: ( x1 in dom (f | X) & x2 in dom (f | X) & abs (x1 - x2) < s implies abs ((f . x1) - (f . x2)) < p )
assume that
A4: x1 in dom (f | X) and
A5: x2 in dom (f | X) and
A6: abs (x1 - x2) < s ; ::_thesis: abs ((f . x1) - (f . x2)) < p
A7: r * (abs (x1 - x2)) < s * r by A1, A6, XREAL_1:68;
abs ((f . x1) - (f . x2)) <= r * (abs (x1 - x2)) by A2, A4, A5;
then abs ((f . x1) - (f . x2)) < (p / r) * r by A7, XXREAL_0:2;
hence abs ((f . x1) - (f . x2)) < p by A1, XCMPLX_1:87; ::_thesis: verum
end;
hence f | X is uniformly_continuous by Th1; ::_thesis: verum
end;
theorem Th11: :: FCONT_2:11
for f being PartFunc of REAL,REAL
for Y being Subset of REAL st Y c= dom f & Y is compact & f | Y is continuous holds
f | Y is uniformly_continuous
proof
let f be PartFunc of REAL,REAL; ::_thesis: for Y being Subset of REAL st Y c= dom f & Y is compact & f | Y is continuous holds
f | Y is uniformly_continuous
let Y be Subset of REAL; ::_thesis: ( Y c= dom f & Y is compact & f | Y is continuous implies f | Y is uniformly_continuous )
assume that
A1: Y c= dom f and
A2: Y is compact and
A3: f | Y is continuous ; ::_thesis: f | Y is uniformly_continuous
assume not f | Y is uniformly_continuous ; ::_thesis: contradiction
then consider r being Real such that
A4: 0 < r and
A5: for s being Real st 0 < s holds
ex x1, x2 being Real st
( x1 in dom (f | Y) & x2 in dom (f | Y) & abs (x1 - x2) < s & not abs ((f . x1) - (f . x2)) < r ) by Th1;
defpred S1[ Element of NAT , Real] means ( $2 in Y & ex x2 being Real st
( x2 in Y & abs ($2 - x2) < 1 / ($1 + 1) & not abs ((f . $2) - (f . x2)) < r ) );
A6: now__::_thesis:_for_n_being_Element_of_NAT_ex_x1_being_Real_st_S1[n,x1]
let n be Element of NAT ; ::_thesis: ex x1 being Real st S1[n,x1]
consider x1 being Real such that
A7: ex x2 being Real st
( x1 in dom (f | Y) & x2 in dom (f | Y) & abs (x1 - x2) < 1 / (n + 1) & not abs ((f . x1) - (f . x2)) < r ) by A5, XREAL_1:139;
take x1 = x1; ::_thesis: S1[n,x1]
dom (f | Y) = Y by A1, RELAT_1:62;
hence S1[n,x1] by A7; ::_thesis: verum
end;
consider s1 being Real_Sequence such that
A8: for n being Element of NAT holds S1[n,s1 . n] from FUNCT_2:sch_3(A6);
now__::_thesis:_for_x_being_set_st_x_in_rng_s1_holds_
x_in_Y
let x be set ; ::_thesis: ( x in rng s1 implies x in Y )
assume x in rng s1 ; ::_thesis: x in Y
then ex n being Element of NAT st x = s1 . n by FUNCT_2:113;
hence x in Y by A8; ::_thesis: verum
end;
then A9: rng s1 c= Y by TARSKI:def_3;
then consider q1 being Real_Sequence such that
A10: q1 is subsequence of s1 and
A11: q1 is convergent and
A12: lim q1 in Y by A2, RCOMP_1:def_3;
lim q1 in dom (f | Y) by A1, A12, RELAT_1:57;
then A13: f | Y is_continuous_in lim q1 by A3, FCONT_1:def_2;
rng q1 c= rng s1 by A10, VALUED_0:21;
then A14: rng q1 c= Y by A9, XBOOLE_1:1;
then rng q1 c= dom f by A1, XBOOLE_1:1;
then rng q1 c= (dom f) /\ Y by A14, XBOOLE_1:19;
then A15: rng q1 c= dom (f | Y) by RELAT_1:61;
then A16: (f | Y) . (lim q1) = lim ((f | Y) /* q1) by A11, A13, FCONT_1:def_1;
A17: (f | Y) /* q1 is convergent by A11, A13, A15, FCONT_1:def_1;
defpred S2[ Element of NAT , real number ] means ( $2 in Y & abs ((s1 . $1) - $2) < 1 / ($1 + 1) & not abs ((f . (s1 . $1)) - (f . $2)) < r );
A18: for n being Element of NAT ex x2 being Real st S2[n,x2] by A8;
consider s2 being Real_Sequence such that
A19: for n being Element of NAT holds S2[n,s2 . n] from FUNCT_2:sch_3(A18);
now__::_thesis:_for_x_being_set_st_x_in_rng_s2_holds_
x_in_Y
let x be set ; ::_thesis: ( x in rng s2 implies x in Y )
assume x in rng s2 ; ::_thesis: x in Y
then ex n being Element of NAT st x = s2 . n by FUNCT_2:113;
hence x in Y by A19; ::_thesis: verum
end;
then A20: rng s2 c= Y by TARSKI:def_3;
consider Ns1 being V39() sequence of NAT such that
A21: q1 = s1 * Ns1 by A10, VALUED_0:def_17;
set q2 = q1 - ((s1 - s2) * Ns1);
A22: now__::_thesis:_for_n_being_Element_of_NAT_holds_(q1_-_((s1_-_s2)_*_Ns1))_._n_=_(s2_*_Ns1)_._n
let n be Element of NAT ; ::_thesis: (q1 - ((s1 - s2) * Ns1)) . n = (s2 * Ns1) . n
thus (q1 - ((s1 - s2) * Ns1)) . n = ((s1 * Ns1) . n) - (((s1 - s2) * Ns1) . n) by A21, RFUNCT_2:1
.= (s1 . (Ns1 . n)) - (((s1 - s2) * Ns1) . n) by FUNCT_2:15
.= (s1 . (Ns1 . n)) - ((s1 - s2) . (Ns1 . n)) by FUNCT_2:15
.= (s1 . (Ns1 . n)) - ((s1 . (Ns1 . n)) - (s2 . (Ns1 . n))) by RFUNCT_2:1
.= (s2 * Ns1) . n by FUNCT_2:15 ; ::_thesis: verum
end;
then A23: q1 - ((s1 - s2) * Ns1) = s2 * Ns1 by FUNCT_2:63;
q1 - ((s1 - s2) * Ns1) is subsequence of s2 by A22, FUNCT_2:63, VALUED_0:def_17;
then rng (q1 - ((s1 - s2) * Ns1)) c= rng s2 by VALUED_0:21;
then A24: rng (q1 - ((s1 - s2) * Ns1)) c= Y by A20, XBOOLE_1:1;
then rng (q1 - ((s1 - s2) * Ns1)) c= dom f by A1, XBOOLE_1:1;
then rng (q1 - ((s1 - s2) * Ns1)) c= (dom f) /\ Y by A24, XBOOLE_1:19;
then A25: rng (q1 - ((s1 - s2) * Ns1)) c= dom (f | Y) by RELAT_1:61;
A26: now__::_thesis:_for_p_being_real_number_st_0_<_p_holds_
ex_k_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_k_<=_m_holds_
abs_(((s1_-_s2)_._m)_-_0)_<_p
let p be real number ; ::_thesis: ( 0 < p implies ex k being Element of NAT st
for m being Element of NAT st k <= m holds
abs (((s1 - s2) . m) - 0) < p )
assume A27: 0 < p ; ::_thesis: ex k being Element of NAT st
for m being Element of NAT st k <= m holds
abs (((s1 - s2) . m) - 0) < p
consider k being Element of NAT such that
A28: p " < k by SEQ_4:3;
take k = k; ::_thesis: for m being Element of NAT st k <= m holds
abs (((s1 - s2) . m) - 0) < p
let m be Element of NAT ; ::_thesis: ( k <= m implies abs (((s1 - s2) . m) - 0) < p )
assume k <= m ; ::_thesis: abs (((s1 - s2) . m) - 0) < p
then k + 1 <= m + 1 by XREAL_1:6;
then 1 / (m + 1) <= 1 / (k + 1) by XREAL_1:118;
then A29: abs ((s1 . m) - (s2 . m)) < 1 / (k + 1) by A19, XXREAL_0:2;
k < k + 1 by NAT_1:13;
then p " < k + 1 by A28, XXREAL_0:2;
then 1 / (k + 1) < 1 / (p ") by A27, XREAL_1:76;
then A30: 1 / (k + 1) < p by XCMPLX_1:216;
abs (((s1 - s2) . m) - 0) = abs ((s1 . m) - (s2 . m)) by RFUNCT_2:1;
hence abs (((s1 - s2) . m) - 0) < p by A30, A29, XXREAL_0:2; ::_thesis: verum
end;
then A31: s1 - s2 is convergent by SEQ_2:def_6;
A32: (s1 - s2) * Ns1 is subsequence of s1 - s2 by VALUED_0:def_17;
then A33: (s1 - s2) * Ns1 is convergent by A31, SEQ_4:16;
lim (s1 - s2) = 0 by A26, A31, SEQ_2:def_7;
then lim ((s1 - s2) * Ns1) = 0 by A31, A32, SEQ_4:17;
then A34: lim (q1 - ((s1 - s2) * Ns1)) = (lim q1) - 0 by A11, A33, SEQ_2:12
.= lim q1 ;
A35: q1 - ((s1 - s2) * Ns1) is convergent by A11, A33, SEQ_2:11;
then A36: (f | Y) /* (q1 - ((s1 - s2) * Ns1)) is convergent by A13, A34, A25, FCONT_1:def_1;
then A37: ((f | Y) /* q1) - ((f | Y) /* (q1 - ((s1 - s2) * Ns1))) is convergent by A17, SEQ_2:11;
(f | Y) . (lim q1) = lim ((f | Y) /* (q1 - ((s1 - s2) * Ns1))) by A13, A35, A34, A25, FCONT_1:def_1;
then A38: lim (((f | Y) /* q1) - ((f | Y) /* (q1 - ((s1 - s2) * Ns1)))) = ((f | Y) . (lim q1)) - ((f | Y) . (lim q1)) by A17, A16, A36, SEQ_2:12
.= 0 ;
now__::_thesis:_for_n_being_Element_of_NAT_holds_contradiction
let n be Element of NAT ; ::_thesis: contradiction
consider k being Element of NAT such that
A39: for m being Element of NAT st k <= m holds
abs (((((f | Y) /* q1) - ((f | Y) /* (q1 - ((s1 - s2) * Ns1)))) . m) - 0) < r by A4, A37, A38, SEQ_2:def_7;
A40: q1 . k in rng q1 by VALUED_0:28;
A41: (q1 - ((s1 - s2) * Ns1)) . k in rng (q1 - ((s1 - s2) * Ns1)) by VALUED_0:28;
abs (((((f | Y) /* q1) - ((f | Y) /* (q1 - ((s1 - s2) * Ns1)))) . k) - 0) = abs ((((f | Y) /* q1) . k) - (((f | Y) /* (q1 - ((s1 - s2) * Ns1))) . k)) by RFUNCT_2:1
.= abs (((f | Y) . (q1 . k)) - (((f | Y) /* (q1 - ((s1 - s2) * Ns1))) . k)) by A15, FUNCT_2:108
.= abs (((f | Y) . (q1 . k)) - ((f | Y) . ((q1 - ((s1 - s2) * Ns1)) . k))) by A25, FUNCT_2:108
.= abs ((f . (q1 . k)) - ((f | Y) . ((q1 - ((s1 - s2) * Ns1)) . k))) by A15, A40, FUNCT_1:47
.= abs ((f . (q1 . k)) - (f . ((q1 - ((s1 - s2) * Ns1)) . k))) by A25, A41, FUNCT_1:47
.= abs ((f . (s1 . (Ns1 . k))) - (f . ((s2 * Ns1) . k))) by A21, A23, FUNCT_2:15
.= abs ((f . (s1 . (Ns1 . k))) - (f . (s2 . (Ns1 . k)))) by FUNCT_2:15 ;
hence contradiction by A19, A39; ::_thesis: verum
end;
hence contradiction ; ::_thesis: verum
end;
theorem :: FCONT_2:12
for Y being Subset of REAL
for f being PartFunc of REAL,REAL st Y c= dom f & Y is compact & f | Y is uniformly_continuous holds
f .: Y is compact by Th9, FCONT_1:29;
theorem :: FCONT_2:13
for f being PartFunc of REAL,REAL
for Y being Subset of REAL st Y <> {} & Y c= dom f & Y is compact & f | Y is uniformly_continuous holds
ex x1, x2 being Real st
( x1 in Y & x2 in Y & f . x1 = upper_bound (f .: Y) & f . x2 = lower_bound (f .: Y) )
proof
let f be PartFunc of REAL,REAL; ::_thesis: for Y being Subset of REAL st Y <> {} & Y c= dom f & Y is compact & f | Y is uniformly_continuous holds
ex x1, x2 being Real st
( x1 in Y & x2 in Y & f . x1 = upper_bound (f .: Y) & f . x2 = lower_bound (f .: Y) )
let Y be Subset of REAL; ::_thesis: ( Y <> {} & Y c= dom f & Y is compact & f | Y is uniformly_continuous implies ex x1, x2 being Real st
( x1 in Y & x2 in Y & f . x1 = upper_bound (f .: Y) & f . x2 = lower_bound (f .: Y) ) )
assume that
A1: Y <> {} and
A2: Y c= dom f and
A3: Y is compact and
A4: f | Y is uniformly_continuous ; ::_thesis: ex x1, x2 being Real st
( x1 in Y & x2 in Y & f . x1 = upper_bound (f .: Y) & f . x2 = lower_bound (f .: Y) )
ex x1, x2 being real number st
( x1 in Y & x2 in Y & f . x1 = upper_bound (f .: Y) & f . x2 = lower_bound (f .: Y) ) by A1, A2, A3, A4, Th9, FCONT_1:31;
hence ex x1, x2 being Real st
( x1 in Y & x2 in Y & f . x1 = upper_bound (f .: Y) & f . x2 = lower_bound (f .: Y) ) ; ::_thesis: verum
end;
theorem :: FCONT_2:14
for X being set
for f being PartFunc of REAL,REAL st X c= dom f & f | X is V8() holds
f | X is uniformly_continuous by Th10;
theorem Th15: :: FCONT_2:15
for p, g being Real
for f being PartFunc of REAL,REAL st p <= g & [.p,g.] c= dom f & f | [.p,g.] is continuous holds
for r being Real st r in [.(f . p),(f . g).] \/ [.(f . g),(f . p).] holds
ex s being Real st
( s in [.p,g.] & r = f . s )
proof
let p, g be Real; ::_thesis: for f being PartFunc of REAL,REAL st p <= g & [.p,g.] c= dom f & f | [.p,g.] is continuous holds
for r being Real st r in [.(f . p),(f . g).] \/ [.(f . g),(f . p).] holds
ex s being Real st
( s in [.p,g.] & r = f . s )
let f be PartFunc of REAL,REAL; ::_thesis: ( p <= g & [.p,g.] c= dom f & f | [.p,g.] is continuous implies for r being Real st r in [.(f . p),(f . g).] \/ [.(f . g),(f . p).] holds
ex s being Real st
( s in [.p,g.] & r = f . s ) )
assume that
A1: p <= g and
A2: [.p,g.] c= dom f and
A3: f | [.p,g.] is continuous ; ::_thesis: for r being Real st r in [.(f . p),(f . g).] \/ [.(f . g),(f . p).] holds
ex s being Real st
( s in [.p,g.] & r = f . s )
let r be Real; ::_thesis: ( r in [.(f . p),(f . g).] \/ [.(f . g),(f . p).] implies ex s being Real st
( s in [.p,g.] & r = f . s ) )
assume A4: r in [.(f . p),(f . g).] \/ [.(f . g),(f . p).] ; ::_thesis: ex s being Real st
( s in [.p,g.] & r = f . s )
A5: [.p,g.] is compact by RCOMP_1:6;
A6: ( f . p < f . g implies ex s being Real st
( s in [.p,g.] & r = f . s ) )
proof
reconsider f1 = [.p,g.] --> r as Function of [.p,g.],REAL by FUNCOP_1:45;
assume that
A7: f . p < f . g and
A8: for s being Real st s in [.p,g.] holds
r <> f . s ; ::_thesis: contradiction
[.(f . p),(f . g).] \/ [.(f . g),(f . p).] = [.(f . p),(f . g).] \/ {} by A7, XXREAL_1:29
.= [.(f . p),(f . g).] ;
then r in { s where s is Real : ( f . p <= s & s <= f . g ) } by A4, RCOMP_1:def_1;
then A9: ex s being Real st
( s = r & f . p <= s & s <= f . g ) ;
p in { s where s is Real : ( p <= s & s <= g ) } by A1;
then p in [.p,g.] by RCOMP_1:def_1;
then A10: r <> f . p by A8;
reconsider f1 = f1 as PartFunc of REAL,REAL ;
A11: dom f1 = [.p,g.] by FUNCOP_1:13;
then A12: [.p,g.] c= (dom f1) /\ (dom f) by A2, XBOOLE_1:19;
then A13: [.p,g.] c= dom (f1 - f) by VALUED_1:12;
A14: (abs (f1 - f)) " {0} = {}
proof
assume (abs (f1 - f)) " {0} <> {} ; ::_thesis: contradiction
then consider x2 being Real such that
A15: x2 in (abs (f1 - f)) " {0} by SUBSET_1:4;
x2 in dom (abs (f1 - f)) by A15, FUNCT_1:def_7;
then A16: x2 in dom (f1 - f) by VALUED_1:def_11;
then x2 in (dom f1) /\ (dom f) by VALUED_1:12;
then A17: x2 in [.p,g.] by A11, XBOOLE_0:def_4;
(abs (f1 - f)) . x2 in {0} by A15, FUNCT_1:def_7;
then (abs (f1 - f)) . x2 = 0 by TARSKI:def_1;
then abs ((f1 - f) . x2) = 0 by VALUED_1:18;
then (f1 - f) . x2 = 0 by ABSVALUE:2;
then (f1 . x2) - (f . x2) = 0 by A16, VALUED_1:13;
then r - (f . x2) = 0 by A17, FUNCOP_1:7;
hence contradiction by A8, A17; ::_thesis: verum
end;
A18: dom ((abs (f1 - f)) ^) = (dom (abs (f1 - f))) \ ((abs (f1 - f)) " {0}) by RFUNCT_1:def_2
.= dom (f1 - f) by A14, VALUED_1:def_11
.= [.p,g.] /\ (dom f) by A11, VALUED_1:12
.= [.p,g.] by A2, XBOOLE_1:28 ;
for x0 being Real st x0 in [.p,g.] /\ (dom f1) holds
f1 . x0 = r by A11, FUNCOP_1:7;
then f1 | [.p,g.] is V8() by PARTFUN2:57;
then (f1 - f) | [.p,g.] is continuous by A3, A12, FCONT_1:18;
then (abs (f1 - f)) | [.p,g.] is continuous by A13, FCONT_1:21;
then ((abs (f1 - f)) ^) | [.p,g.] is continuous by A14, FCONT_1:22;
then ((abs (f1 - f)) ^) .: [.p,g.] is real-bounded by A5, A18, FCONT_1:29, RCOMP_1:10;
then consider M being real number such that
A19: M is UpperBound of ((abs (f1 - f)) ^) .: [.p,g.] by XXREAL_2:def_10;
A20: for x1 being real number st x1 in ((abs (f1 - f)) ^) .: [.p,g.] holds
x1 <= M by A19, XXREAL_2:def_1;
0 + 0 < (abs M) + 1 by COMPLEX1:46, XREAL_1:8;
then 0 < ((abs M) + 1) " ;
then A21: 0 < 1 / ((abs M) + 1) by XCMPLX_1:215;
f | [.p,g.] is uniformly_continuous by A2, A3, Th11, RCOMP_1:6;
then consider s being Real such that
A22: 0 < s and
A23: for x1, x2 being Real st x1 in dom (f | [.p,g.]) & x2 in dom (f | [.p,g.]) & abs (x1 - x2) < s holds
abs ((f . x1) - (f . x2)) < 1 / ((abs M) + 1) by A21, Th1;
A24: now__::_thesis:_for_x1_being_Real_st_x1_in_[.p,g.]_holds_
1_/_((abs_M)_+_1)_<_abs_(r_-_(f_._x1))
let x1 be Real; ::_thesis: ( x1 in [.p,g.] implies 1 / ((abs M) + 1) < abs (r - (f . x1)) )
assume A25: x1 in [.p,g.] ; ::_thesis: 1 / ((abs M) + 1) < abs (r - (f . x1))
then ((abs (f1 - f)) ^) . x1 in ((abs (f1 - f)) ^) .: [.p,g.] by A18, FUNCT_1:def_6;
then ((abs (f1 - f)) ^) . x1 <= M by A20;
then ((abs (f1 - f)) . x1) " <= M by A18, A25, RFUNCT_1:def_2;
then A26: (abs ((f1 - f) . x1)) " <= M by VALUED_1:18;
x1 in (dom f1) /\ (dom f) by A2, A11, A25, XBOOLE_0:def_4;
then x1 in dom (f1 - f) by VALUED_1:12;
then (abs ((f1 . x1) - (f . x1))) " <= M by A26, VALUED_1:13;
then A27: (abs (r - (f . x1))) " <= M by A25, FUNCOP_1:7;
r - (f . x1) <> 0 by A8, A25;
then A28: 0 < abs (r - (f . x1)) by COMPLEX1:47;
M + 0 < (abs M) + 1 by ABSVALUE:4, XREAL_1:8;
then (abs (r - (f . x1))) " < (abs M) + 1 by A27, XXREAL_0:2;
then 1 / ((abs M) + 1) < 1 / ((abs (r - (f . x1))) ") by A28, XREAL_1:76;
hence 1 / ((abs M) + 1) < abs (r - (f . x1)) by XCMPLX_1:216; ::_thesis: verum
end;
now__::_thesis:_contradiction
percases ( p = g or p <> g ) ;
suppose p = g ; ::_thesis: contradiction
hence contradiction by A7; ::_thesis: verum
end;
suppose p <> g ; ::_thesis: contradiction
then p < g by A1, XXREAL_0:1;
then A29: 0 < g - p by XREAL_1:50;
then A30: 0 < (g - p) / s by A22, XREAL_1:139;
consider k being Element of NAT such that
A31: (g - p) / s < k by SEQ_4:3;
((g - p) / s) * s < s * k by A22, A31, XREAL_1:68;
then g - p < s * k by A22, XCMPLX_1:87;
then (g - p) / k < (s * k) / k by A31, A30, XREAL_1:74;
then (g - p) / k < (s * k) * (k ") by XCMPLX_0:def_9;
then (g - p) / k < s * (k * (k ")) ;
then A32: (g - p) / k < s * 1 by A31, A30, XCMPLX_0:def_7;
deffunc H1( Element of NAT ) -> Element of REAL = p + (((g - p) / k) * $1);
consider s1 being Real_Sequence such that
A33: for n being Element of NAT holds s1 . n = H1(n) from SEQ_1:sch_1();
A34: 0 < (g - p) / k by A29, A31, A30, XREAL_1:139;
A35: now__::_thesis:_for_n_being_Element_of_NAT_st_n_<_k_holds_
(_s1_._n_in_[.p,g.]_&_s1_._(n_+_1)_in_[.p,g.]_&_abs_((f_._(s1_._(n_+_1)))_-_(f_._(s1_._n)))_<_1_/_((abs_M)_+_1)_)
let n be Element of NAT ; ::_thesis: ( n < k implies ( s1 . n in [.p,g.] & s1 . (n + 1) in [.p,g.] & abs ((f . (s1 . (n + 1))) - (f . (s1 . n))) < 1 / ((abs M) + 1) ) )
A36: dom (f | [.p,g.]) = [.p,g.] by A2, RELAT_1:62;
assume A37: n < k ; ::_thesis: ( s1 . n in [.p,g.] & s1 . (n + 1) in [.p,g.] & abs ((f . (s1 . (n + 1))) - (f . (s1 . n))) < 1 / ((abs M) + 1) )
then ((g - p) / k) * n < ((g - p) / k) * k by A34, XREAL_1:68;
then ((g - p) / k) * n < g - p by A31, A30, XCMPLX_1:87;
then p + (((g - p) / k) * n) < p + (g - p) by XREAL_1:6;
then A38: s1 . n < p + (g - p) by A33;
n + 1 <= k by A37, NAT_1:13;
then ((g - p) / k) * (n + 1) <= ((g - p) / k) * k by A29, XREAL_1:64;
then ((g - p) / k) * (n + 1) <= g - p by A31, A30, XCMPLX_1:87;
then p + (((g - p) / k) * (n + 1)) <= p + (g - p) by XREAL_1:7;
then A39: s1 . (n + 1) <= p + (g - p) by A33;
p + 0 <= p + (((g - p) / k) * n) by A29, XREAL_1:7;
then p <= s1 . n by A33;
then s1 . n in { x2 where x2 is Real : ( p <= x2 & x2 <= g ) } by A38;
hence A40: s1 . n in [.p,g.] by RCOMP_1:def_1; ::_thesis: ( s1 . (n + 1) in [.p,g.] & abs ((f . (s1 . (n + 1))) - (f . (s1 . n))) < 1 / ((abs M) + 1) )
p + 0 <= p + (((g - p) / k) * (n + 1)) by A29, XREAL_1:7;
then p <= s1 . (n + 1) by A33;
then s1 . (n + 1) in { x2 where x2 is Real : ( p <= x2 & x2 <= g ) } by A39;
hence A41: s1 . (n + 1) in [.p,g.] by RCOMP_1:def_1; ::_thesis: abs ((f . (s1 . (n + 1))) - (f . (s1 . n))) < 1 / ((abs M) + 1)
abs ((s1 . (n + 1)) - (s1 . n)) = abs ((p + (((g - p) / k) * (n + 1))) - (s1 . n)) by A33
.= abs ((p + (((g - p) / k) * (n + 1))) - (p + (((g - p) / k) * n))) by A33
.= (g - p) / k by A29, ABSVALUE:def_1 ;
hence abs ((f . (s1 . (n + 1))) - (f . (s1 . n))) < 1 / ((abs M) + 1) by A23, A32, A40, A41, A36; ::_thesis: verum
end;
defpred S1[ Nat] means r <= f . (s1 . $1);
A42: s1 . k = p + (((g - p) / k) * k) by A33
.= p + (g - p) by A31, A30, XCMPLX_1:87
.= g ;
then A43: ex n being Nat st S1[n] by A9;
consider l being Nat such that
A44: ( S1[l] & ( for m being Nat st S1[m] holds
l <= m ) ) from NAT_1:sch_5(A43);
s1 . 0 = p + (((g - p) / k) * 0) by A33
.= p ;
then l <> 0 by A9, A10, A44, XXREAL_0:1;
then consider l1 being Nat such that
A45: l = l1 + 1 by NAT_1:6;
reconsider l1 = l1 as Element of NAT by ORDINAL1:def_12;
A46: r - (f . (s1 . l1)) <= (f . (s1 . (l1 + 1))) - (f . (s1 . l1)) by A44, A45, XREAL_1:9;
l1 + 1 <= k by A9, A42, A44, A45;
then A47: l1 < k by NAT_1:13;
then A48: abs ((f . (s1 . (l1 + 1))) - (f . (s1 . l1))) < 1 / ((abs M) + 1) by A35;
f . (s1 . l1) < r
proof
assume r <= f . (s1 . l1) ; ::_thesis: contradiction
then l <= l1 by A44;
then l + 0 < l by A45, XREAL_1:8;
hence contradiction ; ::_thesis: verum
end;
then A49: 0 < r - (f . (s1 . l1)) by XREAL_1:50;
then 0 < (f . (s1 . (l1 + 1))) - (f . (s1 . l1)) by A44, A45, XREAL_1:9;
then abs ((f . (s1 . (l1 + 1))) - (f . (s1 . l1))) = (f . (s1 . (l1 + 1))) - (f . (s1 . l1)) by ABSVALUE:def_1;
then A50: abs (r - (f . (s1 . l1))) <= abs ((f . (s1 . (l1 + 1))) - (f . (s1 . l1))) by A49, A46, ABSVALUE:def_1;
s1 . l1 in [.p,g.] by A35, A47;
hence contradiction by A24, A50, A48, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
hence contradiction ; ::_thesis: verum
end;
A51: ( f . g < f . p implies ex s being Real st
( s in [.p,g.] & r = f . s ) )
proof
reconsider f1 = [.p,g.] --> r as Function of [.p,g.],REAL by FUNCOP_1:45;
assume that
A52: f . g < f . p and
A53: for s being Real st s in [.p,g.] holds
r <> f . s ; ::_thesis: contradiction
[.(f . p),(f . g).] \/ [.(f . g),(f . p).] = {} \/ [.(f . g),(f . p).] by A52, XXREAL_1:29
.= [.(f . g),(f . p).] ;
then r in { s where s is Real : ( f . g <= s & s <= f . p ) } by A4, RCOMP_1:def_1;
then A54: ex s being Real st
( s = r & f . g <= s & s <= f . p ) ;
g in { s where s is Real : ( p <= s & s <= g ) } by A1;
then g in [.p,g.] by RCOMP_1:def_1;
then A55: r <> f . g by A53;
reconsider f1 = f1 as PartFunc of REAL,REAL ;
A56: dom f1 = [.p,g.] by FUNCOP_1:13;
then A57: [.p,g.] c= (dom f1) /\ (dom f) by A2, XBOOLE_1:19;
then A58: [.p,g.] c= dom (f1 - f) by VALUED_1:12;
A59: (abs (f1 - f)) " {0} = {}
proof
assume (abs (f1 - f)) " {0} <> {} ; ::_thesis: contradiction
then consider x2 being Real such that
A60: x2 in (abs (f1 - f)) " {0} by SUBSET_1:4;
x2 in dom (abs (f1 - f)) by A60, FUNCT_1:def_7;
then A61: x2 in dom (f1 - f) by VALUED_1:def_11;
then x2 in (dom f1) /\ (dom f) by VALUED_1:12;
then A62: x2 in [.p,g.] by A56, XBOOLE_0:def_4;
(abs (f1 - f)) . x2 in {0} by A60, FUNCT_1:def_7;
then (abs (f1 - f)) . x2 = 0 by TARSKI:def_1;
then abs ((f1 - f) . x2) = 0 by VALUED_1:18;
then (f1 - f) . x2 = 0 by ABSVALUE:2;
then (f1 . x2) - (f . x2) = 0 by A61, VALUED_1:13;
then r - (f . x2) = 0 by A62, FUNCOP_1:7;
hence contradiction by A53, A62; ::_thesis: verum
end;
A63: dom ((abs (f1 - f)) ^) = (dom (abs (f1 - f))) \ ((abs (f1 - f)) " {0}) by RFUNCT_1:def_2
.= dom (f1 - f) by A59, VALUED_1:def_11
.= [.p,g.] /\ (dom f) by A56, VALUED_1:12
.= [.p,g.] by A2, XBOOLE_1:28 ;
for x0 being Real st x0 in [.p,g.] /\ (dom f1) holds
f1 . x0 = r by A56, FUNCOP_1:7;
then f1 | [.p,g.] is V8() by PARTFUN2:57;
then (f1 - f) | [.p,g.] is continuous by A3, A57, FCONT_1:18;
then (abs (f1 - f)) | [.p,g.] is continuous by A58, FCONT_1:21;
then ((abs (f1 - f)) ^) | [.p,g.] is continuous by A59, FCONT_1:22;
then ((abs (f1 - f)) ^) .: [.p,g.] is real-bounded by A5, A63, FCONT_1:29, RCOMP_1:10;
then consider M being real number such that
A64: M is UpperBound of ((abs (f1 - f)) ^) .: [.p,g.] by XXREAL_2:def_10;
A65: for x1 being real number st x1 in ((abs (f1 - f)) ^) .: [.p,g.] holds
x1 <= M by A64, XXREAL_2:def_1;
0 + 0 < (abs M) + 1 by COMPLEX1:46, XREAL_1:8;
then 0 < ((abs M) + 1) " ;
then A66: 0 < 1 / ((abs M) + 1) by XCMPLX_1:215;
f | [.p,g.] is uniformly_continuous by A2, A3, Th11, RCOMP_1:6;
then consider s being Real such that
A67: 0 < s and
A68: for x1, x2 being Real st x1 in dom (f | [.p,g.]) & x2 in dom (f | [.p,g.]) & abs (x1 - x2) < s holds
abs ((f . x1) - (f . x2)) < 1 / ((abs M) + 1) by A66, Th1;
A69: now__::_thesis:_for_x1_being_Real_st_x1_in_[.p,g.]_holds_
1_/_((abs_M)_+_1)_<_abs_(r_-_(f_._x1))
let x1 be Real; ::_thesis: ( x1 in [.p,g.] implies 1 / ((abs M) + 1) < abs (r - (f . x1)) )
assume A70: x1 in [.p,g.] ; ::_thesis: 1 / ((abs M) + 1) < abs (r - (f . x1))
then ((abs (f1 - f)) ^) . x1 in ((abs (f1 - f)) ^) .: [.p,g.] by A63, FUNCT_1:def_6;
then ((abs (f1 - f)) ^) . x1 <= M by A65;
then ((abs (f1 - f)) . x1) " <= M by A63, A70, RFUNCT_1:def_2;
then A71: (abs ((f1 - f) . x1)) " <= M by VALUED_1:18;
x1 in (dom f1) /\ (dom f) by A2, A56, A70, XBOOLE_0:def_4;
then x1 in dom (f1 - f) by VALUED_1:12;
then (abs ((f1 . x1) - (f . x1))) " <= M by A71, VALUED_1:13;
then A72: (abs (r - (f . x1))) " <= M by A70, FUNCOP_1:7;
r - (f . x1) <> 0 by A53, A70;
then A73: 0 < abs (r - (f . x1)) by COMPLEX1:47;
M + 0 < (abs M) + 1 by ABSVALUE:4, XREAL_1:8;
then (abs (r - (f . x1))) " < (abs M) + 1 by A72, XXREAL_0:2;
then 1 / ((abs M) + 1) < 1 / ((abs (r - (f . x1))) ") by A73, XREAL_1:76;
hence 1 / ((abs M) + 1) < abs (r - (f . x1)) by XCMPLX_1:216; ::_thesis: verum
end;
now__::_thesis:_contradiction
percases ( p = g or p <> g ) ;
suppose p = g ; ::_thesis: contradiction
hence contradiction by A52; ::_thesis: verum
end;
suppose p <> g ; ::_thesis: contradiction
then p < g by A1, XXREAL_0:1;
then A74: 0 < g - p by XREAL_1:50;
then A75: 0 < (g - p) / s by A67, XREAL_1:139;
consider k being Element of NAT such that
A76: (g - p) / s < k by SEQ_4:3;
((g - p) / s) * s < s * k by A67, A76, XREAL_1:68;
then g - p < s * k by A67, XCMPLX_1:87;
then (g - p) / k < (s * k) / k by A76, A75, XREAL_1:74;
then (g - p) / k < (s * k) * (k ") by XCMPLX_0:def_9;
then (g - p) / k < s * (k * (k ")) ;
then A77: (g - p) / k < s * 1 by A76, A75, XCMPLX_0:def_7;
deffunc H1( Element of NAT ) -> Element of REAL = g - (((g - p) / k) * $1);
consider s1 being Real_Sequence such that
A78: for n being Element of NAT holds s1 . n = H1(n) from SEQ_1:sch_1();
A79: 0 < (g - p) / k by A74, A76, A75, XREAL_1:139;
A80: now__::_thesis:_for_n_being_Element_of_NAT_st_n_<_k_holds_
(_s1_._n_in_[.p,g.]_&_s1_._(n_+_1)_in_[.p,g.]_&_abs_((f_._(s1_._(n_+_1)))_-_(f_._(s1_._n)))_<_1_/_((abs_M)_+_1)_)
let n be Element of NAT ; ::_thesis: ( n < k implies ( s1 . n in [.p,g.] & s1 . (n + 1) in [.p,g.] & abs ((f . (s1 . (n + 1))) - (f . (s1 . n))) < 1 / ((abs M) + 1) ) )
A81: dom (f | [.p,g.]) = [.p,g.] by A2, RELAT_1:62;
assume A82: n < k ; ::_thesis: ( s1 . n in [.p,g.] & s1 . (n + 1) in [.p,g.] & abs ((f . (s1 . (n + 1))) - (f . (s1 . n))) < 1 / ((abs M) + 1) )
then ((g - p) / k) * n < ((g - p) / k) * k by A79, XREAL_1:68;
then ((g - p) / k) * n < g - p by A76, A75, XCMPLX_1:87;
then g - (g - p) < g - (((g - p) / k) * n) by XREAL_1:15;
then A83: g - (g - p) < s1 . n by A78;
n + 1 <= k by A82, NAT_1:13;
then ((g - p) / k) * (n + 1) <= ((g - p) / k) * k by A74, XREAL_1:64;
then ((g - p) / k) * (n + 1) <= g - p by A76, A75, XCMPLX_1:87;
then g - (g - p) <= g - (((g - p) / k) * (n + 1)) by XREAL_1:13;
then A84: g - (g - p) <= s1 . (n + 1) by A78;
g - (((g - p) / k) * n) <= g - 0 by A74, XREAL_1:13;
then s1 . n <= g by A78;
then s1 . n in { x2 where x2 is Real : ( p <= x2 & x2 <= g ) } by A83;
hence A85: s1 . n in [.p,g.] by RCOMP_1:def_1; ::_thesis: ( s1 . (n + 1) in [.p,g.] & abs ((f . (s1 . (n + 1))) - (f . (s1 . n))) < 1 / ((abs M) + 1) )
g - (((g - p) / k) * (n + 1)) <= g - 0 by A74, XREAL_1:13;
then s1 . (n + 1) <= g by A78;
then s1 . (n + 1) in { x2 where x2 is Real : ( p <= x2 & x2 <= g ) } by A84;
hence A86: s1 . (n + 1) in [.p,g.] by RCOMP_1:def_1; ::_thesis: abs ((f . (s1 . (n + 1))) - (f . (s1 . n))) < 1 / ((abs M) + 1)
abs ((s1 . (n + 1)) - (s1 . n)) = abs ((g - (((g - p) / k) * (n + 1))) - (s1 . n)) by A78
.= abs ((g - (((g - p) / k) * (n + 1))) - (g - (((g - p) / k) * n))) by A78
.= abs (- ((((g - p) / k) * (n + 1)) - (((g - p) / k) * n)))
.= abs (((g - p) / k) * ((n + 1) - n)) by COMPLEX1:52
.= (g - p) / k by A74, ABSVALUE:def_1 ;
hence abs ((f . (s1 . (n + 1))) - (f . (s1 . n))) < 1 / ((abs M) + 1) by A68, A77, A85, A86, A81; ::_thesis: verum
end;
defpred S1[ Nat] means r <= f . (s1 . $1);
A87: s1 . k = g - (((g - p) / k) * k) by A78
.= g - (g - p) by A76, A75, XCMPLX_1:87
.= p ;
then A88: ex n being Nat st S1[n] by A54;
consider l being Nat such that
A89: ( S1[l] & ( for m being Nat st S1[m] holds
l <= m ) ) from NAT_1:sch_5(A88);
s1 . 0 = g - (((g - p) / k) * 0) by A78
.= g ;
then l <> 0 by A54, A55, A89, XXREAL_0:1;
then consider l1 being Nat such that
A90: l = l1 + 1 by NAT_1:6;
reconsider l1 = l1 as Element of NAT by ORDINAL1:def_12;
A91: r - (f . (s1 . l1)) <= (f . (s1 . (l1 + 1))) - (f . (s1 . l1)) by A89, A90, XREAL_1:9;
l1 + 1 <= k by A54, A87, A89, A90;
then A92: l1 < k by NAT_1:13;
then A93: abs ((f . (s1 . (l1 + 1))) - (f . (s1 . l1))) < 1 / ((abs M) + 1) by A80;
f . (s1 . l1) < r
proof
assume r <= f . (s1 . l1) ; ::_thesis: contradiction
then l <= l1 by A89;
then l + 0 < l by A90, XREAL_1:8;
hence contradiction ; ::_thesis: verum
end;
then A94: 0 < r - (f . (s1 . l1)) by XREAL_1:50;
then 0 < (f . (s1 . (l1 + 1))) - (f . (s1 . l1)) by A89, A90, XREAL_1:9;
then abs ((f . (s1 . (l1 + 1))) - (f . (s1 . l1))) = (f . (s1 . (l1 + 1))) - (f . (s1 . l1)) by ABSVALUE:def_1;
then A95: abs (r - (f . (s1 . l1))) <= abs ((f . (s1 . (l1 + 1))) - (f . (s1 . l1))) by A94, A91, ABSVALUE:def_1;
s1 . l1 in [.p,g.] by A80, A92;
hence contradiction by A69, A95, A93, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
hence contradiction ; ::_thesis: verum
end;
( f . p = f . g implies ex s being Real st
( s in [.p,g.] & r = f . s ) )
proof
assume A96: f . p = f . g ; ::_thesis: ex s being Real st
( s in [.p,g.] & r = f . s )
take p ; ::_thesis: ( p in [.p,g.] & r = f . p )
thus p in [.p,g.] by A1, XXREAL_1:1; ::_thesis: r = f . p
[.(f . p),(f . g).] \/ [.(f . g),(f . p).] = {(f . p)} by A96, XXREAL_1:17;
hence r = f . p by A4, TARSKI:def_1; ::_thesis: verum
end;
hence ex s being Real st
( s in [.p,g.] & r = f . s ) by A6, A51, XXREAL_0:1; ::_thesis: verum
end;
theorem Th16: :: FCONT_2:16
for p, g being Real
for f being PartFunc of REAL,REAL st p <= g & [.p,g.] c= dom f & f | [.p,g.] is continuous holds
for r being Real st r in [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] holds
ex s being Real st
( s in [.p,g.] & r = f . s )
proof
let p, g be Real; ::_thesis: for f being PartFunc of REAL,REAL st p <= g & [.p,g.] c= dom f & f | [.p,g.] is continuous holds
for r being Real st r in [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] holds
ex s being Real st
( s in [.p,g.] & r = f . s )
let f be PartFunc of REAL,REAL; ::_thesis: ( p <= g & [.p,g.] c= dom f & f | [.p,g.] is continuous implies for r being Real st r in [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] holds
ex s being Real st
( s in [.p,g.] & r = f . s ) )
assume that
A1: p <= g and
A2: [.p,g.] c= dom f and
A3: f | [.p,g.] is continuous ; ::_thesis: for r being Real st r in [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] holds
ex s being Real st
( s in [.p,g.] & r = f . s )
[.p,g.] is compact by RCOMP_1:6;
then A4: f .: [.p,g.] is real-bounded by A2, A3, FCONT_1:29, RCOMP_1:10;
set ub = upper_bound (f .: [.p,g.]);
set lb = lower_bound (f .: [.p,g.]);
[.p,g.] <> {} by A1, XXREAL_1:1;
then consider x2, x1 being real number such that
A5: x2 in [.p,g.] and
A6: x1 in [.p,g.] and
A7: f . x2 = upper_bound (f .: [.p,g.]) and
A8: f . x1 = lower_bound (f .: [.p,g.]) by A2, A3, FCONT_1:31, RCOMP_1:6;
reconsider x1 = x1, x2 = x2 as Real by XREAL_0:def_1;
let r be Real; ::_thesis: ( r in [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] implies ex s being Real st
( s in [.p,g.] & r = f . s ) )
assume A9: r in [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] ; ::_thesis: ex s being Real st
( s in [.p,g.] & r = f . s )
f . x1 in f .: [.p,g.] by A2, A6, FUNCT_1:def_6;
then A10: [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] = [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] \/ [.(upper_bound (f .: [.p,g.])),(lower_bound (f .: [.p,g.])).] by A4, SEQ_4:11, XXREAL_1:222;
now__::_thesis:_ex_s_being_Real_st_
(_s_in_[.p,g.]_&_r_=_f_._s_)
percases ( x1 <= x2 or x2 <= x1 ) ;
supposeA11: x1 <= x2 ; ::_thesis: ex s being Real st
( s in [.p,g.] & r = f . s )
A12: [.x1,x2.] c= [.p,g.] by A5, A6, XXREAL_2:def_12;
A13: [.x1,x2.] c= [.p,g.] by A5, A6, XXREAL_2:def_12;
then f | [.x1,x2.] is continuous by A3, FCONT_1:16;
then consider s being Real such that
A14: s in [.x1,x2.] and
A15: r = f . s by A2, A9, A7, A8, A10, A11, A12, Th15, XBOOLE_1:1;
take s = s; ::_thesis: ( s in [.p,g.] & r = f . s )
thus ( s in [.p,g.] & r = f . s ) by A13, A14, A15; ::_thesis: verum
end;
supposeA16: x2 <= x1 ; ::_thesis: ex s being Real st
( s in [.p,g.] & r = f . s )
A17: [.x2,x1.] c= [.p,g.] by A5, A6, XXREAL_2:def_12;
A18: [.x2,x1.] c= [.p,g.] by A5, A6, XXREAL_2:def_12;
then f | [.x2,x1.] is continuous by A3, FCONT_1:16;
then consider s being Real such that
A19: s in [.x2,x1.] and
A20: r = f . s by A2, A9, A7, A8, A10, A16, A17, Th15, XBOOLE_1:1;
take s = s; ::_thesis: ( s in [.p,g.] & r = f . s )
thus ( s in [.p,g.] & r = f . s ) by A18, A19, A20; ::_thesis: verum
end;
end;
end;
hence ex s being Real st
( s in [.p,g.] & r = f . s ) ; ::_thesis: verum
end;
theorem Th17: :: FCONT_2:17
for p, g being Real
for f being PartFunc of REAL,REAL st f is one-to-one & [.p,g.] c= dom f & p <= g & f | [.p,g.] is continuous & not f | [.p,g.] is increasing holds
f | [.p,g.] is decreasing
proof
let p, g be Real; ::_thesis: for f being PartFunc of REAL,REAL st f is one-to-one & [.p,g.] c= dom f & p <= g & f | [.p,g.] is continuous & not f | [.p,g.] is increasing holds
f | [.p,g.] is decreasing
let f be PartFunc of REAL,REAL; ::_thesis: ( f is one-to-one & [.p,g.] c= dom f & p <= g & f | [.p,g.] is continuous & not f | [.p,g.] is increasing implies f | [.p,g.] is decreasing )
assume that
A1: f is one-to-one and
A2: [.p,g.] c= dom f and
A3: p <= g and
A4: f | [.p,g.] is continuous and
A5: not f | [.p,g.] is increasing and
A6: not f | [.p,g.] is decreasing ; ::_thesis: contradiction
now__::_thesis:_contradiction
percases ( p = g or p <> g ) ;
suppose p = g ; ::_thesis: contradiction
then [.p,g.] = {p} by XXREAL_1:17;
hence contradiction by A6, RFUNCT_2:44; ::_thesis: verum
end;
supposeA7: p <> g ; ::_thesis: contradiction
A8: g in [.p,g.] by A3, XXREAL_1:1;
A9: p in [.p,g.] by A3, XXREAL_1:1;
then A10: f . p <> f . g by A1, A2, A7, A8, FUNCT_1:def_4;
now__::_thesis:_contradiction
percases ( f . p < f . g or f . p > f . g ) by A10, XXREAL_0:1;
supposeA11: f . p < f . g ; ::_thesis: contradiction
A12: for x1 being Real st p <= x1 & x1 <= g holds
( f . p <= f . x1 & f . x1 <= f . g )
proof
let x1 be Real; ::_thesis: ( p <= x1 & x1 <= g implies ( f . p <= f . x1 & f . x1 <= f . g ) )
assume that
A13: p <= x1 and
A14: x1 <= g and
A15: ( not f . p <= f . x1 or not f . x1 <= f . g ) ; ::_thesis: contradiction
now__::_thesis:_contradiction
percases ( f . x1 < f . p or f . g < f . x1 ) by A15;
supposeA16: f . x1 < f . p ; ::_thesis: contradiction
then f . p in { r where r is Real : ( f . x1 <= r & r <= f . g ) } by A11;
then f . p in [.(f . x1),(f . g).] by RCOMP_1:def_1;
then A17: f . p in [.(f . x1),(f . g).] \/ [.(f . g),(f . x1).] by XBOOLE_0:def_3;
x1 in { r where r is Real : ( p <= r & r <= g ) } by A13, A14;
then A18: x1 in [.p,g.] by RCOMP_1:def_1;
g in [.p,g.] by A3, XXREAL_1:1;
then A19: [.x1,g.] c= [.p,g.] by A18, XXREAL_2:def_12;
then f | [.x1,g.] is continuous by A4, FCONT_1:16;
then consider s being Real such that
A20: s in [.x1,g.] and
A21: f . s = f . p by A2, A14, A19, A17, Th15, XBOOLE_1:1;
s in { t where t is Real : ( x1 <= t & t <= g ) } by A20, RCOMP_1:def_1;
then A22: ex r being Real st
( r = s & x1 <= r & r <= g ) ;
A23: x1 > p by A13, A16, XXREAL_0:1;
s in [.p,g.] by A19, A20;
hence contradiction by A1, A2, A9, A23, A21, A22, FUNCT_1:def_4; ::_thesis: verum
end;
supposeA24: f . g < f . x1 ; ::_thesis: contradiction
then f . g in { r where r is Real : ( f . p <= r & r <= f . x1 ) } by A11;
then f . g in [.(f . p),(f . x1).] by RCOMP_1:def_1;
then A25: f . g in [.(f . p),(f . x1).] \/ [.(f . x1),(f . p).] by XBOOLE_0:def_3;
x1 in { r where r is Real : ( p <= r & r <= g ) } by A13, A14;
then A26: x1 in [.p,g.] by RCOMP_1:def_1;
p in [.p,g.] by A3, XXREAL_1:1;
then A27: [.p,x1.] c= [.p,g.] by A26, XXREAL_2:def_12;
then f | [.p,x1.] is continuous by A4, FCONT_1:16;
then consider s being Real such that
A28: s in [.p,x1.] and
A29: f . s = f . g by A2, A13, A27, A25, Th15, XBOOLE_1:1;
s in { t where t is Real : ( p <= t & t <= x1 ) } by A28, RCOMP_1:def_1;
then A30: ex r being Real st
( r = s & p <= r & r <= x1 ) ;
s in [.p,g.] by A27, A28;
then s = g by A1, A2, A8, A29, FUNCT_1:def_4;
hence contradiction by A14, A24, A30, XXREAL_0:1; ::_thesis: verum
end;
end;
end;
hence contradiction ; ::_thesis: verum
end;
consider x1, x2 being Real such that
A31: x1 in [.p,g.] /\ (dom f) and
A32: x2 in [.p,g.] /\ (dom f) and
A33: x1 < x2 and
A34: f . x2 <= f . x1 by A5, RFUNCT_2:20;
A35: x1 in [.p,g.] by A31, XBOOLE_0:def_4;
then A36: [.p,x1.] c= [.p,g.] by A9, XXREAL_2:def_12;
A37: x2 in [.p,g.] by A32, XBOOLE_0:def_4;
then x2 in { r where r is Real : ( p <= r & r <= g ) } by RCOMP_1:def_1;
then ex r being Real st
( r = x2 & p <= r & r <= g ) ;
then f . p <= f . x2 by A12;
then f . x2 in { r where r is Real : ( f . p <= r & r <= f . x1 ) } by A34;
then f . x2 in [.(f . p),(f . x1).] by RCOMP_1:def_1;
then A38: f . x2 in [.(f . p),(f . x1).] \/ [.(f . x1),(f . p).] by XBOOLE_0:def_3;
x1 in { t where t is Real : ( p <= t & t <= g ) } by A35, RCOMP_1:def_1;
then A39: ex r being Real st
( r = x1 & p <= r & r <= g ) ;
p in [.p,g.] by A3, XXREAL_1:1;
then A40: [.p,x1.] c= [.p,g.] by A35, XXREAL_2:def_12;
then f | [.p,x1.] is continuous by A4, FCONT_1:16;
then consider s being Real such that
A41: s in [.p,x1.] and
A42: f . s = f . x2 by A2, A39, A38, A36, Th15, XBOOLE_1:1;
s in { t where t is Real : ( p <= t & t <= x1 ) } by A41, RCOMP_1:def_1;
then A43: ex r being Real st
( r = s & p <= r & r <= x1 ) ;
s in [.p,g.] by A40, A41;
hence contradiction by A1, A2, A33, A37, A42, A43, FUNCT_1:def_4; ::_thesis: verum
end;
supposeA44: f . p > f . g ; ::_thesis: contradiction
A45: for x1 being Real st p <= x1 & x1 <= g holds
( f . g <= f . x1 & f . x1 <= f . p )
proof
let x1 be Real; ::_thesis: ( p <= x1 & x1 <= g implies ( f . g <= f . x1 & f . x1 <= f . p ) )
assume that
A46: p <= x1 and
A47: x1 <= g and
A48: ( not f . g <= f . x1 or not f . x1 <= f . p ) ; ::_thesis: contradiction
now__::_thesis:_contradiction
percases ( f . x1 < f . g or f . p < f . x1 ) by A48;
supposeA49: f . x1 < f . g ; ::_thesis: contradiction
now__::_thesis:_contradiction
percases ( g = x1 or g <> x1 ) ;
suppose g = x1 ; ::_thesis: contradiction
hence contradiction by A49; ::_thesis: verum
end;
supposeA50: g <> x1 ; ::_thesis: contradiction
x1 in { r where r is Real : ( p <= r & r <= g ) } by A46, A47;
then A51: x1 in [.p,g.] by RCOMP_1:def_1;
f . g in { r where r is Real : ( f . x1 <= r & r <= f . p ) } by A44, A49;
then f . g in [.(f . x1),(f . p).] by RCOMP_1:def_1;
then A52: f . g in [.(f . p),(f . x1).] \/ [.(f . x1),(f . p).] by XBOOLE_0:def_3;
p in [.p,g.] by A3, XXREAL_1:1;
then A53: [.p,x1.] c= [.p,g.] by A51, XXREAL_2:def_12;
then f | [.p,x1.] is continuous by A4, FCONT_1:16;
then consider s being Real such that
A54: s in [.p,x1.] and
A55: f . s = f . g by A2, A46, A53, A52, Th15, XBOOLE_1:1;
s in { t where t is Real : ( p <= t & t <= x1 ) } by A54, RCOMP_1:def_1;
then A56: ex r being Real st
( r = s & p <= r & r <= x1 ) ;
s in [.p,g.] by A53, A54;
then s = g by A1, A2, A8, A55, FUNCT_1:def_4;
hence contradiction by A47, A50, A56, XXREAL_0:1; ::_thesis: verum
end;
end;
end;
hence contradiction ; ::_thesis: verum
end;
supposeA57: f . p < f . x1 ; ::_thesis: contradiction
now__::_thesis:_contradiction
percases ( p = x1 or p <> x1 ) ;
suppose p = x1 ; ::_thesis: contradiction
hence contradiction by A57; ::_thesis: verum
end;
supposeA58: p <> x1 ; ::_thesis: contradiction
x1 in { r where r is Real : ( p <= r & r <= g ) } by A46, A47;
then A59: x1 in [.p,g.] by RCOMP_1:def_1;
f . p in { r where r is Real : ( f . g <= r & r <= f . x1 ) } by A44, A57;
then f . p in [.(f . g),(f . x1).] by RCOMP_1:def_1;
then A60: f . p in [.(f . x1),(f . g).] \/ [.(f . g),(f . x1).] by XBOOLE_0:def_3;
g in [.p,g.] by A3, XXREAL_1:1;
then A61: [.x1,g.] c= [.p,g.] by A59, XXREAL_2:def_12;
then f | [.x1,g.] is continuous by A4, FCONT_1:16;
then consider s being Real such that
A62: s in [.x1,g.] and
A63: f . s = f . p by A2, A47, A61, A60, Th15, XBOOLE_1:1;
s in { t where t is Real : ( x1 <= t & t <= g ) } by A62, RCOMP_1:def_1;
then A64: ex r being Real st
( r = s & x1 <= r & r <= g ) ;
s in [.p,g.] by A61, A62;
then s = p by A1, A2, A9, A63, FUNCT_1:def_4;
hence contradiction by A46, A58, A64, XXREAL_0:1; ::_thesis: verum
end;
end;
end;
hence contradiction ; ::_thesis: verum
end;
end;
end;
hence contradiction ; ::_thesis: verum
end;
consider x1, x2 being Real such that
A65: x1 in [.p,g.] /\ (dom f) and
A66: x2 in [.p,g.] /\ (dom f) and
A67: x1 < x2 and
A68: f . x1 <= f . x2 by A6, RFUNCT_2:21;
A69: x2 in [.p,g.] by A66, XBOOLE_0:def_4;
then A70: [.x2,g.] c= [.p,g.] by A8, XXREAL_2:def_12;
A71: x1 in [.p,g.] by A65, XBOOLE_0:def_4;
then x1 in { t where t is Real : ( p <= t & t <= g ) } by RCOMP_1:def_1;
then ex r being Real st
( r = x1 & p <= r & r <= g ) ;
then f . g <= f . x1 by A45;
then f . x1 in { r where r is Real : ( f . g <= r & r <= f . x2 ) } by A68;
then f . x1 in [.(f . g),(f . x2).] by RCOMP_1:def_1;
then A72: f . x1 in [.(f . x2),(f . g).] \/ [.(f . g),(f . x2).] by XBOOLE_0:def_3;
x2 in { r where r is Real : ( p <= r & r <= g ) } by A69, RCOMP_1:def_1;
then A73: ex r being Real st
( r = x2 & p <= r & r <= g ) ;
g in [.p,g.] by A3, XXREAL_1:1;
then A74: [.x2,g.] c= [.p,g.] by A69, XXREAL_2:def_12;
then f | [.x2,g.] is continuous by A4, FCONT_1:16;
then consider s being Real such that
A75: s in [.x2,g.] and
A76: f . s = f . x1 by A2, A73, A72, A70, Th15, XBOOLE_1:1;
s in { t where t is Real : ( x2 <= t & t <= g ) } by A75, RCOMP_1:def_1;
then A77: ex r being Real st
( r = s & x2 <= r & r <= g ) ;
s in [.p,g.] by A74, A75;
hence contradiction by A1, A2, A67, A71, A76, A77, FUNCT_1:def_4; ::_thesis: verum
end;
end;
end;
hence contradiction ; ::_thesis: verum
end;
end;
end;
hence contradiction ; ::_thesis: verum
end;
theorem :: FCONT_2:18
for p, g being Real
for f being PartFunc of REAL,REAL st f is one-to-one & p <= g & [.p,g.] c= dom f & f | [.p,g.] is continuous & not ( lower_bound (f .: [.p,g.]) = f . p & upper_bound (f .: [.p,g.]) = f . g ) holds
( lower_bound (f .: [.p,g.]) = f . g & upper_bound (f .: [.p,g.]) = f . p )
proof
let p, g be Real; ::_thesis: for f being PartFunc of REAL,REAL st f is one-to-one & p <= g & [.p,g.] c= dom f & f | [.p,g.] is continuous & not ( lower_bound (f .: [.p,g.]) = f . p & upper_bound (f .: [.p,g.]) = f . g ) holds
( lower_bound (f .: [.p,g.]) = f . g & upper_bound (f .: [.p,g.]) = f . p )
let f be PartFunc of REAL,REAL; ::_thesis: ( f is one-to-one & p <= g & [.p,g.] c= dom f & f | [.p,g.] is continuous & not ( lower_bound (f .: [.p,g.]) = f . p & upper_bound (f .: [.p,g.]) = f . g ) implies ( lower_bound (f .: [.p,g.]) = f . g & upper_bound (f .: [.p,g.]) = f . p ) )
assume that
A1: f is one-to-one and
A2: p <= g and
A3: [.p,g.] c= dom f and
A4: f | [.p,g.] is continuous ; ::_thesis: ( ( lower_bound (f .: [.p,g.]) = f . p & upper_bound (f .: [.p,g.]) = f . g ) or ( lower_bound (f .: [.p,g.]) = f . g & upper_bound (f .: [.p,g.]) = f . p ) )
A5: p in [.p,g.] by A2, XXREAL_1:1;
then A6: f . p in f .: [.p,g.] by A3, FUNCT_1:def_6;
A7: g in [.p,g.] by A2, XXREAL_1:1;
then A8: f . g in f .: [.p,g.] by A3, FUNCT_1:def_6;
A9: g in [.p,g.] /\ (dom f) by A3, A7, XBOOLE_0:def_4;
A10: p in [.p,g.] /\ (dom f) by A3, A5, XBOOLE_0:def_4;
[.p,g.] <> {} by A2, XXREAL_1:1;
then consider x1, x2 being real number such that
A11: x1 in [.p,g.] and
A12: x2 in [.p,g.] and
A13: f . x1 = upper_bound (f .: [.p,g.]) and
A14: f . x2 = lower_bound (f .: [.p,g.]) by A3, A4, FCONT_1:31, RCOMP_1:6;
A15: x2 in [.p,g.] /\ (dom f) by A3, A12, XBOOLE_0:def_4;
x2 in { t where t is Real : ( p <= t & t <= g ) } by A12, RCOMP_1:def_1;
then A16: ex r being Real st
( r = x2 & p <= r & r <= g ) ;
x1 in { r where r is Real : ( p <= r & r <= g ) } by A11, RCOMP_1:def_1;
then A17: ex r being Real st
( r = x1 & p <= r & r <= g ) ;
[.p,g.] is compact by RCOMP_1:6;
then A18: f .: [.p,g.] is real-bounded by A3, A4, FCONT_1:29, RCOMP_1:10;
A19: x1 in [.p,g.] /\ (dom f) by A3, A11, XBOOLE_0:def_4;
now__::_thesis:_(_(_lower_bound_(f_.:_[.p,g.])_=_f_._p_&_upper_bound_(f_.:_[.p,g.])_=_f_._g_)_or_(_lower_bound_(f_.:_[.p,g.])_=_f_._g_&_upper_bound_(f_.:_[.p,g.])_=_f_._p_)_)
percases ( f | [.p,g.] is increasing or f | [.p,g.] is decreasing ) by A1, A2, A3, A4, Th17;
supposeA20: f | [.p,g.] is increasing ; ::_thesis: ( ( lower_bound (f .: [.p,g.]) = f . p & upper_bound (f .: [.p,g.]) = f . g ) or ( lower_bound (f .: [.p,g.]) = f . g & upper_bound (f .: [.p,g.]) = f . p ) )
A21: now__::_thesis:_not_x1_<>_g
assume x1 <> g ; ::_thesis: contradiction
then x1 < g by A17, XXREAL_0:1;
then f . x1 < f . g by A9, A19, A20, RFUNCT_2:20;
hence contradiction by A8, A18, A13, SEQ_4:def_1; ::_thesis: verum
end;
now__::_thesis:_not_x2_<>_p
assume x2 <> p ; ::_thesis: contradiction
then p < x2 by A16, XXREAL_0:1;
then f . p < f . x2 by A10, A15, A20, RFUNCT_2:20;
hence contradiction by A6, A18, A14, SEQ_4:def_2; ::_thesis: verum
end;
hence ( ( lower_bound (f .: [.p,g.]) = f . p & upper_bound (f .: [.p,g.]) = f . g ) or ( lower_bound (f .: [.p,g.]) = f . g & upper_bound (f .: [.p,g.]) = f . p ) ) by A13, A14, A21; ::_thesis: verum
end;
supposeA22: f | [.p,g.] is decreasing ; ::_thesis: ( ( lower_bound (f .: [.p,g.]) = f . p & upper_bound (f .: [.p,g.]) = f . g ) or ( lower_bound (f .: [.p,g.]) = f . g & upper_bound (f .: [.p,g.]) = f . p ) )
A23: now__::_thesis:_not_x2_<>_g
assume x2 <> g ; ::_thesis: contradiction
then x2 < g by A16, XXREAL_0:1;
then f . g < f . x2 by A9, A15, A22, RFUNCT_2:21;
hence contradiction by A8, A18, A14, SEQ_4:def_2; ::_thesis: verum
end;
now__::_thesis:_not_x1_<>_p
assume x1 <> p ; ::_thesis: contradiction
then p < x1 by A17, XXREAL_0:1;
then f . x1 < f . p by A10, A19, A22, RFUNCT_2:21;
hence contradiction by A6, A18, A13, SEQ_4:def_1; ::_thesis: verum
end;
hence ( ( lower_bound (f .: [.p,g.]) = f . p & upper_bound (f .: [.p,g.]) = f . g ) or ( lower_bound (f .: [.p,g.]) = f . g & upper_bound (f .: [.p,g.]) = f . p ) ) by A13, A14, A23; ::_thesis: verum
end;
end;
end;
hence ( ( lower_bound (f .: [.p,g.]) = f . p & upper_bound (f .: [.p,g.]) = f . g ) or ( lower_bound (f .: [.p,g.]) = f . g & upper_bound (f .: [.p,g.]) = f . p ) ) ; ::_thesis: verum
end;
theorem Th19: :: FCONT_2:19
for p, g being Real
for f being PartFunc of REAL,REAL st p <= g & [.p,g.] c= dom f & f | [.p,g.] is continuous holds
f .: [.p,g.] = [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).]
proof
let p, g be Real; ::_thesis: for f being PartFunc of REAL,REAL st p <= g & [.p,g.] c= dom f & f | [.p,g.] is continuous holds
f .: [.p,g.] = [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).]
let f be PartFunc of REAL,REAL; ::_thesis: ( p <= g & [.p,g.] c= dom f & f | [.p,g.] is continuous implies f .: [.p,g.] = [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] )
assume that
A1: p <= g and
A2: [.p,g.] c= dom f and
A3: f | [.p,g.] is continuous ; ::_thesis: f .: [.p,g.] = [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).]
[.p,g.] is compact by RCOMP_1:6;
then A4: f .: [.p,g.] is real-bounded by A2, A3, FCONT_1:29, RCOMP_1:10;
now__::_thesis:_for_y_being_Real_holds_
(_(_y_in_f_.:_[.p,g.]_implies_y_in_[.(lower_bound_(f_.:_[.p,g.])),(upper_bound_(f_.:_[.p,g.])).]_)_&_(_y_in_[.(lower_bound_(f_.:_[.p,g.])),(upper_bound_(f_.:_[.p,g.])).]_implies_y_in_f_.:_[.p,g.]_)_)
let y be Real; ::_thesis: ( ( y in f .: [.p,g.] implies y in [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] ) & ( y in [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] implies y in f .: [.p,g.] ) )
thus ( y in f .: [.p,g.] implies y in [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] ) ::_thesis: ( y in [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] implies y in f .: [.p,g.] )
proof
assume A5: y in f .: [.p,g.] ; ::_thesis: y in [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).]
then A6: y >= lower_bound (f .: [.p,g.]) by A4, SEQ_4:def_2;
y <= upper_bound (f .: [.p,g.]) by A4, A5, SEQ_4:def_1;
then y in { s where s is Real : ( lower_bound (f .: [.p,g.]) <= s & s <= upper_bound (f .: [.p,g.]) ) } by A6;
hence y in [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] by RCOMP_1:def_1; ::_thesis: verum
end;
assume y in [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] ; ::_thesis: y in f .: [.p,g.]
then ex x0 being Real st
( x0 in [.p,g.] & y = f . x0 ) by A1, A2, A3, Th16;
hence y in f .: [.p,g.] by A2, FUNCT_1:def_6; ::_thesis: verum
end;
hence f .: [.p,g.] = [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] by SUBSET_1:3; ::_thesis: verum
end;
theorem :: FCONT_2:20
for p, g being Real
for f being one-to-one PartFunc of REAL,REAL st p <= g & [.p,g.] c= dom f & f | [.p,g.] is continuous holds
(f ") | [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] is continuous
proof
let p, g be Real; ::_thesis: for f being one-to-one PartFunc of REAL,REAL st p <= g & [.p,g.] c= dom f & f | [.p,g.] is continuous holds
(f ") | [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] is continuous
let f be one-to-one PartFunc of REAL,REAL; ::_thesis: ( p <= g & [.p,g.] c= dom f & f | [.p,g.] is continuous implies (f ") | [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] is continuous )
assume that
A1: p <= g and
A2: [.p,g.] c= dom f and
A3: f | [.p,g.] is continuous ; ::_thesis: (f ") | [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] is continuous
now__::_thesis:_(f_")_|_[.(lower_bound_(f_.:_[.p,g.])),(upper_bound_(f_.:_[.p,g.])).]_is_continuous
percases ( f | [.p,g.] is increasing or f | [.p,g.] is decreasing ) by A1, A2, A3, Th17;
suppose f | [.p,g.] is increasing ; ::_thesis: (f ") | [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] is continuous
then ((f | [.p,g.]) ") | (f .: [.p,g.]) is increasing by RFUNCT_2:51;
then ((f ") | (f .: [.p,g.])) | (f .: [.p,g.]) is increasing by RFUNCT_2:17;
then (f ") | (f .: [.p,g.]) is monotone by RELAT_1:72;
then A4: (f ") | [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] is monotone by A1, A2, A3, Th19;
(f ") .: [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] = (f ") .: (f .: [.p,g.]) by A1, A2, A3, Th19
.= ((f ") | (f .: [.p,g.])) .: (f .: [.p,g.]) by RELAT_1:129
.= ((f | [.p,g.]) ") .: (f .: [.p,g.]) by RFUNCT_2:17
.= ((f | [.p,g.]) ") .: (rng (f | [.p,g.])) by RELAT_1:115
.= ((f | [.p,g.]) ") .: (dom ((f | [.p,g.]) ")) by FUNCT_1:33
.= rng ((f | [.p,g.]) ") by RELAT_1:113
.= dom (f | [.p,g.]) by FUNCT_1:33
.= (dom f) /\ [.p,g.] by RELAT_1:61
.= [.p,g.] by A2, XBOOLE_1:28 ;
hence (f ") | [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] is continuous by A1, A4, FCONT_1:46; ::_thesis: verum
end;
suppose f | [.p,g.] is decreasing ; ::_thesis: (f ") | [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] is continuous
then ((f | [.p,g.]) ") | (f .: [.p,g.]) is decreasing by RFUNCT_2:52;
then ((f ") | (f .: [.p,g.])) | (f .: [.p,g.]) is decreasing by RFUNCT_2:17;
then (f ") | (f .: [.p,g.]) is monotone by RELAT_1:72;
then A5: (f ") | [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] is monotone by A1, A2, A3, Th19;
(f ") .: [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] = (f ") .: (f .: [.p,g.]) by A1, A2, A3, Th19
.= ((f ") | (f .: [.p,g.])) .: (f .: [.p,g.]) by RELAT_1:129
.= ((f | [.p,g.]) ") .: (f .: [.p,g.]) by RFUNCT_2:17
.= ((f | [.p,g.]) ") .: (rng (f | [.p,g.])) by RELAT_1:115
.= ((f | [.p,g.]) ") .: (dom ((f | [.p,g.]) ")) by FUNCT_1:33
.= rng ((f | [.p,g.]) ") by RELAT_1:113
.= dom (f | [.p,g.]) by FUNCT_1:33
.= (dom f) /\ [.p,g.] by RELAT_1:61
.= [.p,g.] by A2, XBOOLE_1:28 ;
hence (f ") | [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] is continuous by A1, A5, FCONT_1:46; ::_thesis: verum
end;
end;
end;
hence (f ") | [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] is continuous ; ::_thesis: verum
end;