:: Real Function Uniform Continuity
:: by Jaros{\l}aw Kotowicz and Konrad Raczkowski
::
:: Received June 18, 1990
:: Copyright (c) 1990-2021 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 00;
then
A10: 0<|.p.| by COMPLEX1:47;
A11: 0 <> |.p.| by A9,COMPLEX1:47;
now
let r;
assume 0 {} & 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~~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: n0 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 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~~~~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: n0 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 {} 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.pp 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.gf.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.x1x1;
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.px1;
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 {} 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 x1p;
then pg;
then x2p;
then p=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;
~~