:: Real Function Uniform Continuity
:: by Jaros{\l}aw Kotowicz and Konrad Raczkowski
::
:: Received June 18, 1990
:: Copyright (c) 1990-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, REAL_1, SEQ_1, PARTFUN1, CARD_1, ARYTM_3,
RELAT_1, COMPLEX1, ARYTM_1, FUNCT_1, TARSKI, XBOOLE_0, XXREAL_0,
VALUED_1, XXREAL_2, ORDINAL2, FCONT_1, RCOMP_1, VALUED_0, SEQ_2, FUNCT_2,
NAT_1, SEQ_4, XXREAL_1, FUNCOP_1, ORDINAL4, SEQM_3, FCONT_2;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, FUNCOP_1, NUMBERS, XXREAL_0,
XREAL_0, XXREAL_2, VALUED_0, XCMPLX_0, COMPLEX1, REAL_1, NAT_1, FUNCT_1,
RELSET_1, PARTFUN1, FUNCT_2, VALUED_1, SEQ_1, COMSEQ_2, SEQ_2, SEQ_4,
PARTFUN2, RFUNCT_1, RFUNCT_2, RCOMP_1, FCONT_1, RECDEF_1;
constructors PARTFUN1, REAL_1, SQUARE_1, NAT_1, COMPLEX1, VALUED_1, SEQ_2,
SEQM_3, SEQ_4, RCOMP_1, PARTFUN2, RFUNCT_1, RFUNCT_2, FCONT_1, RECDEF_1,
XXREAL_2, RELSET_1, BINOP_2, COMSEQ_2;
registrations XBOOLE_0, RELSET_1, NUMBERS, XREAL_0, NAT_1, MEMBERED, RFUNCT_2,
VALUED_0, VALUED_1, FUNCT_2, ORDINAL1, XXREAL_2, FCONT_1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities VALUED_1;
theorems TARSKI, SUBSET_1, NAT_1, FUNCT_1, ABSVALUE, SEQ_2, SEQ_4, PARTFUN2,
RFUNCT_1, RFUNCT_2, RCOMP_1, FCONT_1, RELAT_1, FUNCT_2, XREAL_0,
XBOOLE_0, XBOOLE_1, XCMPLX_0, XCMPLX_1, FUNCOP_1, XREAL_1, COMPLEX1,
XXREAL_0, ORDINAL1, VALUED_1, XXREAL_2, XXREAL_1, VALUED_0, RELSET_1;
schemes NAT_1, SEQ_1, FUNCT_2;
begin
reserve n,m for Element of NAT;
reserve x, X,X1,Z,Z1 for set;
reserve s,g,r,t,p,x0,x1,x2 for Real;
reserve s1,s2,q1 for Real_Sequence;
reserve Y for Subset of REAL;
reserve f,f1,f2 for PartFunc of REAL,REAL;
definition
let f;
attr f is uniformly_continuous means
for r st 0<r ex s st 0<s &
for x1,x2 st x1 in dom f & x2 in dom f & |.x1-x2.| < s
holds |.f.x1-f.x2.| < r;
end;
theorem Th1:
f|X is uniformly_continuous iff
for r st 0<r
ex s st 0<s &
for x1,x2 st x1 in dom(f|X) & x2 in dom(f|X) & |.x1-x2.| < s
holds |.f.x1-f.x2.| < r
proof
thus f|X is uniformly_continuous implies for r st 0<r ex s st 0<s & for x1,
x2 st x1 in dom(f|X) & x2 in dom(f|X) & |.x1-x2.| < s holds |.f.x1-f.x2.|
< r
proof
assume
A1: f|X is uniformly_continuous;
let r;
assume 0<r;
then consider s such that
A2: 0<s and
A3: for x1,x2 st x1 in dom(f|X) & x2 in dom (f|X) & |.x1-x2.| < s
holds |.(f|X).x1 - (f|X).x2.| < r by A1;
take s;
thus 0<s by A2;
let x1,x2;
assume that
A4: x1 in dom(f|X) and
A5: x2 in dom(f|X);
A6: (f|X).x2 = f.x2 by A5,FUNCT_1:47;
(f|X).x1 = f.x1 by A4,FUNCT_1:47;
hence thesis by A3,A4,A5,A6;
end;
assume
A7: for r st 0<r ex s st 0<s & for x1,x2 st x1 in dom(f|X) & x2 in dom(f
|X) & |.x1-x2.| < s holds |.f.x1-f.x2.| < r;
let r;
assume 0<r;
then consider s such that
A8: 0<s and
A9: for x1,x2 st x1 in dom(f|X) & x2 in dom(f|X) & |.x1-x2.| < s
holds |.f.x1-f.x2.| < r by A7;
take s;
thus 0<s by A8;
let x1,x2;
assume that
A10: x1 in dom(f|X) and
A11: x2 in dom(f|X);
A12: (f|X).x2 = f.x2 by A11,FUNCT_1:47;
(f|X).x1 = f.x1 by A10,FUNCT_1:47;
hence thesis by A9,A10,A11,A12;
end;
theorem Th2:
f|X is uniformly_continuous & X1 c= X implies f|X1 is uniformly_continuous
proof
assume that
A1: f|X is uniformly_continuous and
A2: X1 c= X;
now
let r;
assume 0<r;
then consider s such that
A3: 0<s and
A4: for x1,x2 st x1 in dom(f|X) & x2 in dom(f|X) & |.x1-x2.|<s holds
|.f.x1-f.x2.|<r by A1,Th1;
take s;
thus 0<s by A3;
let x1,x2;
assume that
A5: x1 in dom(f|X1) and
A6: x2 in dom(f|X1) and
A7: |.x1-x2.|<s;
f|X1 c= f|X by A2,RELAT_1:75;
then dom(f|X1) c= dom(f|X) by RELAT_1:11;
hence |.f.x1-f.x2.|<r by A4,A5,A6,A7;
end;
hence thesis by Th1;
end;
theorem
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
proof
assume that
A1: X c= dom f1 and
A2: X1 c= dom f2;
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;
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
let r;
A9: dom(f1+f2) = dom f1 /\ dom f2 by VALUED_1:def 1;
assume 0<r;
then
A10: 0<r/2 by XREAL_1:215;
then consider s such that
A11: 0<s and
A12: for x1,x2 st x1 in dom(f1|(X/\X1)) & x2 in dom(f1|(X/\X1)) &
|.x1 -x2.|<s holds |.f1.x1-f1.x2.|<r/2 by A8,Th1;
consider g such that
A13: 0<g and
A14: for x1,x2 st x1 in dom(f2|(X/\X1)) & x2 in dom(f2|(X/\X1)) &
|.x1 -x2.|<g holds |.f2.x1-f2.x2.|<r/2 by A7,A10,Th1;
take p=min(s,g);
thus 0<p by A11,A13,XXREAL_0:15;
let x1,x2;
assume that
A15: x1 in dom((f1+f2)|(X/\X1)) and
A16: x2 in dom((f1+f2)|(X/\X1)) and
A17: |.x1-x2.|<p;
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: |.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: |.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: |.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 |.f1.x1-f1.x2.|<r/2 by A12,A24,A23;
then
A27: |.f1.x1-f1.x2.|+|.f2.x1-f2.x2.|<r/2+r/2 by A26,XREAL_1:8;
A28: |.f1.x1 - f1.x2 + (f2.x1-f2.x2).| <= |.f1.x1-f1.x2.| + |.f2.x1-f2
.x2.| by COMPLEX1:56;
|.(f1+f2).x1-(f1+f2).x2.| = |.f1.x1 + f2.x1-(f1+f2).x2.| by A4,A22,
VALUED_1:def 1
.= |.f1.x1 + f2.x1 - (f1.x2+f2.x2).| by A4,A18,VALUED_1:def 1
.= |.f1.x1 - f1.x2 + (f2.x1-f2.x2).|;
hence |.(f1+f2).x1 - (f1+f2).x2.| < r by A27,A28,XXREAL_0:2;
end;
hence thesis by Th1;
end;
theorem
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
proof
assume that
A1: X c= dom f1 and
A2: X1 c= dom f2;
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;
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
let r;
A9: dom(f1-f2) = dom f1 /\ dom f2 by VALUED_1:12;
assume 0<r;
then
A10: 0<r/2 by XREAL_1:215;
then consider s such that
A11: 0<s and
A12: for x1,x2 st x1 in dom(f1|(X /\ X1)) & x2 in dom(f1|(X /\ X1)) &
|.x1-x2.|<s holds |.f1.x1-f1.x2.|<r/2 by A8,Th1;
consider g such that
A13: 0<g and
A14: for x1,x2 st x1 in dom(f2|(X /\ X1)) & x2 in dom(f2|(X /\ X1)) &
|.x1-x2.|<g holds |.f2.x1-f2.x2.|<r/2 by A7,A10,Th1;
take p=min(s,g);
thus 0<p by A11,A13,XXREAL_0:15;
let x1,x2;
assume that
A15: x1 in dom((f1-f2)|(X/\X1)) and
A16: x2 in dom((f1-f2)|(X/\X1)) and
A17: |.x1-x2.|<p;
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: |.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: |.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: |.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 |.f1.x1-f1.x2.|<r/2 by A12,A24,A23;
then
A27: |.f1.x1-f1.x2.|+|.f2.x1-f2.x2.|<r/2+r/2 by A26,XREAL_1:8;
A28: |.f1.x1 - f1.x2 - (f2.x1-f2.x2).| <= |.f1.x1-f1.x2.| + |.f2.x1-f2
.x2.| by COMPLEX1:57;
|.(f1-f2).x1-(f1-f2).x2.| = |.f1.x1 - f2.x1-(f1-f2).x2.| by A4,A22,
VALUED_1:13
.= |.f1.x1 - f2.x1 - (f1.x2-f2.x2).| by A4,A18,VALUED_1:13
.= |.f1.x1 - f1.x2 - (f2.x1-f2.x2).|;
hence |.(f1-f2).x1 - (f1-f2).x2.| < r by A27,A28,XXREAL_0:2;
end;
hence thesis by Th1;
end;
theorem Th5:
X c= dom f & f|X is uniformly_continuous implies (p(#)f)|X is
uniformly_continuous
proof
assume X c= dom f;
then
A1: X c= dom (p(#)f) by VALUED_1:def 5;
assume
A2: f|X is uniformly_continuous;
per cases;
suppose
A3: p=0;
now
let r;
assume
A4: 0<r;
then consider s such that
A5: 0<s and
for x1,x2 st x1 in dom(f|X) & x2 in dom(f|X) & |.x1-x2.|<s holds
|.f.x1-f.x2.|<r by A2,Th1;
take s;
thus 0<s by A5;
let x1,x2;
assume that
A6: x1 in dom((p(#)f)|X) and
A7: x2 in dom((p(#)f)|X) and
|.x1-x2.|<s;
A8: x2 in X by A7,RELAT_1:57;
x1 in X by A6,RELAT_1:57;
then |.(p(#)f).x1-(p(#)f).x2.| = |.p*(f.x1)-(p(#)f).x2.| by A1,
VALUED_1:def 5
.= |.0 - p*(f.x2).| by A1,A3,A8,VALUED_1:def 5
.= 0 by A3,ABSVALUE:2;
hence |.(p(#)f).x1-(p(#)f).x2.| <r by A4;
end;
hence thesis by Th1;
end;
suppose
A9: p<>0;
then
A10: 0<|.p.| by COMPLEX1:47;
A11: 0 <> |.p.| by A9,COMPLEX1:47;
now
let r;
assume 0<r;
then 0 < r/|.p.| by A10,XREAL_1:139;
then consider s such that
A12: 0<s and
A13: for x1,x2 st x1 in dom(f|X) & x2 in dom(f|X) & |.x1-x2.|<s
holds |.f.x1-f.x2.|<r/|.p.| by A2,Th1;
take s;
thus 0<s by A12;
let x1,x2;
assume that
A14: x1 in dom((p(#)f)|X) and
A15: x2 in dom((p(#)f)|X) and
A16: |.x1-x2.|<s;
A17: x2 in X by A15,RELAT_1:57;
A18: x1 in X by A14,RELAT_1:57;
then
A19: |.(p(#)f).x1-(p(#)f).x2.| = |.p*(f.x1)-(p(#)f).x2.| by A1,
VALUED_1:def 5
.= |.p*(f.x1) - p*(f.x2).| by A1,A17,VALUED_1:def 5
.= |.p*(f.x1 - f.x2).|
.= |.p.|*|.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 |.p.|*|.f.x1-f.x2.|<r/|.p.|*|.p.| by A10,A13,A16,A20,XREAL_1:68;
hence |.(p(#)f).x1-(p(#)f).x2.| <r by A11,A19,XCMPLX_1:87;
end;
hence thesis by Th1;
end;
end;
theorem
X c= dom f & f|X is uniformly_continuous implies (-f)|X is
uniformly_continuous
by Th5;
theorem
f|X is uniformly_continuous implies (abs f)|X is uniformly_continuous
proof
assume
A1: f|X is uniformly_continuous;
now
let r;
assume 0<r;
then consider s such that
A2: 0<s and
A3: for x1,x2 st x1 in dom(f|X) & x2 in dom(f|X) & |.x1-x2.|<s holds
|.f.x1-f.x2.|<r by A1,Th1;
take s;
thus 0<s by A2;
let x1,x2;
assume that
A4: x1 in dom((abs f)|X) and
A5: x2 in dom((abs f)|X) and
A6: |.x1-x2.|<s;
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(f)).x1-(abs(f)).x2.| = |.|.f.x1.|-(abs(f)).x2.| by VALUED_1:18
.= |.|.f.x1.|-|.f.x2.|.| by VALUED_1:18;
then
A9: |.(abs(f)).x1-(abs(f)).x2.| <= |.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 |.f.x1-f.x2.|<r by A3,A6,A8;
hence |.(abs f).x1 - (abs f).x2.| < r by A9,XXREAL_0:2;
end;
hence thesis by Th1;
end;
theorem
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
proof
assume that
A1: X c= dom f1 and
A2: X1 c= dom f2;
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;
consider x1 be Real such that
A7: for r being object st r in Z /\ dom f1 holds |.f1.r.|<=x1
by A5,RFUNCT_1:73;
consider x2 be Real such that
A8: for r being object st r in Z1 /\ dom f2 holds |.f2.r.|<=x2
by A6,RFUNCT_1:73;
reconsider x1, x2 as Real;
set M1=|.x1.|+1;
set M2=|.x2.|+1;
set M=max(M1,M2);
A9: now
let r;
A10: M1 <= M by XXREAL_0:25;
assume r in X /\ Z /\ X1 /\ Z1;
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: |.f1.r.|<=x1 by A7;
x1+0 < M1 by ABSVALUE:4,XREAL_1:8;
then |.f1.r.| < M1 by A14,XXREAL_0:2;
hence |.f1.r.| < M by A10,XXREAL_0:2;
A15: M2 <= M 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: |.f2.r.|<=x2 by A8;
x2+0 < M2 by ABSVALUE:4,XREAL_1:8;
then |.f2.r.| < M2 by A18,XXREAL_0:2;
hence |.f2.r.| < M by A15,XXREAL_0:2;
end;
A19: 0+0 < |.x2.|+1 by COMPLEX1:46,XREAL_1:8;
0+0 < |.x1.|+1 by COMPLEX1:46,XREAL_1:8;
then
A20: 0 < M by A19,XXREAL_0:16;
then
A21: 0<2*M by XREAL_1:129;
for r st 0<r ex s st 0<s & for x1,x2 st x1 in dom((f1(#)f2)|(X/\Z/\X1/\
Z1)) & x2 in dom((f1(#)f2)|(X/\Z/\X1/\Z1)) & |.x1-x2.| < s holds |.(f1(#)
f2).x1 - (f1(#)f2).x2.| < r
proof
let r;
assume 0<r;
then
A22: 0<r/(2*M) by A21,XREAL_1:139;
then consider s such that
A23: 0<s and
A24: for x1,x2 st x1 in dom(f1|X) & x2 in dom(f1|X) & |.x1-x2.|<s
holds |.f1.x1-f1.x2.|<r/(2*M) by A3,Th1;
consider g such that
A25: 0<g and
A26: for x1,x2 st x1 in dom(f2|X1) & x2 in dom(f2|X1) & |.x1-x2.|<g
holds |.f2.x1-f2.x2.|<r/(2*M) by A4,A22,Th1;
take p=min(s,g);
thus 0<p by A23,A25,XXREAL_0:15;
let y1,y2 be Real;
assume that
A27: y1 in dom((f1(#)f2)|(X/\Z/\X1/\Z1)) and
A28: y2 in dom((f1(#)f2)|(X/\Z/\X1/\Z1));
assume
A29: |.y1-y2.|<p;
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 |.y1-y2.|<g by A29,XXREAL_0:2;
then
A38: |.f2.y1-f2.y2.|<r/(2*M) by A26,A37,A36;
|.(f1(#)f2).y1-(f1(#)f2).y2.| = |.(f1.y1)*(f2.y1) - (f1(#) f2).y2.|
by VALUED_1:5
.= |.(f1.y1)*(f2.y1)+((f1.y1)*(f2.y2)-(f1.y1)*(f2.y2))-(f1.y2)*(f2.
y2).| by VALUED_1:5
.= |.(f1.y1)*((f2.y1)-(f2.y2))+((f1.y1)-(f1.y2))*(f2.y2).|;
then
A39: |.(f1(#)f2).y1-(f1(#)f2).y2.|<=|.(f1.y1)*((f2.y1)-(f2.y2)).| +
|.((f1.y1)-(f1.y2))*(f2.y2).| by COMPLEX1:56;
A40: |.(f1.y1)*((f2.y1)-(f2.y2)).|=|.f1.y1.|*|.f2.y1-f2.y2.| by
COMPLEX1:65;
A41: |.f2.y2.| < M by A9,A30;
A42: 0 <= |.f2.y2.| by COMPLEX1:46;
A43: 0 <= |.f1.y1-f1.y2.| by COMPLEX1:46;
A44: |.((f1.y1)-(f1.y2))*(f2.y2).|=|.f2.y2.|*|.(f1.y1)-(f1.y2).| by
COMPLEX1:65;
p<=s by XXREAL_0:17;
then |.y1-y2.|<s by A29,XXREAL_0:2;
then |.f1.y1-f1.y2.|<r/(2*M) by A24,A35,A32;
then
A45: |.((f1.y1)-(f1.y2))*(f2.y2).| < M*(r/(2*M)) by A44,A41,A43,A42,XREAL_1:96;
A46: 0 <= |.f1.y1.| by COMPLEX1:46;
A47: 0 <= |.f2.y1-f2.y2.| by COMPLEX1:46;
|.f1.y1.| < M by A9,A33;
then |.(f1.y1)*((f2.y1)-(f2.y2)).| < M*(r/(2*M)) by A40,A38,A47,A46,
XREAL_1:96;
then
A48: |.(f1.y1)*((f2.y1)-(f2.y2)).|+|.((f1.y1)-(f1.y2))*(f2.y2).|< M*(r/(
2*M))+M*(r/(2*M)) by A45,XREAL_1:8;
M*(r/(2*M))+M*(r/(2*M)) = M*(r/(M*2)+r/(M*2)) .= r/M*M by XCMPLX_1:118
.= r by A20,XCMPLX_1:87;
hence thesis by A39,A48,XXREAL_0:2;
end;
hence thesis by Th1;
end;
theorem Th9:
X c= dom f & f|X is uniformly_continuous implies f|X is continuous
proof
assume
A1: X c= dom f;
assume
A2: f|X is uniformly_continuous;
now
let x0,r be Real;
assume that
A3: x0 in X and
A4: 0<r;
A5: x0 in dom(f|X) by A1,A3,RELAT_1:62;
consider s such that
A6: 0<s and
A7: for x1,x2 st x1 in dom(f|X) & x2 in dom(f|X) & |.x1-x2.| < s
holds |.f.x1-f.x2.| < r by A2,A4,Th1;
reconsider s as Real;
take s;
thus 0<s by A6;
let x1 be Real;
assume that
A8: x1 in X and
A9: |.x1-x0.| < s;
x1 in dom(f|X) by A1,A8,RELAT_1:62;
hence |.f.x1 - f.x0.| < r by A7,A9,A5;
end;
hence thesis by A1,FCONT_1:14;
end;
theorem Th10:
f|X is Lipschitzian implies f|X is uniformly_continuous
proof
assume f|X is Lipschitzian;
then consider r be Real such that
A1: 0<r and
A2: for x1,x2 be Real st x1 in dom(f|X) & x2 in dom(f|X) holds
|.f.x1-f.x2.|<=r*|.x1-x2.| by FCONT_1:32;
for r st 0<r
ex s st 0<s &
for x1,x2 st x1 in dom(f|X) & x2 in dom(f|X) & |.x1-x2.| < s
holds |.f.x1-f.x2.| < r
proof
:: now dlaczego nie akceptuje Diffuse Statement !!! A.T.
let p such that
A3: 0<p;
take s=p/r;
thus 0<s by A1,A3,XREAL_1:139;
let x1,x2;
assume that
A4: x1 in dom(f|X) and
A5: x2 in dom(f|X) and
A6: |.x1-x2.| < s;
A7: r*|.x1-x2.| < s*r by A1,A6,XREAL_1:68;
|.f.x1-f.x2.|<=r*|.x1-x2.| by A2,A4,A5;
then |.f.x1-f.x2.|<p/r*r by A7,XXREAL_0:2;
hence |.f.x1-f.x2.| < p by A1,XCMPLX_1:87;
end;
hence thesis by Th1;
end;
theorem Th11:
for f,Y st Y c= dom f & Y is compact & f|Y is continuous holds f
|Y is uniformly_continuous
proof
let f,Y such that
A1: Y c= dom f and
A2: Y is compact and
A3: f|Y is continuous;
assume not thesis;
then consider r such that
A4: 0<r and
A5: for s st 0<s ex x1,x2 st x1 in dom(f|Y) & x2 in dom(f|Y) & |.x1 -
x2.| < s & not |.f.x1-f.x2.| < r by Th1;
defpred P[Element of NAT,Real]
means $2 in Y & ex x2 being Element of REAL st x2 in Y & |.$2-x2.|
<1/($1+1) & not |.f.($2)-f.x2.| < r;
A6: now
let n;
consider x1 such that
A7: ex x2 st x1 in dom(f|Y) & x2 in dom(f|Y) & |.x1-x2.| < 1/(n+1)
& not |.f.x1-f.x2.| < r by A5,XREAL_1:139;
reconsider x1 as Element of REAL by XREAL_0:def 1;
take x1;
dom(f|Y) = Y by A1,RELAT_1:62;
hence P[n,x1] by A7;
end;
consider s1 such that
A8: for n holds P[n,s1.n] from FUNCT_2:sch 3(A6);
now
let x be object;
assume x in rng s1;
then ex n st x=s1.n by FUNCT_2:113;
hence x in Y by A8;
end;
then
A9: rng s1 c= Y by TARSKI:def 3;
then consider q1 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 P[Element of NAT,Real] means $2 in Y & |.s1.$1-$2.| < 1/($1+
1) & not |.f.(s1.$1)-f.$2.| < r;
A18: for n ex x2 being Element of REAL st P[n,x2] by A8;
consider s2 such that
A19: for n holds P[n,s2.n] from FUNCT_2:sch 3(A18);
now
let x be object;
assume x in rng s2;
then ex n st x=s2.n by FUNCT_2:113;
hence x in Y by A19;
end;
then
A20: rng s2 c= Y by TARSKI:def 3;
consider Ns1 be increasing sequence of NAT such that
A21: q1=s1*Ns1 by A10,VALUED_0:def 17;
set q2 = q1 - (s1-s2)*Ns1;
A22: now
let n;
thus q2.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;
end;
then
A23: q2 = s2*Ns1 by FUNCT_2:63;
q2 is subsequence of s2 by A22,FUNCT_2:63,VALUED_0:def 17;
then rng q2 c= rng s2 by VALUED_0:21;
then
A24: rng q2 c= Y by A20,XBOOLE_1:1;
then rng q2 c= dom f by A1,XBOOLE_1:1;
then rng q2 c= dom f /\ Y by A24,XBOOLE_1:19;
then
A25: rng q2 c= dom (f|Y) by RELAT_1:61;
A26: now
let p be Real such that
A27: 0<p;
consider k be Nat such that
A28: p" < k by SEQ_4:3;
take k;
let m be Nat;
A29: m in NAT by ORDINAL1:def 12;
assume k <= m;
then k+1 <= m+1 by XREAL_1:6;
then 1/(m+1) <= 1/(k+1) by XREAL_1:118;
then
A30: |.s1.m-s2.m.| < 1/(k+1) by A19,XXREAL_0:2,A29;
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
A31: 1/(k+1) < p by XCMPLX_1:216;
|.(s1-s2).m - 0.| = |.s1.m-s2.m.| by RFUNCT_2:1;
hence |.(s1-s2).m - 0.| < p by A31,A30,XXREAL_0:2;
end;
then
A32: s1-s2 is convergent by SEQ_2:def 6;
A33: (s1-s2)*Ns1 is subsequence of s1-s2 by VALUED_0:def 17;
then
A34: (s1-s2)*Ns1 is convergent by A32,SEQ_4:16;
lim (s1-s2) = 0 by A26,A32,SEQ_2:def 7;
then lim ((s1-s2)*Ns1) = 0 by A32,A33,SEQ_4:17;
then
A35: lim q2 = lim q1 - 0 by A11,A34,SEQ_2:12
.= lim q1;
A36: q2 is convergent by A11,A34,SEQ_2:11;
then
A37: (f|Y)/*q2 is convergent by A13,A35,A25,FCONT_1:def 1;
then
A38: (f|Y)/*q1 - (f|Y)/*q2 is convergent by A17,SEQ_2:11;
(f|Y).(lim q1) = lim ((f|Y)/*q2) by A13,A36,A35,A25,FCONT_1:def 1;
then
A39: lim ((f|Y)/*q1 - (f|Y)/*q2) = (f|Y).(lim q1) - (f|Y).(lim q1) by A17,A16
,A37,SEQ_2:12
.= 0;
now
let n;
consider k be Nat such that
A40: for m being Nat st k<=m holds |.((f|Y)/*q1 - (f|Y)/*q2).m-0.|<r
by A4,A38,A39,
SEQ_2:def 7;
A41: q1.k in rng q1 by VALUED_0:28;
A42: q2.k in rng q2 by VALUED_0:28;
A43: k in NAT by ORDINAL1:def 12;
|.((f|Y)/*q1 - (f|Y)/*q2).k - 0.| = |.((f|Y)/*q1).k - ((f|Y)/*q2).
k.| by RFUNCT_2:1
.= |.(f|Y).(q1.k) - ((f|Y)/*q2).k.| by A15,FUNCT_2:108,A43
.= |.(f|Y).(q1.k) - (f|Y).(q2.k).| by A25,FUNCT_2:108,A43
.= |.f.(q1.k) - (f|Y).(q2.k).| by A15,A41,FUNCT_1:47
.= |.f.(q1.k) - f.(q2.k).| by A25,A42,FUNCT_1:47
.= |.f.(s1.(Ns1.k)) - f.((s2*Ns1).k).| by A21,A23,FUNCT_2:15,A43
.= |.f.(s1.(Ns1.k)) - f.(s2.(Ns1.k)).| by FUNCT_2:15,A43;
hence contradiction by A19,A40;
end;
hence contradiction;
end;
theorem
Y c= dom f & Y is compact & f|Y is uniformly_continuous implies f.:Y
is compact by Th9,FCONT_1:29;
theorem
for f,Y st Y <> {} & Y c= dom f & Y is compact & f|Y is
uniformly_continuous ex x1,x2 st x1 in Y & x2 in Y & f.x1 = upper_bound (f.:Y)
& f.x2 = lower_bound (f.:Y)
by Th9,FCONT_1:31;
theorem
X c= dom f & f|X is constant implies f|X is uniformly_continuous by Th10;
theorem Th15:
p<= g & [.p,g.] c= dom f & f|[.p,g.] is continuous implies for r
st r in [.f.p,f.g.] \/ [.f.g,f.p.] ex s st s in [.p,g.] & r = f.s
proof
assume that
A1: p<=g and
A2: [.p,g.] c= dom f and
A3: f|[.p,g.] is continuous;
let r such that
A4: r in [.f.p,f.g.] \/ [.f.g,f.p.];
A5: [.p,g.] is compact by RCOMP_1:6;
A6: f.p < f.g implies ex s st s in [.p,g.] & r = f.s
proof
r in REAL by XREAL_0:def 1;
then 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 st s in [.p,g.] holds r <> f.s;
[.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: f.p<=s & s<= f.g} by A4,RCOMP_1:def 1;
then
A9: ex s st s=r & f.p<=s & s<=f.g;
p in [.p,g.] by A1,XXREAL_1:1;
then
A10: r<> f.p by A8;
reconsider f1 as PartFunc of REAL, REAL by RELSET_1:7;
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} <> {};
then consider x2 being Element of 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 |.(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;
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;
reconsider r as Element of REAL by XREAL_0:def 1;
for x0 being Element of REAL st x0 in [.p,g.] /\ dom f1 holds f1.x0=r
by A11,FUNCOP_1:7;
then f1|[.p,g.] is constant 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 such that
A19: M is UpperBound of (abs(f1-f)^).:[.p,g.] by XXREAL_2:def 10;
A20: for x1 be Real st x1 in (abs(f1-f)^).:[.p,g.] holds x1<=M
by A19,XXREAL_2:def 1;
0+0<|.M.|+1 by COMPLEX1:46,XREAL_1:8;
then 0<(|.M.|+1)";
then
A21: 0<1/(|.M.|+1) by XCMPLX_1:215;
f|[.p,g.] is uniformly_continuous by A2,A3,Th11,RCOMP_1:6;
then consider s such that
A22: 0<s and
A23: for x1,x2 st x1 in dom(f|[.p,g.]) & x2 in dom(f|[.p,g .]) &
|.x1 - x2.| < s holds |.f.x1-f.x2.| < 1/(|.M.|+1) by A21,Th1;
A24: now
let x1;
assume
A25: x1 in [.p,g.];
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: |.(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 |.f1.x1-f.x1.|" <= M by A26,VALUED_1:13;
then
A27: |.r-f.x1.|" <= M by A25,FUNCOP_1:7;
r-f.x1<>0 by A8,A25;
then
A28: 0<|.r-f.x1.| by COMPLEX1:47;
M+0<|.M.|+1 by ABSVALUE:4,XREAL_1:8;
then |.r-f.x1.|" < |.M.|+1 by A27,XXREAL_0:2;
then 1/(|.M.|+1)<1/|.r-f.x1.|" by A28,XREAL_1:76;
hence 1/(|.M.|+1)<|.r-f.x1.| by XCMPLX_1:216;
end;
now
per cases;
suppose
p=g;
hence contradiction by A7;
end;
suppose
p<>g;
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 be 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 F(Nat) = p + (g-p)/k*$1;
consider s1 such that
A33: for n being Nat holds s1.n = F(n) from SEQ_1:sch 1;
A34: 0<(g-p)/k by A29,A31,A30,XREAL_1:139;
A35: now
let n;
A36: dom(f|[.p,g.]) = [.p,g.] by A2,RELAT_1:62;
assume
A37: n<k;
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: p<=x2 & x2<=g} by A38;
hence
A40: s1.n in [.p,g.] by RCOMP_1:def 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: p<=x2 & x2<= g} by A39;
hence
A41: s1.(n+1) in [.p,g.] by RCOMP_1:def 1;
|.s1.(n+1) -s1.n.| = |.p + (g-p)/k*(n+1) - s1.n.| by A33
.= |.p + (g-p)/k*(n+1) - (p + (g-p)/k*n).| by A33
.= (g-p)/k by A29,ABSVALUE:def 1;
hence |.f.(s1.(n+1)) - f.(s1.n).| < 1/(|.M.|+1) by A23,A32,A40,A41
,A36;
end;
defpred P[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 be Nat st P[n] by A9;
consider l be Nat such that
A44: P[l] & for m be Nat st P[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 be Nat such that
A45: l=l1+1 by NAT_1:6;
reconsider 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: |.f.(s1.(l1+1)) - f.(s1.l1).| < 1/(|.M.|+1) by A35;
f.(s1.l1) < r
proof
assume r <= f.(s1.l1);
then l <= l1 by A44;
then l+0 < l by A45,XREAL_1:8;
hence contradiction;
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 |.f.(s1.(l1+1)) - f.(s1.l1).| = f.(s1.(l1+1)) - f.(s1.l1) by
ABSVALUE:def 1;
then
A50: |.r - f.(s1.l1).| <= |.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;
end;
end;
hence contradiction;
end;
A51: f.g < f.p implies ex s st s in [.p,g.] & r = f.s
proof
r in REAL by XREAL_0:def 1;
then 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 st s in [.p,g.] holds r <> f.s;
[.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: f.g<=s & s<=f.p} by A4,RCOMP_1:def 1;
then
A54: ex s st s=r & f.g<=s & s<=f.p;
g in {s: 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 as PartFunc of REAL, REAL by RELSET_1:7;
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} <> {};
then consider x2 being Element of 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 |.(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;
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;
reconsider r as Element of REAL by XREAL_0:def 1;
for x0 being Element of REAL st x0 in [.p,g.] /\ dom f1 holds f1.x0=r
by A56,FUNCOP_1:7;
then f1|[.p,g.] is constant 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 such that
A64: M is UpperBound of (abs(f1-f)^).:[.p,g.] by XXREAL_2:def 10;
A65: for x1 be Real st x1 in (abs(f1-f)^).:[.p,g.] holds x1<=M
by A64,XXREAL_2:def 1;
0+0<|.M.|+1 by COMPLEX1:46,XREAL_1:8;
then 0<(|.M.|+1)";
then
A66: 0<1/(|.M.|+1) by XCMPLX_1:215;
f|[.p,g.] is uniformly_continuous by A2,A3,Th11,RCOMP_1:6;
then consider s such that
A67: 0<s and
A68: for x1,x2 st x1 in dom(f|[.p,g.]) & x2 in dom(f|[.p,g .]) &
|.x1 - x2.| < s holds |.f.x1-f.x2.| < 1/(|.M.|+1) by A66,Th1;
A69: now
let x1;
assume
A70: x1 in [.p,g.];
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: |.(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 |.f1.x1-f.x1.|" <= M by A71,VALUED_1:13;
then
A72: |.r-f.x1.|" <= M by A70,FUNCOP_1:7;
r-f.x1<>0 by A53,A70;
then
A73: 0<|.r-f.x1.| by COMPLEX1:47;
M+0<|.M.|+1 by ABSVALUE:4,XREAL_1:8;
then |.r-f.x1.|" < |.M.|+1 by A72,XXREAL_0:2;
then 1/(|.M.|+1)<1/|.r-f.x1.|" by A73,XREAL_1:76;
hence 1/(|.M.|+1)<|.r-f.x1.| by XCMPLX_1:216;
end;
now
per cases;
suppose
p=g;
hence contradiction by A52;
end;
suppose
p<>g;
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 be 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 F(Nat) = g - (g-p)/k*$1;
consider s1 such that
A78: for n being Nat holds s1.n = F(n) from SEQ_1:sch 1;
A79: 0<(g-p)/k by A74,A76,A75,XREAL_1:139;
A80: now
let n;
A81: dom(f|[.p,g.]) = [.p,g.] by A2,RELAT_1:62;
assume
A82: n<k;
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: p<=x2 & x2<=g} by A83;
hence
A85: s1.n in [.p,g.] by RCOMP_1:def 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: p<=x2 & x2<=g} by A84;
hence
A86: s1.(n+1) in [.p,g.] by RCOMP_1:def 1;
|.s1.(n+1) -s1.n.| = |.g- (g-p)/k*(n+1) - s1.n.| by A78
.= |.g - (g-p)/k*(n+1) - (g - (g-p)/k*n).| by A78
.= |.-((g-p)/k*(n+1) - (g-p)/k*n).|
.= |.(g-p)/k*(n+1 - n).| by COMPLEX1:52
.= (g-p)/k by A74,ABSVALUE:def 1;
hence |.f.(s1.(n+1)) - f.(s1.n).| < 1/(|.M.|+1) by A68,A77,A85,A86
,A81;
end;
defpred P[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 be Nat st P[n] by A54;
consider l be Nat such that
A89: P[l] & for m be Nat st P[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 be Nat such that
A90: l=l1+1 by NAT_1:6;
reconsider 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: |.f.(s1.(l1+1)) - f.(s1.l1).| < 1/(|.M.|+1) by A80;
f.(s1.l1) < r
proof
assume r <= f.(s1.l1);
then l <= l1 by A89;
then l+0 < l by A90,XREAL_1:8;
hence contradiction;
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 |.f.(s1.(l1+1)) - f.(s1.l1).| = f.(s1.(l1+1)) - f.(s1.l1) by
ABSVALUE:def 1;
then
A95: |.r - f.(s1.l1).| <= |.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;
end;
end;
hence contradiction;
end;
f.p = f.g implies ex s st s in [.p,g.] & r = f.s
proof
assume
A96: f.p = f.g;
take p;
thus p in [.p,g.] by A1,XXREAL_1:1;
[.f.p,f.g.] \/ [.f.g,f.p.] = {f.p} by A96,XXREAL_1:17;
hence thesis by A4,TARSKI:def 1;
end;
hence thesis by A6,A51,XXREAL_0:1;
end;
theorem Th16:
p<=g & [.p,g.] c= dom f & f|[.p,g.] is continuous implies for r
st r in [.(lower_bound (f.:[.p,g.])),(upper_bound (f.:[.p,g.])).] ex s st s in
[.p,g.] & r = f.s
proof
assume that
A1: p<=g and
A2: [.p,g.] c= dom f and
A3: f|[.p,g.] is continuous;
[.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 be Real such that
A5: x2 in [.p,g.] and
A6: x1 in [.p,g.] and
A7: f.x2=ub and
A8: f.x1=lb by A2,A3,FCONT_1:31,RCOMP_1:6;
reconsider x1,x2 as Real;
let r such that
A9: r in [.lb,ub.];
f.x1 in f.:[.p,g.] by A2,A6,FUNCT_1:def 6;
then
A10: [.lb,ub.] = [.lb,ub.] \/ [.ub,lb.] by A4,SEQ_4:11,XXREAL_1:222;
now
per cases;
suppose
A11: x1 <= x2;
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 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;
thus s in [.p,g.] & r=f.s by A13,A14,A15;
end;
suppose
A16: x2 <= x1;
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 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;
thus s in [.p,g.] & r=f.s by A18,A19,A20;
end;
end;
hence thesis;
end;
theorem Th17:
f is one-to-one & [.p,g.] c= dom f & p<=g & f|[.p,g.] is
continuous implies f|[.p,g.] is increasing or f|[.p,g.] is decreasing
proof
A0: p is set by TARSKI:1;
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;
now
per cases;
suppose p=g;
then [.p,g.]={p} by XXREAL_1:17;
hence contradiction by A6,A0,RFUNCT_2:44;
end;
suppose
A7: p<>g;
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
per cases by A10,XXREAL_0:1;
suppose
A11: f.p<f.g;
A12: for x1 st p<=x1 & x1<=g holds f.p<=f.x1 & f.x1<=f.g
proof
let x1;
assume that
A13: p<=x1 and
A14: x1<=g and
A15: not (f.p<=f.x1 & f.x1 <=f.g);
now
per cases by A15;
suppose
A16: f.x1<f.p;
then f.p in {r: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: 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 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: x1<=t & t<=g} by A20,RCOMP_1:def 1;
then
A22: ex r 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;
end;
suppose
A24: f.g<f.x1;
then f.g in {r: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: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 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: p<=t & t<=x1} by A28,RCOMP_1:def 1;
then
A30: ex r 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;
end;
end;
hence contradiction;
end;
consider x1,x2 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: p<=r & r<=g} by RCOMP_1:def 1;
then ex r st r=x2 & p<=r & r<=g;
then f.p <= f.x2 by A12;
then f.x2 in {r: 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:p<=t & t<=g} by A35,RCOMP_1:def 1;
then
A39: ex r 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 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: p<=t & t<=x1} by A41,RCOMP_1:def 1;
then
A43: ex r 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;
end;
suppose
A44: f.p>f.g;
A45: for x1 st p<=x1 & x1<=g holds f.g<=f.x1 & f.x1<=f.p
proof
let x1;
assume that
A46: p<=x1 and
A47: x1<=g and
A48: not (f.g<=f.x1 & f.x1 <=f.p);
now
per cases by A48;
suppose
A49: f.x1<f.g;
now
per cases;
suppose
g=x1;
hence contradiction by A49;
end;
suppose
A50: g<>x1;
x1 in {r: p<=r & r<=g} by A46,A47;
then
A51: x1 in [.p,g.] by RCOMP_1:def 1;
f.g in {r: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 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: p<=t & t<=x1} by A54,RCOMP_1:def 1;
then
A56: ex r 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;
end;
end;
hence contradiction;
end;
suppose
A57: f.p<f.x1;
now
per cases;
suppose
p=x1;
hence contradiction by A57;
end;
suppose
A58: p<>x1;
x1 in {r:p<=r & r<=g} by A46,A47;
then
A59: x1 in [.p,g.] by RCOMP_1:def 1;
f.p in {r: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 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: x1<=t & t<=g} by A62,RCOMP_1:def 1;
then
A64: ex r 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;
end;
end;
hence contradiction;
end;
end;
hence contradiction;
end;
consider x1,x2 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:p<=t & t<=g} by RCOMP_1:def 1;
then ex r st r=x1 & p<=r & r<=g;
then f.g <= f.x1 by A45;
then f.x1 in {r: 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: p<=r & r<=g} by A69,RCOMP_1:def 1;
then
A73: ex r 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 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: x2<=t & t<=g} by A75,RCOMP_1:def 1;
then
A77: ex r 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;
end;
end;
hence contradiction;
end;
end;
hence contradiction;
end;
theorem
f is one-to-one & p<=g & [.p,g.] c= dom f & f|[.p,g.] is continuous
implies 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
proof
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;
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 be Real 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: p<=t & t<=g} by A12,RCOMP_1:def 1;
then
A16: ex r st r=x2 & p<=r & r<=g;
x1 in {r: p<=r & r<=g} by A11,RCOMP_1:def 1;
then
A17: ex r 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
per cases by A1,A2,A3,A4,Th17;
suppose
A20: f|[.p,g.] is increasing;
A21: now
assume x1<>g;
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;
end;
now
assume x2<>p;
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;
end;
hence thesis by A13,A14,A21;
end;
suppose
A22: f|[.p,g.] is decreasing;
A23: now
assume x2<>g;
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;
end;
now
assume x1<>p;
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;
end;
hence thesis by A13,A14,A23;
end;
end;
hence thesis;
end;
::$N Darboux Theorem
theorem Th19:
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.]).]
proof
assume that
A1: p<=g and
A2: [.p,g.] c= dom f and
A3: f|[.p,g.] is continuous;
[.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
let y be Element of REAL;
thus y in f.:[.p,g.] implies y in [.lower_bound(f.:[.p,g.]),upper_bound(f
.:[.p,g.]).]
proof
assume
A5: y in 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: lower_bound(f.:[.p,g.])<=s & s<=upper_bound(f.:[.p,g.])}
by A6;
hence thesis by RCOMP_1:def 1;
end;
assume y in [.lower_bound(f.:[.p,g.]),upper_bound(f.:[.p,g.]).];
then ex x0 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;
end;
hence thesis by SUBSET_1:3;
end;
theorem
for f be 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 f be one-to-one PartFunc of REAL,REAL;
assume that
A1: p<=g and
A2: [.p,g.] c= dom f and
A3: f|[.p,g.] is continuous;
now
per cases by A1,A2,A3,Th17;
suppose
f|[.p,g.] is increasing;
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 thesis by A1,A4,FCONT_1:46;
end;
suppose
f|[.p,g.] is decreasing;
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 thesis by A1,A5,FCONT_1:46;
end;
end;
hence thesis;
end;