Copyright (c) 1991 Association of Mizar Users
environ
vocabulary SEQ_1, PARTFUN1, SUBSET_1, PRE_TOPC, RELAT_1, SEQ_2, ORDINAL2,
BOOLE, LIMFUNC1, FUNCT_1, SEQM_3, PROB_1, ARYTM, RCOMP_1, ARYTM_1,
ABSVALUE, ARYTM_3, FCONT_1, RFUNCT_2, SQUARE_1;
notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
REAL_1, NAT_1, FUNCT_1, SEQ_1, RELSET_1, SEQ_2, SEQM_3, ABSVALUE,
PARTFUN1, SQUARE_1, PARTFUN2, RCOMP_1, RFUNCT_2, FCONT_1, LIMFUNC1;
constructors REAL_1, NAT_1, SEQ_2, SEQM_3, ABSVALUE, PROB_1, PARTFUN1,
PARTFUN2, RCOMP_1, RFUNCT_2, FCONT_1, LIMFUNC1, MEMBERED, XBOOLE_0;
clusters RELSET_1, PARTFUN2, RFUNCT_2, XREAL_0, SEQ_1, ARYTM_3, MEMBERED,
ZFMISC_1, XBOOLE_0, ORDINAL2;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, RCOMP_1, XBOOLE_0;
theorems AXIOMS, REAL_1, FUNCT_1, NAT_1, SEQ_1, SEQ_2, SEQM_3, SEQ_4,
ABSVALUE, SQUARE_1, PARTFUN1, PROB_1, PARTFUN2, RCOMP_1, RFUNCT_2,
FCONT_1, SUBSET_1, REAL_2, LIMFUNC1, FCONT_2, TARSKI, FUNCT_2, RELAT_1,
XREAL_0, XBOOLE_0, XBOOLE_1, XCMPLX_1;
schemes SEQ_1, RCOMP_1;
begin
reserve x,X for set;
reserve x0,r,r1,r2,g,g1,g2,p,s for Real;
reserve n,m for Nat;
reserve a,b,d for Real_Sequence;
reserve f for PartFunc of REAL,REAL;
theorem Th1:
[#] REAL is closed
proof let a such that rng a c= [#] REAL & a is convergent;
lim a in REAL; hence thesis by SUBSET_1:def 4;
end;
theorem
{} REAL is open
proof ({} REAL)` = [#] REAL by SUBSET_1:22;
hence thesis by Th1,RCOMP_1:def 5;
end;
theorem Th3:
{} REAL is closed
proof let a; assume rng a c= {} REAL & a is convergent;
then rng a = {} by XBOOLE_1:3;
then dom a = {} by RELAT_1:65; hence thesis by FUNCT_2:def 1;
end;
theorem Th4:
[#] REAL is open
proof ([#] REAL)` = {} REAL by SUBSET_1:21;
hence thesis by Th3,RCOMP_1:def 5;
end;
theorem Th5:
right_closed_halfline(r) is closed
proof let a such that
A1: rng a c= right_closed_halfline(r) & a is convergent;
deffunc F(Nat) = r;
consider b such that
A2: for n holds b.n = F(n) from ExRealSeq;
now let n;
b.n = r & b.(n+1) = r by A2;
hence b.n = b.(n+1);
end;
then A3: b is constant by SEQM_3:16;
then A4: b is convergent by SEQ_4:39;
A5: lim b = b.0 by A3,SEQ_4:41
.= r by A2;
now let n; a.n in rng a by RFUNCT_2:10;
then a.n in right_closed_halfline(r) by A1;
then a.n in {g: r <= g} by LIMFUNC1:def 2;
then ex r1 st a.n = r1 & r <= r1;
hence b.n <= a.n by A2;
end;
then r <= lim a by A1,A4,A5,SEQ_2:32;
then (lim a) in {g1: r <= g1};
hence thesis by LIMFUNC1:def 2;
end;
theorem Th6:
left_closed_halfline(r) is closed
proof let a such that
A1: rng a c= left_closed_halfline(r) & a is convergent;
deffunc F(Nat) = r;
consider b such that
A2: for n holds b.n = F(n) from ExRealSeq;
now let n;
b.n = r & b.(n+1) = r by A2;
hence b.n = b.(n+1);
end;
then A3: b is constant by SEQM_3:16;
then A4: b is convergent by SEQ_4:39;
A5: lim b = b.0 by A3,SEQ_4:41
.= r by A2;
now let n; a.n in rng a by RFUNCT_2:10;
then a.n in left_closed_halfline(r) by A1;
then a.n in {g: g <= r} by LIMFUNC1:def 1;
then ex r1 st a.n = r1 & r1 <= r;
hence a.n <= b.n by A2;
end;
then lim a <= r by A1,A4,A5,SEQ_2:32;
then (lim a) in {g1: g1 <= r};
hence thesis by LIMFUNC1:def 1;
end;
theorem Th7:
right_open_halfline(r) is open
proof
A1: (right_open_halfline(r))` = REAL \ right_open_halfline(r) by SUBSET_1:def
5
.= left_closed_halfline(r) by LIMFUNC1:24;
left_closed_halfline(r) is closed by Th6;
hence thesis by A1,RCOMP_1:def 5;
end;
theorem Th8:
left_open_halfline(r) is open
proof
A1: (left_open_halfline(r))` = REAL \ left_open_halfline(r) by SUBSET_1:def 5
.= right_closed_halfline(r) by LIMFUNC1:24;
right_closed_halfline(r) is closed by Th5;
hence thesis by A1,RCOMP_1:def 5;
end;
definition let r;
cluster right_open_halfline(r) -> open;
coherence by Th7;
cluster halfline(r) -> open;
coherence by Th8;
end;
definition let p,g be real number;
cluster ].p,g.[ -> open;
coherence by RCOMP_1:25;
end;
theorem Th9:
0 < r & g in ].x0 - r,x0 + r.[ iff ex r1 st g = x0 + r1 & abs(r1) < r
proof
thus 0 < r & g in ].x0 - r,x0 + r.[ implies ex r1 st g = x0 + r1 & abs(r1) <
r
proof assume 0 < r & g in ].x0 - r,x0 + r.[;
then g in {g1: x0 - r < g1 & g1 < x0 + r} by RCOMP_1:def 2;
then A1: ex g1 st g1 = g & x0 - r < g1 & g1 < x0 + r;
take r1 = g - x0;
thus x0 + r1 = g by XCMPLX_1:27;
now per cases;
suppose x0 <= g; then 0 <= g - x0 by SQUARE_1:12;
then A2: abs(g - x0) = g - x0 by ABSVALUE:def 1;
g - x0 < x0 + r - x0 by A1,REAL_1:92;
hence thesis by A2,XCMPLX_1:26;
suppose g <= x0; then 0 <= x0 - g by SQUARE_1:12;
then A3: x0 - g = abs(x0 - g) by ABSVALUE:def 1
.= abs(- (g - x0)) by XCMPLX_1:143
.= abs(g - x0) by ABSVALUE:17;
x0 - g < x0 - (x0 - r) by A1,REAL_1:92;
hence thesis by A3,XCMPLX_1:18;
end;
hence thesis;
end;
given r1 such that
A4: g = x0 + r1 & abs(r1) < r;
thus 0 < r by A4,ABSVALUE:5;
abs(g - x0) < r by A4,XCMPLX_1:26;
hence thesis by RCOMP_1:8;
end;
theorem
0 < r & g in ].x0 - r,x0 + r.[ iff g - x0 in ].-r,r.[
proof
thus 0 < r & g in ].x0 - r,x0 + r.[ implies g - x0 in ].-r,r.[
proof assume 0 < r & g in ].x0 - r,x0 + r.[; then consider r1 such that
A1: g = x0 + r1 & abs(r1) < r by Th9;
A2: g - x0 = r1 by A1,XCMPLX_1:26;
abs(r1 - 0) < r by A1;
then r1 in ].0 - r, 0 + r.[ by RCOMP_1:8;
hence g - x0 in ].-r, r.[ by A2,XCMPLX_1:150;
end;
set r1 = g - x0;
assume r1 in ].-r,r.[;
then r1 in {g1: -r < g1 & g1 < r} by RCOMP_1:def 2;
then ex g1 st g1 = r1 & -r < g1 & g1 < r;
then A3: abs(r1) < r by SEQ_2:9;
x0 + r1 = g by XCMPLX_1:27;
hence thesis by A3,Th9;
end;
theorem Th11:
left_closed_halfline(p) = {p} \/ left_open_halfline(p)
proof
thus left_closed_halfline(p) c= {p} \/ left_open_halfline(p)
proof let x; assume x in left_closed_halfline(p);
then x in {g1: g1 <= p} by LIMFUNC1:def 1;
then consider g1 such that
A1: g1 = x & g1 <= p;
now per cases by A1,AXIOMS:21;
suppose g1 < p; then x in {g2: g2 < p} by A1;
then x in left_open_halfline(p) by PROB_1:def 15;
hence thesis by XBOOLE_0:def 2;
suppose g1 = p; then x in {p} by A1,TARSKI:def 1;
hence thesis by XBOOLE_0:def 2;
end;
hence thesis;
end;
let x such that A2: x in {p} \/ left_open_halfline(p);
now per cases by A2,XBOOLE_0:def 2;
suppose x in {p}; then x = p by TARSKI:def 1; then x in {g: g <= p};
hence thesis by LIMFUNC1:def 1;
suppose
x in left_open_halfline(p); then x in {g: g < p} by PROB_1:def 15;
then consider g1 such that
A3: g1 = x & g1 < p; x in {g2: g2 <= p} by A3;
hence thesis by LIMFUNC1:def 1;
end;
hence thesis;
end;
theorem Th12:
right_closed_halfline(p) = {p} \/ right_open_halfline(p)
proof
thus right_closed_halfline(p) c= {p} \/ right_open_halfline(p)
proof let x; assume x in right_closed_halfline(p);
then x in {g1: p <= g1} by LIMFUNC1:def 2;
then consider g1 such that
A1: g1 = x & p <= g1;
now per cases by A1,AXIOMS:21;
suppose p < g1; then x in {g2: p < g2} by A1;
then x in right_open_halfline(p) by LIMFUNC1:def 3;
hence thesis by XBOOLE_0:def 2;
suppose g1 = p; then x in {p} by A1,TARSKI:def 1;
hence thesis by XBOOLE_0:def 2;
end;
hence thesis;
end;
let x such that A2: x in {p} \/ right_open_halfline(p);
now per cases by A2,XBOOLE_0:def 2;
suppose x in {p}; then x = p by TARSKI:def 1; then x in {g: p <= g};
hence thesis by LIMFUNC1:def 2;
suppose
x in right_open_halfline(p); then x in {g: p < g} by LIMFUNC1:def 3;
then consider g1 such that
A3: g1 = x & p < g1; x in {g2: p <= g2} by A3;
hence thesis by LIMFUNC1:def 2;
end;
hence thesis;
end;
theorem Th13:
for x0 be real number holds
(for n holds a.n = x0 - p/(n+1)) implies a is convergent & lim a = x0
proof
let x0 be real number;
assume
A1: for n holds a.n = x0 - p/(n+1);
deffunc F(Nat) = x0;
consider b such that
A2: for n holds b.n = F(n) from ExRealSeq;
deffunc F(Nat) = p/($1+1);
consider d such that
A3: for n holds d.n = F(n) from ExRealSeq;
A4: d is convergent & lim d = 0 by A3,SEQ_4:46;
now let n;
b.n = x0 & b.(n+1) = x0 by A2;
hence b.n = b.(n+1);
end;
then A5: b is constant by SEQM_3:16;
then A6: b is convergent by SEQ_4:39;
A7: lim b = b.0 by A5,SEQ_4:41
.= x0 by A2;
now let n;
thus (b - d).n = b.n - d.n by RFUNCT_2:6
.= x0 - d.n by A2
.= x0 - p/(n+1) by A3
.=a.n by A1;
end;
then A8: a = b - d by FUNCT_2:113;
hence a is convergent by A4,A6,SEQ_2:25;
thus lim a = x0 - 0 by A4,A6,A7,A8,SEQ_2:26
.= x0;
end;
theorem Th14:
for x0 be real number holds
(for n holds a.n = x0 + p/(n+1)) implies a is convergent & lim a = x0
proof
let x0 be real number;
assume
A1: for n holds a.n = x0 + p/(n+1);
deffunc F(Nat) = x0;
consider b such that
A2: for n holds b.n = F(n) from ExRealSeq;
deffunc F(Nat) = p/($1+1);
consider d such that
A3: for n holds d.n = F(n) from ExRealSeq;
A4: d is convergent & lim d = 0 by A3,SEQ_4:46;
now let n;
b.n = x0 & b.(n+1) = x0 by A2;
hence b.n = b.(n+1);
end;
then A5: b is constant by SEQM_3:16;
then A6: b is convergent by SEQ_4:39;
A7: lim b = b.0 by A5,SEQ_4:41
.= x0 by A2;
now let n;
thus (b + d).n = b.n + d.n by SEQ_1:11
.= x0 + d.n by A2
.= x0 + p/(n+1) by A3
.=a.n by A1;
end;
then A8: a = b + d by FUNCT_2:113;
hence a is convergent by A4,A6,SEQ_2:19;
thus lim a = x0 + 0 by A4,A6,A7,A8,SEQ_2:20
.= x0;
end;
theorem
f is_continuous_in x0 & f.x0 <> r &
(ex N be Neighbourhood of x0 st N c= dom f) implies
ex N be Neighbourhood of x0 st N c= dom f & for g st g in N holds f.g <> r
proof assume
A1: f is_continuous_in x0 & f.x0 <> r;
given N be Neighbourhood of x0 such that
A2: N c= dom f; assume
A3: for N be Neighbourhood of x0 holds
not N c= dom f or ex g st g in N & f.g = r;
consider p be real number such that
A4: 0 < p & N = ].x0 - p,x0 + p.[ by RCOMP_1:def 7;
A5: p is Real by XREAL_0:def 1;
deffunc F(Nat) = x0 - p/($1+1);
consider a such that
A6: for n holds a.n = F(n) from ExRealSeq;
deffunc F(Nat) = x0 + p/($1+1);
consider b such that
A7: for n holds b.n = F(n) from ExRealSeq;
defpred P[Nat,real number] means x0 - p/($1+1) < $2 &
$2 < x0 + p/($1+1) & f.$2 = r & $2 in dom f;
A8: for n ex g be real number st P[n,g]
proof let n;
A9: 0 <= n by NAT_1:18; then 0 < n + 1 by NAT_1:38;
then 0 < p/(n+1) by A4,SEQ_2:6;
then reconsider Nn = ].x0 - p/(n+1),x0 + p/(n+1).[ as Neighbourhood of x0
by RCOMP_1:def 7;
A10: Nn c= dom f
proof let x; assume x in Nn;
then x in {g2: x0 - p/(n+1) < g2 & g2 < x0 + p/(n+1)} by RCOMP_1:def 2;
then consider g2 such that
A11: g2 = x & x0 - p/(n+1) < g2 & g2 < x0 + p/(n+1);
0 + 1 <= n + 1 by A9,REAL_1:55;
then A12: p/(n+1) <= p/1 by A4,REAL_2:201;
then x0 - p <= x0 - p/(n+1) by REAL_1:92;
then A13: x0 - p < g2 by A11,AXIOMS:22;
x0 + p/(n+1) <= x0 + p by A12,REAL_1:55;
then g2 < x0 + p by A11,AXIOMS:22;
then x in {r1: x0 - p < r1 & r1 < x0 + p} by A11,A13;
then x in N by A4,RCOMP_1:def 2;
hence thesis by A2;
end;
then consider g such that
A14: g in Nn & f.g = r by A3;
take g;
g in {g1: x0 - p/(n+1) < g1 & g1 <x0 + p/(n+1)} by A14,RCOMP_1:def 2;
then ex g1 st g1 = g & x0 - p/(n+1) < g1 & g1 <x0 + p/(n+1);
hence x0 - p/(n+1) < g & g <x0 + p/(n+1);
thus f.g = r by A14;
thus thesis by A10,A14;
end;
consider d such that
A15: for n holds P[n,d.n] from RealSeqChoice(A8);
A16: a is convergent & lim a = x0 by A5,A6,Th13;
A17: b is convergent & lim b = x0 by A5,A7,Th14;
A18: now let n;
x0 - p/(n+1) < d.n & d.n < x0 + p/(n+1) by A15;
hence a.n <= d.n & d.n <= b.n by A6,A7;
end;
then A19: d is convergent by A16,A17,SEQ_2:33;
A20: lim d = x0 by A16,A17,A18,SEQ_2:34;
A21: rng d c= dom f
proof let x; assume x in rng d; then ex n st x = d.n by RFUNCT_2:9;
hence thesis by A15;
end;
then A22: f*d is convergent & f.x0 = lim (f*d) by A1,A19,A20,FCONT_1:def 1;
now let r2 be real number such that A23: 0 < r2;
take n = 0;
let m such that n <= m;
abs((f*d).m - r) = abs(f.(d.m) - r) by A21,RFUNCT_2:21
.= abs(r - r) by A15
.= abs(0) by XCMPLX_1:14
.= 0 by ABSVALUE:7;
hence abs((f*d).m - r) < r2 by A23;
end;
hence contradiction by A1,A22,SEQ_2:def 7;
end;
theorem
f is_increasing_on X or f is_decreasing_on X implies f|X is one-to-one
proof assume
A1: f is_increasing_on X or f is_decreasing_on X;
now per cases by A1;
suppose A2: f is_increasing_on X;
now given r1,r2 such that
A3: r1 in dom (f|X) & r2 in dom (f|X) & (f|X).r1 = (f|X).r2 and
A4: r1 <> r2;
A5: r1 in X /\ dom f & r2 in X /\ dom f by A3,FUNCT_1:68;
now per cases by A4,REAL_1:def 5;
suppose r1 < r2; then f.r1 < f.r2 by A2,A5,RFUNCT_2:def 2;
then (f|X).r1 < f.r2 by A3,FUNCT_1:68;
hence contradiction by A3,FUNCT_1:68;
suppose r2 < r1; then f.r2 < f.r1 by A2,A5,RFUNCT_2:def 2;
then (f|X).r2 < f.r1 by A3,FUNCT_1:68;
hence contradiction by A3,FUNCT_1:68;
end;
hence contradiction;
end;
hence thesis by PARTFUN1:38;
suppose A6: f is_decreasing_on X;
now given r1,r2 such that
A7: r1 in dom (f|X) & r2 in dom (f|X) & (f|X).r1 = (f|X).r2 and
A8: r1 <> r2;
A9: r1 in X /\ dom f & r2 in X /\ dom f by A7,FUNCT_1:68;
now per cases by A8,REAL_1:def 5;
suppose r1 < r2; then f.r2 < f.r1 by A6,A9,RFUNCT_2:def 3;
then (f|X).r2 < f.r1 by A7,FUNCT_1:68;
hence contradiction by A7,FUNCT_1:68;
suppose r2 < r1; then f.r1 < f.r2 by A6,A9,RFUNCT_2:def 3;
then (f|X).r1 < f.r2 by A7,FUNCT_1:68;
hence contradiction by A7,FUNCT_1:68;
end;
hence contradiction;
end;
hence thesis by PARTFUN1:38;
end;
hence thesis;
end;
theorem Th17:
for f be one-to-one PartFunc of REAL,REAL st f is_increasing_on X holds
(f|X)" is_increasing_on f.:X
proof let f be one-to-one PartFunc of REAL,REAL;
assume that
A1: f is_increasing_on X and
A2: not (f|X)" is_increasing_on f.:X;
consider r1,r2 such that
A3: r1 in f.:X /\ dom ((f|X)") & r2 in f.:X /\ dom((f|X)") & r1 < r2 &
((f|X)").r1 >= ((f|X)").r2 by A2,RFUNCT_2:def 2;
f.:X = rng (f|X) by RELAT_1:148;
then A4: r1 in rng (f|X) & r2 in rng (f|X) by A3,XBOOLE_0:def 3;
A5: f|X is_increasing_on X by A1,RFUNCT_2:50;
now per cases;
suppose ((f|X)").r1 = ((f|X)").r2;
then r1 = (f|X).(((f|X)").r2) by A4,FUNCT_1:57
.= r2 by A4,FUNCT_1:57;
hence contradiction by A3;
suppose ((f|X)").r1 <> ((f|X)").r2;
then A6: ((f|X)").r2 < ((f|X)").r1 by A3,REAL_1:def 5;
A7: ((f|X)").r2 in dom (f|X) & ((f|X)").r1 in dom (f|X) by A4,PARTFUN2:79;
dom (f|X) = dom ((f|X)|X) by RELAT_1:101
.= X /\ dom (f|X) by RELAT_1:90;
then (f|X).(((f|X)").r2) < (f|X).(((f|X)").r1) by A5,A6,A7,RFUNCT_2:def 2;
then r2 < (f|X).(((f|X)").r1) by A4,FUNCT_1:57;
hence contradiction by A3,A4,FUNCT_1:57;
end;
hence contradiction;
end;
theorem Th18:
for f be one-to-one PartFunc of REAL,REAL st f is_decreasing_on X holds
(f|X)" is_decreasing_on f.:X
proof let f be one-to-one PartFunc of REAL,REAL;
assume that
A1: f is_decreasing_on X and
A2: not (f|X)" is_decreasing_on f.:X;
consider r1,r2 such that
A3: r1 in f.:X /\ dom ((f|X)") & r2 in f.:X /\ dom((f|X)") & r1 < r2 &
((f|X)").r1 <= ((f|X)").r2 by A2,RFUNCT_2:def 3;
f.:X = rng (f|X) by RELAT_1:148;
then A4: r1 in rng (f|X) & r2 in rng (f|X) by A3,XBOOLE_0:def 3;
A5: f|X is_decreasing_on X by A1,RFUNCT_2:51;
now per cases;
suppose ((f|X)").r1 = ((f|X)").r2;
then r1 = (f|X).(((f|X)").r2) by A4,FUNCT_1:57
.= r2 by A4,FUNCT_1:57;
hence contradiction by A3;
suppose ((f|X)").r1 <> ((f|X)").r2;
then A6: ((f|X)").r2 > ((f|X)").r1 by A3,REAL_1:def 5;
A7: ((f|X)").r2 in dom (f|X) & ((f|X)").r1 in dom (f|X) by A4,PARTFUN2:79;
dom (f|X) = dom ((f|X)|X) by RELAT_1:101
.= X /\ dom (f|X) by RELAT_1:90;
then (f|X).(((f|X)").r2) < (f|X).(((f|X)").r1) by A5,A6,A7,RFUNCT_2:def 3;
then r2 < (f|X).(((f|X)").r1) by A4,FUNCT_1:57;
hence contradiction by A3,A4,FUNCT_1:57;
end;
hence contradiction;
end;
theorem Th19:
X c= dom f & f is_monotone_on X & (ex p st f.:
X = left_open_halfline(p)) implies
f is_continuous_on X
proof assume
A1: X c= dom f & f is_monotone_on X;
given p such that
A2: f.:X = left_open_halfline(p);
set L = left_open_halfline(p);
now per cases by A1,RFUNCT_2:def 6;
suppose f is_non_decreasing_on X;
then A3: f|X is_non_decreasing_on X by RFUNCT_2:52;
for x0 be real number st x0 in X holds f|X is_continuous_in x0
proof let x0 be real number; assume
A4: x0 in X;
then x0 in dom f /\ X by A1,XBOOLE_0:def 3;
then A5: x0 in dom (f|X) by RELAT_1:90;
then A6: (f|X).x0 in (f|X).:X by A4,FUNCT_1:def 12;
A7: x0 is Real by XREAL_0:def 1;
A8: (f|X).:X = f.:X by RFUNCT_2:5;
A9: (f|X).x0 in L by A2,A6,RFUNCT_2:5;
now let N1 be Neighbourhood of (f|X).x0;
consider N2 being Neighbourhood of (f|X).x0 such that
A10: N2 c= L by A9,RCOMP_1:39;
consider N3 being Neighbourhood of (f|X).x0 such that
A11: N3 c= N1 & N3 c= N2 by RCOMP_1:38;
consider r be real number such that
A12: r>0 & N3 = ].(f|X).x0 - r,(f|X).x0 + r.[ by RCOMP_1:def 7;
reconsider r as Real by XREAL_0:def 1;
set M1 = (f|X).x0 - r/2;
set M2 = (f|X).x0 + r/2;
A13: r/2 > 0 by A12,SEQ_2:3;
then (f|X).x0 - r < (f|X).x0 - r + r/2 by REAL_1:69;
then (f|X).x0 - r < (f|X).x0 - (r/2 + r/2) + r/2 by XCMPLX_1:66;
then (f|X).x0 - r < (f|X).x0 - (r/2 + r/2 - r/2) by XCMPLX_1:37;
then A14: (f|X).x0 - r < (f|X).x0 - r/2 by XCMPLX_1:26;
A15: (f|X).x0 < (f|X).x0 + r/2 by A13,REAL_1:69;
then A16: (f|X).x0 - r/2 < (f|X).x0 by REAL_1:84;
A17: (f|X).x0 < (f|X).x0 + r by A12,REAL_1:69;
then (f|X).x0 - r/2 < (f|X).x0 + r by A16,AXIOMS:22;
then (f|X).x0 - r/2 in {s: (f|X).x0 - r < s & s < (f|X).x0 + r} by A14
;
then A18: M1 in ].(f|X).x0 - r,(f|X).x0 + r.[ by RCOMP_1:def 2;
(f|X).x0 + r/2 < (f|X).x0 + r/2 + r/2 by A13,REAL_1:69;
then (f|X).x0 + r/2 < (f|X).x0 + (r/2 + r/2) by XCMPLX_1:1;
then A19: (f|X).x0 + r/2 < (f|X).x0 + r by XCMPLX_1:66;
(f|X).x0 - r < (f|X).x0 + r - r by A17,REAL_1:54;
then (f|X).x0 - r < (f|X).x0 by XCMPLX_1:26;
then (f|X).x0 - r < (f|X).x0 + r/2 by A15,AXIOMS:22;
then (f|X).x0 + r/2 in {s: (f|X).x0 - r < s & s < (f|X).x0 + r} by A19
;
then A20: M2 in ].(f|X).x0 - r,(f|X).x0 + r.[ by RCOMP_1:def 2;
then A21: [.M1,M2.] c= ].(f|X).x0 - r,(f|X).x0 + r.[ by A18,RCOMP_1:17;
M1 in N2 by A11,A12,A18;
then consider r1 such that
A22: r1 in dom (f|X) & r1 in
X & M1 = (f|X).r1 by A2,A8,A10,PARTFUN2:78;
M2 in N2 by A11,A12,A20;
then consider r2 such that
A23: r2 in dom (f|X) & r2 in
X & M2 = (f|X).r2 by A2,A8,A10,PARTFUN2:78;
set R = min(x0 - r1,r2 - x0);
A24: (f|X).x0 < (f|X).x0 + r/2 by A13,REAL_1:69;
then A25: M1 < (f|X).x0 by REAL_1:84;
A26: r1 <> x0 by A22,A24,REAL_1:84;
now assume
A27: x0 < r1;
A28: x0 in X /\ dom( f|X) by A4,A5,XBOOLE_0:def 3;
r1 in X /\ dom(f|X) by A22,XBOOLE_0:def 3;
hence contradiction by A3,A7,A22,A25,A27,A28,RFUNCT_2:def 4;
end;
then r1 < x0 by A26,REAL_1:def 5;
then A29: x0 - r1 > 0 by SQUARE_1:11;
A30: M2 > (f|X).x0 by A13,REAL_1:69;
A31: x0 <> r2 by A13,A23,REAL_1:69;
now assume
A32: r2 < x0;
A33: x0 in X /\ dom(f|X) by A4,A5,XBOOLE_0:def 3;
r2 in X /\ dom (f|X) by A23,XBOOLE_0:def 3;
hence contradiction by A3,A7,A23,A30,A32,A33,RFUNCT_2:def 4;
end;
then x0 < r2 by A31,REAL_1:def 5;
then r2 - x0 > 0 by SQUARE_1:11;
then R > 0 by A29,SQUARE_1:38;
then reconsider N = ].x0 - R,x0 + R.[ as Neighbourhood of x0 by RCOMP_1
:def 7;
take N;
let x be real number; assume
A34: x in dom (f|X) & x in N;
then x in {s: x0 - R < s & s < x0 + R} by RCOMP_1:def 2;
then A35: ex s st s = x & x0 - R < s & s < x0 + R;
then x0 < R + x by REAL_1:84;
then x0 - x < R + x - x by REAL_1:54
;
then A36: x0 - x < R by XCMPLX_1:26; R <= x0 - r1 by SQUARE_1:35;
then x0 - x < x0 - r1 by A36,AXIOMS:22;
then -(x0 - x) > -(x0 - r1) by REAL_1:50;
then x - x0 > -(x0 - r1) by XCMPLX_1:143;
then x - x0 > r1 - x0 by XCMPLX_1:143;
then x - x0 + x0 > r1 - x0 + x0 by REAL_1:53;
then x > r1 - x0 + x0 by XCMPLX_1:27;
then A37: x > r1 by XCMPLX_1:27;
A38: x is Real by XREAL_0:def 1;
A39: x - x0 < R by A35,REAL_1:84; R <= r2 - x0 by SQUARE_1:35;
then x - x0 < r2 - x0 by A39,AXIOMS:22;
then x - x0 + x0 < r2 - x0 + x0 by REAL_1:53;
then x < r2 - x0 + x0 by XCMPLX_1:27;
then A40: x < r2 by XCMPLX_1:27;
dom (f|X) c= X by RELAT_1:87;
then A41: x in X /\ dom (f|X) by A34,XBOOLE_1:28;
r2 in X /\ dom (f|X) by A23,XBOOLE_0:def 3;
then A42: (f|X).x <= (f|X).r2 by A3,A38,A40,A41,RFUNCT_2:def 4;
r1 in X /\ dom (f|X) by A22,XBOOLE_0:def 3;
then (f|X).r1 <= (f|X).x by A3,A37,A38,A41,RFUNCT_2:def 4;
then (f|X).x in {s: M1<=s & s<=M2} by A22,A23,A42;
then (f|X).x in [.M1,M2.] by RCOMP_1:def 1;
then (f|X).x in N3 by A12,A21;
hence (f|X).x in N1 by A11;
end;
hence thesis by A5,FCONT_1:4;
end;
hence f is_continuous_on X by A1,FCONT_1:def 2;
suppose f is_non_increasing_on X;
then A43: f|X is_non_increasing_on X by RFUNCT_2:53;
for x0 be real number st x0 in X holds f|X is_continuous_in x0
proof let x0 be real number; assume
A44: x0 in X;
then x0 in dom f /\ X by A1,XBOOLE_0:def 3;
then A45: x0 in dom(f|X) by RELAT_1:90;
then A46: (f|X).x0 in (f|X).:X by A44,FUNCT_1:def 12;
A47: x0 is Real by XREAL_0:def 1;
A48: (f|X).:X = f.:X by RFUNCT_2:5;
A49: (f|X).x0 in L by A2,A46,RFUNCT_2:5;
now let N1 be Neighbourhood of (f|X).x0;
consider N2 being Neighbourhood of (f|X).x0 such that
A50: N2 c= L by A49,RCOMP_1:39;
consider N3 being Neighbourhood of (f|X).x0 such that
A51: N3 c= N1 & N3 c= N2 by RCOMP_1:38;
consider r be real number such that
A52: r > 0 & N3 = ].(f|X).x0 - r,(f|X).x0 + r.[ by RCOMP_1:def 7;
reconsider r as Real by XREAL_0:def 1;
set M1 = (f|X).x0 - r/2;
set M2 = (f|X).x0 + r/2;
A53: r/2 > 0 by A52,SEQ_2:3;
then (f|X).x0 - r < (f|X).x0 - r + r/2 by REAL_1:69;
then (f|X).x0 - r < (f|X).x0 - (r/2 + r/2) + r/2 by XCMPLX_1:66;
then (f|X).x0 - r < (f|X).x0 - (r/2 + r/2 - r/2) by XCMPLX_1:37;
then A54: (f|X).x0 - r < (f|X).x0 - r/2 by XCMPLX_1:26;
A55: (f|X).x0 < (f|X).x0 + r/2 by A53,REAL_1:69;
then A56: (f|X).x0 - r/2 < (f|X).x0 by REAL_1:84;
A57: (f|X).x0 < (f|X).x0 + r by A52,REAL_1:69;
then (f|X).x0 - r/2 < (f|X).x0 + r by A56,AXIOMS:22;
then (f|X).x0 - r/2 in {s: (f|X).x0 - r < s & s < (f|X).x0 + r} by A54
;
then A58: M1 in ].(f|X).x0 - r,(f|X).x0 + r.[ by RCOMP_1:def 2;
(f|X).x0 + r/2 < (f|X).x0 + r/2 + r/2 by A53,REAL_1:69;
then (f|X).x0 + r/2 < (f|X).x0 + (r/2 + r/2) by XCMPLX_1:1;
then A59: (f|X).x0 + r/2 < (f|X).x0 + r by XCMPLX_1:66;
(f|X).x0 - r < (f|X).x0 + r - r by A57,REAL_1:54;
then (f|X).x0 - r < (f|X).x0 by XCMPLX_1:26;
then (f|X).x0 - r < (f|X).x0 + r/2 by A55,AXIOMS:22;
then (f|X).x0 + r/2 in {s: (f|X).x0 - r < s & s < (f|X).x0 + r} by A59
;
then A60: M2 in ].(f|X).x0 - r,(f|X).x0 + r.[ by RCOMP_1:def 2;
then A61: [.M1,M2.] c= ].(f|X).x0 - r,(f|X).x0 + r.[ by A58,RCOMP_1:17;
M1 in N2 by A51,A52,A58;
then consider r1 such that
A62: r1 in dom (f|X) & r1 in
X & M1 = (f|X).r1 by A2,A48,A50,PARTFUN2:78;
M2 in N2 by A51,A52,A60;
then consider r2 such that
A63: r2 in dom (f|X) & r2 in
X & M2 = (f|X).r2 by A2,A48,A50,PARTFUN2:78;
set R = min(r1 - x0,x0 - r2);
A64: (f|X).x0 < (f|X).x0 + r/2 by A53,REAL_1:69;
then A65: M1 < (f|X).x0 by REAL_1:84;
A66: r1 <> x0 by A62,A64,REAL_1:84;
now assume
A67: x0 > r1;
A68: x0 in X /\ dom (f|X) by A44,A45,XBOOLE_0:def 3;
r1 in X /\ dom(f|X) by A62,XBOOLE_0:def 3;
hence contradiction by A43,A47,A62,A65,A67,A68,RFUNCT_2:def 5;
end;
then r1 > x0 by A66,REAL_1:def 5;
then A69: r1 - x0 > 0 by SQUARE_1:11;
A70: M2 > (f|X).x0 by A53,REAL_1:69;
A71: x0 <> r2 by A53,A63,REAL_1:69;
now assume
A72: r2 > x0;
A73: x0 in X /\ dom (f|X) by A44,A45,XBOOLE_0:def 3;
r2 in X /\ dom (f|X) by A63,XBOOLE_0:def 3;
hence contradiction by A43,A47,A63,A70,A72,A73,RFUNCT_2:def 5;
end;
then x0 > r2 by A71,REAL_1:def 5;
then x0 - r2 > 0 by SQUARE_1:11;
then R > 0 by A69,SQUARE_1:38;
then reconsider N = ].x0 - R,x0 + R.[ as Neighbourhood of x0 by RCOMP_1
:def 7;
take N;
let x be real number; assume
A74: x in dom (f|X) & x in N;
then x in {s: x0 - R < s & s < x0 + R} by RCOMP_1:def 2;
then A75: ex s st s = x & x0 - R < s & s < x0 + R;
then x0 < R + x by REAL_1:84;
then x0 - x < R + x - x by REAL_1:54
;
then A76: x0 - x < R by XCMPLX_1:26; R <= x0 - r2 by SQUARE_1:35;
then x0 - x < x0 - r2 by A76,AXIOMS:22;
then -(x0 - x) > -(x0 - r2) by REAL_1:50;
then x - x0 > - (x0 - r2) by XCMPLX_1:143;
then x - x0 > r2 - x0 by XCMPLX_1:143;
then x - x0 + x0 > r2 - x0 + x0 by REAL_1:53;
then x > r2 - x0 + x0 by XCMPLX_1:27;
then A77: x > r2 by XCMPLX_1:27;
A78: x is Real by XREAL_0:def 1;
A79: x - x0 < R by A75,REAL_1:84; R <= r1 - x0 by SQUARE_1:35;
then x - x0 < r1-x0 by A79,AXIOMS:22;
then x - x0 + x0 < r1 - x0 + x0 by REAL_1:53;
then x < r1 - x0 + x0 by XCMPLX_1:27;
then A80: x < r1 by XCMPLX_1:27;
dom (f|X) c= X by RELAT_1:87;
then A81: x in X /\ dom(f|X) by A74,XBOOLE_1:28;
r2 in X /\ dom(f|X) by A63,XBOOLE_0:def 3;
then A82: (f|X).x <= (f|X).r2 by A43,A77,A78,A81,RFUNCT_2:def 5;
r1 in X /\ dom(f|X) by A62,XBOOLE_0:def 3;
then (f|X).r1 <= (f|X).x by A43,A78,A80,A81,RFUNCT_2:def 5;
then (f|X).x in {s: M1 <= s & s <= M2} by A62,A63,A82;
then (f|X).x in [.M1,M2.] by RCOMP_1:def 1;
then (f|X).x in N3 by A52,A61;
hence (f|X).x in N1 by A51;
end;
hence thesis by A45,FCONT_1:4;
end;
hence f is_continuous_on X by A1,FCONT_1:def 2;
end;
hence thesis;
end;
theorem Th20:
X c= dom f & f is_monotone_on X &
(ex p st f.:X = right_open_halfline(p)) implies f is_continuous_on X
proof assume
A1: X c= dom f & f is_monotone_on X;
given p such that
A2: f.:X = right_open_halfline(p);
set L = right_open_halfline(p);
now per cases by A1,RFUNCT_2:def 6;
suppose f is_non_decreasing_on X;
then A3: f|X is_non_decreasing_on X by RFUNCT_2:52;
for x0 be real number st x0 in X holds f|X is_continuous_in x0
proof let x0 be real number; assume
A4: x0 in X;
then x0 in dom f /\ X by A1,XBOOLE_0:def 3;
then A5: x0 in dom (f|X) by RELAT_1:90;
then A6: (f|X).x0 in (f|X).:X by A4,FUNCT_1:def 12;
A7: x0 is Real by XREAL_0:def 1;
A8: (f|X).:X = f.:X by RFUNCT_2:5;
A9: (f|X).x0 in L by A2,A6,RFUNCT_2:5;
now let N1 be Neighbourhood of (f|X).x0;
consider N2 being Neighbourhood of (f|X).x0 such that
A10: N2 c= L by A9,RCOMP_1:39;
consider N3 being Neighbourhood of (f|X).x0 such that
A11: N3 c= N1 & N3 c= N2 by RCOMP_1:38;
consider r be real number such that
A12: r>0 & N3 = ].(f|X).x0 - r,(f|X).x0 + r.[ by RCOMP_1:def 7;
reconsider r as Real by XREAL_0:def 1;
set M1 = (f|X).x0 - r/2;
set M2 = (f|X).x0 + r/2;
A13: r/2 > 0 by A12,SEQ_2:3;
then (f|X).x0 - r < (f|X).x0 - r + r/2 by REAL_1:69;
then (f|X).x0 - r < (f|X).x0 - (r/2 + r/2) + r/2 by XCMPLX_1:66;
then (f|X).x0 - r < (f|X).x0 - (r/2 + r/2 - r/2) by XCMPLX_1:37;
then A14: (f|X).x0 - r < (f|X).x0 - r/2 by XCMPLX_1:26;
A15: (f|X).x0 < (f|X).x0 + r/2 by A13,REAL_1:69;
then A16: (f|X).x0 - r/2 < (f|X).x0 by REAL_1:84;
A17: (f|X).x0 < (f|X).x0 + r by A12,REAL_1:69;
then (f|X).x0 - r/2 < (f|X).x0 + r by A16,AXIOMS:22;
then (f|X).x0 - r/2 in {s: (f|X).x0 - r < s & s < (f|X).x0 + r} by A14
;
then A18: M1 in ].(f|X).x0 - r,(f|X).x0 + r.[ by RCOMP_1:def 2;
(f|X).x0 + r/2 < (f|X).x0 + r/2 + r/2 by A13,REAL_1:69;
then (f|X).x0 + r/2 < (f|X).x0 + (r/2 + r/2) by XCMPLX_1:1;
then A19: (f|X).x0 + r/2 < (f|X).x0 + r by XCMPLX_1:66;
(f|X).x0 - r < (f|X).x0 + r - r by A17,REAL_1:54;
then (f|X).x0 - r < (f|X).x0 by XCMPLX_1:26;
then (f|X).x0 - r < (f|X).x0 + r/2 by A15,AXIOMS:22;
then (f|X).x0 + r/2 in {s: (f|X).x0 - r < s & s < (f|X).x0 + r} by A19
;
then A20: M2 in ].(f|X).x0 - r,(f|X).x0 + r.[ by RCOMP_1:def 2;
then A21: [.M1,M2.] c= ].(f|X).x0 - r,(f|X).x0 + r.[ by A18,RCOMP_1:17;
M1 in N2 by A11,A12,A18;
then consider r1 such that
A22: r1 in dom (f|X) & r1 in
X & M1 = (f|X).r1 by A2,A8,A10,PARTFUN2:78;
M2 in N2 by A11,A12,A20;
then consider r2 such that
A23: r2 in dom (f|X) & r2 in
X & M2 = (f|X).r2 by A2,A8,A10,PARTFUN2:78;
set R = min(x0 - r1,r2 - x0);
A24: (f|X).x0 < (f|X).x0 + r/2 by A13,REAL_1:69;
then A25: M1 < (f|X).x0 by REAL_1:84;
A26: r1 <> x0 by A22,A24,REAL_1:84;
now assume
A27: x0 < r1;
A28: x0 in X /\ dom( f|X) by A4,A5,XBOOLE_0:def 3;
r1 in X /\ dom(f|X) by A22,XBOOLE_0:def 3;
hence contradiction by A3,A7,A22,A25,A27,A28,RFUNCT_2:def 4;
end;
then r1 < x0 by A26,REAL_1:def 5;
then A29: x0 - r1 > 0 by SQUARE_1:11;
A30: M2 > (f|X).x0 by A13,REAL_1:69;
A31: x0 <> r2 by A13,A23,REAL_1:69;
now assume
A32: r2 < x0;
A33: x0 in X /\ dom(f|X) by A4,A5,XBOOLE_0:def 3;
r2 in X /\ dom (f|X) by A23,XBOOLE_0:def 3;
hence contradiction by A3,A7,A23,A30,A32,A33,RFUNCT_2:def 4;
end;
then x0 < r2 by A31,REAL_1:def 5;
then r2 - x0 > 0 by SQUARE_1:11;
then R > 0 by A29,SQUARE_1:38;
then reconsider N = ].x0 - R,x0 + R.[ as Neighbourhood of x0 by RCOMP_1
:def 7;
take N;
let x be real number; assume
A34: x in dom (f|X) & x in N;
then x in {s: x0 - R < s & s < x0 + R} by RCOMP_1:def 2;
then A35: ex s st s = x & x0 - R < s & s < x0 + R;
then x0 < R + x by REAL_1:84;
then x0 - x < R + x - x by REAL_1:54
;
then A36: x0 - x < R by XCMPLX_1:26; R <= x0 - r1 by SQUARE_1:35;
then x0 - x < x0 - r1 by A36,AXIOMS:22;
then -(x0 - x) > -(x0 - r1) by REAL_1:50;
then x - x0 > -(x0 - r1) by XCMPLX_1:143;
then x - x0 > r1 - x0 by XCMPLX_1:143;
then x - x0 + x0 > r1 - x0 + x0 by REAL_1:53;
then x > r1 - x0 + x0 by XCMPLX_1:27;
then A37: x > r1 by XCMPLX_1:27;
A38: x is Real by XREAL_0:def 1;
A39: x - x0 < R by A35,REAL_1:84; R <= r2 - x0 by SQUARE_1:35;
then x - x0 < r2 - x0 by A39,AXIOMS:22;
then x - x0 + x0 < r2 - x0 + x0 by REAL_1:53;
then x < r2 - x0 + x0 by XCMPLX_1:27;
then A40: x < r2 by XCMPLX_1:27;
dom (f|X) c= X by RELAT_1:87;
then A41: x in X /\ dom (f|X) by A34,XBOOLE_1:28;
r2 in X /\ dom (f|X) by A23,XBOOLE_0:def 3;
then A42: (f|X).x <= (f|X).r2 by A3,A38,A40,A41,RFUNCT_2:def 4;
r1 in X /\ dom (f|X) by A22,XBOOLE_0:def 3;
then (f|X).r1 <= (f|X).x by A3,A37,A38,A41,RFUNCT_2:def 4;
then (f|X).x in {s: M1<=s & s<=M2} by A22,A23,A42;
then (f|X).x in [.M1,M2.] by RCOMP_1:def 1;
then (f|X).x in N3 by A12,A21;
hence (f|X).x in N1 by A11;
end;
hence thesis by A5,FCONT_1:4;
end;
hence f is_continuous_on X by A1,FCONT_1:def 2;
suppose f is_non_increasing_on X;
then A43: f|X is_non_increasing_on X by RFUNCT_2:53;
for x0 be real number st x0 in X holds f|X is_continuous_in x0
proof let x0 be real number; assume
A44: x0 in X;
then x0 in dom f /\ X by A1,XBOOLE_0:def 3;
then A45: x0 in dom(f|X) by RELAT_1:90;
then A46: (f|X).x0 in (f|X).:X by A44,FUNCT_1:def 12;
A47: (f|X).:X = f.:X by RFUNCT_2:5;
A48: x0 is Real by XREAL_0:def 1;
A49: (f|X).x0 in L by A2,A46,RFUNCT_2:5;
now let N1 be Neighbourhood of (f|X).x0;
consider N2 being Neighbourhood of (f|X).x0 such that
A50: N2 c= L by A49,RCOMP_1:39;
consider N3 being Neighbourhood of (f|X).x0 such that
A51: N3 c= N1 & N3 c= N2 by RCOMP_1:38;
consider r be real number such that
A52: r > 0 & N3 = ].(f|X).x0 - r,(f|X).x0 + r.[ by RCOMP_1:def 7;
reconsider r as Real by XREAL_0:def 1;
set M1 = (f|X).x0 - r/2;
set M2 = (f|X).x0 + r/2;
A53: r/2 > 0 by A52,SEQ_2:3;
then (f|X).x0 - r < (f|X).x0 - r + r/2 by REAL_1:69;
then (f|X).x0 - r < (f|X).x0 - (r/2 + r/2) + r/2 by XCMPLX_1:66;
then (f|X).x0 - r < (f|X).x0 - (r/2 + r/2 - r/2) by XCMPLX_1:37;
then A54: (f|X).x0 - r < (f|X).x0 - r/2 by XCMPLX_1:26;
A55: (f|X).x0 < (f|X).x0 + r/2 by A53,REAL_1:69;
then A56: (f|X).x0 - r/2 < (f|X).x0 by REAL_1:84;
A57: (f|X).x0 < (f|X).x0 + r by A52,REAL_1:69;
then (f|X).x0 - r/2 < (f|X).x0 + r by A56,AXIOMS:22;
then (f|X).x0 - r/2 in {s: (f|X).x0 - r < s & s < (f|X).x0 + r} by A54
;
then A58: M1 in ].(f|X).x0 - r,(f|X).x0 + r.[ by RCOMP_1:def 2;
(f|X).x0 + r/2 < (f|X).x0 + r/2 + r/2 by A53,REAL_1:69;
then (f|X).x0 + r/2 < (f|X).x0 + (r/2 + r/2) by XCMPLX_1:1;
then A59: (f|X).x0 + r/2 < (f|X).x0 + r by XCMPLX_1:66;
(f|X).x0 - r < (f|X).x0 + r - r by A57,REAL_1:54;
then (f|X).x0 - r < (f|X).x0 by XCMPLX_1:26;
then (f|X).x0 - r < (f|X).x0 + r/2 by A55,AXIOMS:22;
then (f|X).x0 + r/2 in {s: (f|X).x0 - r < s & s < (f|X).x0 + r} by A59
;
then A60: M2 in ].(f|X).x0 - r,(f|X).x0 + r.[ by RCOMP_1:def 2;
then A61: [.M1,M2.] c= ].(f|X).x0 - r,(f|X).x0 + r.[ by A58,RCOMP_1:17;
M1 in N2 by A51,A52,A58;
then consider r1 such that
A62: r1 in dom (f|X) & r1 in
X & M1 = (f|X).r1 by A2,A47,A50,PARTFUN2:78;
M2 in N2 by A51,A52,A60;
then consider r2 such that
A63: r2 in dom (f|X) & r2 in
X & M2 = (f|X).r2 by A2,A47,A50,PARTFUN2:78;
set R = min(r1 - x0,x0 - r2);
A64: (f|X).x0 < (f|X).x0 + r/2 by A53,REAL_1:69;
then A65: M1 < (f|X).x0 by REAL_1:84;
A66: r1 <> x0 by A62,A64,REAL_1:84;
now assume
A67: x0 > r1;
A68: x0 in X /\ dom (f|X) by A44,A45,XBOOLE_0:def 3;
r1 in X /\ dom(f|X) by A62,XBOOLE_0:def 3;
hence contradiction by A43,A48,A62,A65,A67,A68,RFUNCT_2:def 5;
end;
then r1 > x0 by A66,REAL_1:def 5;
then A69: r1 - x0 > 0 by SQUARE_1:11;
A70: M2 > (f|X).x0 by A53,REAL_1:69;
A71: x0 <> r2 by A53,A63,REAL_1:69;
now assume
A72: r2 > x0;
A73: x0 in X /\ dom (f|X) by A44,A45,XBOOLE_0:def 3;
r2 in X /\ dom (f|X) by A63,XBOOLE_0:def 3;
hence contradiction by A43,A48,A63,A70,A72,A73,RFUNCT_2:def 5;
end;
then x0 > r2 by A71,REAL_1:def 5;
then x0 - r2 > 0 by SQUARE_1:11;
then R > 0 by A69,SQUARE_1:38;
then reconsider N = ].x0 - R,x0 + R.[ as Neighbourhood of x0 by RCOMP_1
:def 7;
take N;
let x be real number; assume
A74: x in dom (f|X) & x in N;
then x in {s: x0 - R < s & s < x0 + R} by RCOMP_1:def 2;
then A75: ex s st s = x & x0 - R < s & s < x0 + R;
then x0 < R + x by REAL_1:84;
then x0 - x < R + x - x by REAL_1:54
;
then A76: x0 - x < R by XCMPLX_1:26; R <= x0 - r2 by SQUARE_1:35;
then x0 - x < x0 - r2 by A76,AXIOMS:22;
then -(x0 - x) > -(x0 - r2) by REAL_1:50;
then x - x0 > - (x0 - r2) by XCMPLX_1:143;
then x - x0 > r2 - x0 by XCMPLX_1:143;
then x - x0 + x0 > r2 - x0 + x0 by REAL_1:53;
then x > r2 - x0 + x0 by XCMPLX_1:27;
then A77: x > r2 by XCMPLX_1:27;
A78: x is Real by XREAL_0:def 1;
A79: x - x0 < R by A75,REAL_1:84; R <= r1 - x0 by SQUARE_1:35;
then x - x0 < r1-x0 by A79,AXIOMS:22;
then x - x0 + x0 < r1 - x0 + x0 by REAL_1:53;
then x < r1 - x0 + x0 by XCMPLX_1:27;
then A80: x < r1 by XCMPLX_1:27;
dom (f|X) c= X by RELAT_1:87;
then A81: x in X /\ dom(f|X) by A74,XBOOLE_1:28;
r2 in X /\ dom(f|X) by A63,XBOOLE_0:def 3;
then A82: (f|X).x <= (f|X).r2 by A43,A77,A78,A81,RFUNCT_2:def 5;
r1 in X /\ dom(f|X) by A62,XBOOLE_0:def 3;
then (f|X).r1 <= (f|X).x by A43,A78,A80,A81,RFUNCT_2:def 5;
then (f|X).x in {s: M1 <= s & s <= M2} by A62,A63,A82;
then (f|X).x in [.M1,M2.] by RCOMP_1:def 1;
then (f|X).x in N3 by A52,A61;
hence (f|X).x in N1 by A51;
end;
hence thesis by A45,FCONT_1:4;
end;
hence f is_continuous_on X by A1,FCONT_1:def 2;
end;
hence thesis;
end;
theorem Th21:
X c= dom f & f is_monotone_on X & (ex p st f.:
X=left_closed_halfline(p)) implies
f is_continuous_on X
proof assume
A1: X c= dom f & f is_monotone_on X;
given p such that
A2: f.:X = left_closed_halfline(p);
set l = left_closed_halfline(p);
set L = left_open_halfline(p);
for x0 be real number st x0 in X holds f|X is_continuous_in x0
proof let x0 be real number; assume
A3: x0 in X;
then x0 in dom f /\ X by A1,XBOOLE_0:def 3;
then A4: x0 in dom (f|X) by RELAT_1:90;
then A5: (f|X).x0 in (f|X).:X by A3,FUNCT_1:def 12;
A6: (f|X).:X = f.:X by RFUNCT_2:5;
then (f|X).x0 in {p} \/ L by A2,A5,Th11;
then A7: (f|X).x0 in {p} or (f|X).x0 in L by XBOOLE_0:def 2;
A8: L c= l by LIMFUNC1:15;
A9: x0 is Real by XREAL_0:def 1;
now let N1 be Neighbourhood of (f|X).x0;
now per cases by A1,RFUNCT_2:def 6;
suppose f is_non_decreasing_on X;
then A10: f|X is_non_decreasing_on X by RFUNCT_2:52;
now per cases by A7,TARSKI:def 1;
suppose (f|X).x0 in L;
then consider N2 being Neighbourhood of (f|X).x0 such that
A11: N2 c= L by RCOMP_1:39;
consider N3 being Neighbourhood of (f|X).x0 such that
A12: N3 c= N1 & N3 c= N2 by RCOMP_1:38;
consider r be real number such that
A13: r>0 & N3 = ].(f|X).x0 - r,(f|X).x0 + r.[ by RCOMP_1:def 7;
reconsider r as Real by XREAL_0:def 1;
set M1 = (f|X).x0 - r/2;
set M2 = (f|X).x0 + r/2;
A14: r/2 > 0 by A13,SEQ_2:3;
then (f|X).x0 - r < (f|X).x0 - r + r/2 by REAL_1:69;
then (f|X).x0 - r < (f|X).x0 - (r/2 + r/2) + r/2 by XCMPLX_1:66;
then (f|X).x0 - r < (f|X).x0 - (r/2 + r/2 - r/2) by XCMPLX_1:37;
then A15: (f|X).x0 - r < (f|X).x0 - r/2 by XCMPLX_1:26;
A16: (f|X).x0 < (f|X).x0 + r/2 by A14,REAL_1:69;
then A17: (f|X).x0 - r/2 < (f|X).x0 by REAL_1:84;
A18: (f|X).x0 < (f|X).x0 + r by A13,REAL_1:69;
then (f|X).x0 - r/2 < (f|X).x0 + r by A17,AXIOMS:22;
then (f|X).x0 - r/2 in {s: (f|X).x0 - r < s & s < (f|X).x0 + r} by
A15;
then A19: M1 in ].(f|X).x0 - r,(f|X).x0 + r.[ by RCOMP_1:def 2;
(f|X).x0 + r/2 < (f|X).x0 + r/2 + r/2 by A14,REAL_1:69;
then (f|X).x0 + r/2 < (f|X).x0 + (r/2 + r/2) by XCMPLX_1:1;
then A20: (f|X).x0 + r/2 < (f|X).x0 + r by XCMPLX_1:66;
(f|X).x0 - r < (f|X).x0 + r - r by A18,REAL_1:54;
then (f|X).x0 - r < (f|X).x0 by XCMPLX_1:26;
then (f|X).x0 - r < (f|X).x0 + r/2 by A16,AXIOMS:22;
then (f|X).x0 + r/2 in {s: (f|X).x0 - r < s & s < (f|X).x0 + r} by
A20;
then A21: M2 in ].(f|X).x0 - r,(f|X).x0 + r.[ by RCOMP_1:def 2;
then A22: [.M1,M2.] c= ].(f|X).x0 - r,(f|X).x0 + r.[ by A19,RCOMP_1:
17;
M1 in N2 by A12,A13,A19;
then M1 in L by A11;
then consider r1 such that
A23: r1 in dom (f|X) & r1 in
X & M1 = (f|X).r1 by A2,A6,A8,PARTFUN2:78;
M2 in N2 by A12,A13,A21;
then M2 in L by A11;
then consider r2 such that
A24: r2 in dom (f|X) & r2 in
X & M2 = (f|X).r2 by A2,A6,A8,PARTFUN2:78;
set R = min(x0 - r1,r2 - x0);
A25: (f|X).x0 < (f|X).x0 + r/2 by A14,REAL_1:69;
then A26: M1 < (f|X).x0 by REAL_1:84;
A27: r1 <> x0 by A23,A25,REAL_1:84;
now assume
A28: x0 < r1;
A29: x0 in X /\ dom( f|X) by A3,A4,XBOOLE_0:def 3;
r1 in X /\ dom(f|X) by A23,XBOOLE_0:def 3;
hence contradiction by A9,A10,A23,A26,A28,A29,RFUNCT_2:def 4;
end;
then r1 < x0 by A27,REAL_1:def 5;
then A30: x0 - r1 > 0 by SQUARE_1:11;
A31: M2 > (f|X).x0 by A14,REAL_1:69;
A32: x0 <> r2 by A14,A24,REAL_1:69;
now assume
A33: r2 < x0;
A34: x0 in X /\ dom(f|X) by A3,A4,XBOOLE_0:def 3;
r2 in X /\ dom (f|X) by A24,XBOOLE_0:def 3;
hence contradiction by A9,A10,A24,A31,A33,A34,RFUNCT_2:def 4;
end;
then x0 < r2 by A32,REAL_1:def 5;
then r2 - x0 > 0 by SQUARE_1:11;
then R > 0 by A30,SQUARE_1:38;
then reconsider N = ].x0 - R,x0+ R.[ as Neighbourhood of x0 by
RCOMP_1:def 7;
take N;
let x be real number; assume
A35: x in dom (f|X) & x in N;
then x in {s: x0 - R < s & s < x0 + R} by RCOMP_1:def 2;
then A36: ex s st s = x & x0 - R < s & s < x0 + R;
then x0 < R + x by REAL_1:84;
then x0 - x < R + x - x by REAL_1:54;
then A37: x0 - x < R by XCMPLX_1:26; R <= x0 - r1 by SQUARE_1:35;
then x0 - x < x0 - r1 by A37,AXIOMS:22;
then -(x0 - x) > -(x0 - r1) by REAL_1:50;
then x - x0 > -(x0 - r1) by XCMPLX_1:143;
then x - x0 > r1 - x0 by XCMPLX_1:143;
then x - x0 + x0 > r1 - x0 + x0 by REAL_1:53;
then x > r1 - x0 + x0 by XCMPLX_1:27;
then A38: x > r1 by XCMPLX_1:27;
A39: x is Real by XREAL_0:def 1;
A40: x - x0 < R by A36,REAL_1:84; R <= r2 - x0 by SQUARE_1:35;
then x - x0 < r2 - x0 by A40,AXIOMS:22;
then x - x0 + x0 < r2 - x0 + x0 by REAL_1:53;
then x < r2 - x0 + x0 by XCMPLX_1:27;
then A41: x < r2 by XCMPLX_1:27;
dom (f|X) c= X by RELAT_1:87;
then A42: x in X /\ dom (f|X) by A35,XBOOLE_1:28;
r2 in X /\ dom (f|X) by A24,XBOOLE_0:def 3;
then A43: (f|X).x <= (f|X).r2 by A10,A39,A41,A42,RFUNCT_2:def 4;
r1 in X /\ dom (f|X) by A23,XBOOLE_0:def 3;
then (f|X).r1 <= (f|X).x by A10,A38,A39,A42,RFUNCT_2:def 4;
then (f|X).x in {s: M1 <= s & s <= M2} by A23,A24,A43;
then (f|X).x in [.M1,M2.] by RCOMP_1:def 1;
then (f|X).x in N3 by A13,A22;
hence (f|X).x in N1 by A12;
suppose A44: (f|X).x0 = p;
then consider r be real number such that
A45: r > 0 & N1 = ].p - r,p + r.[ by RCOMP_1:def 7;
reconsider r as Real by XREAL_0:def 1;
set R = r/2;
A46: 0 < R by A45,SEQ_2:3;
A47: R < r by A45,SEQ_2:4;
then A48: p + R < p + r by REAL_1:53;
A49: p - r < p by A45,SQUARE_1:29;
A50: p < p + R by A46,REAL_1:69; then p - r < p + R by A49,AXIOMS:22
;
then p + R in {s: p - r < s & s < p + r} by A48;
then A51: p + R in ].p - r, p + r.[ by RCOMP_1:def 2;
A52: p - R < p by A46,SQUARE_1:29; p < p + r by A45,REAL_1:69;
then A53: p - R < p + r by A52,AXIOMS:22;
p - r < p - R by A47,REAL_1:92;
then p - R in {s: p - r < s & s < p + r} by A53;
then p - R in ].p - r, p + r.[ by RCOMP_1:def 2;
then A54: [.p - R, p + R.] c= N1 by A45,A51,RCOMP_1:17;
p - R in {s : s < p} by A52;
then p - R in L by PROB_1:def 15;
then consider r1 such that
A55: r1 in dom (f|X) & r1 in
X & p - R = (f|X).r1 by A2,A6,A8,PARTFUN2:78;
A56: r1 <> x0 by A44,A46,A55,SQUARE_1:29;
now assume
A57: x0 < r1;
A58: x0 in X /\ dom (f|X) by A3,A4,XBOOLE_0:def 3;
r1 in X /\ dom (f|X) by A55,XBOOLE_0:def 3;
hence contradiction by A9,A10,A44,A52,A55,A57,A58,RFUNCT_2:def 4;
end;
then r1 < x0 by A56,REAL_1:def 5; then x0 - r1 > 0 by SQUARE_1:11;
then reconsider N = ].x0 - (x0 - r1),x0 + (x0 - r1).[ as
Neighbourhood of x0 by RCOMP_1:def 7;
take N;
let x be real number such that
A59: x in dom(f|X) & x in N;
A60: x is Real by XREAL_0:def 1;
A61: dom (f|X) c= X by RELAT_1:87;
then (f|X).x in l by A2,A6,A59,FUNCT_1:def 12;
then (f|X).x in {s: s <= p} by LIMFUNC1:def 1;
then ex s st s = (f|X).x & s <= p;
then A62: (f|X).x <= p + R by A50,AXIOMS:22;
A63: x in X /\ dom (f|X) by A59,A61,XBOOLE_0:def 3;
A64: r1 in X /\ dom (f|X) by A55,XBOOLE_0:def 3;
x in {s: x0 - (x0-r1) < s & s < x0 + (x0-r1)} by A59,RCOMP_1:def 2
;
then ex s st s = x & x0 - (x0-r1) < s & s < x0 + (x0-r1);
then r1 < x by XCMPLX_1:18;
then p - R <= (f|X).x by A10,A55,A60,A63,A64,RFUNCT_2:def 4;
then (f|X).x in {s: p - R <= s & s <= p + R} by A62;
then (f|X).x in [.p - R, p + R.] by RCOMP_1:def 1;
hence (f|X).x in N1 by A54;
end;
hence ex N being Neighbourhood of x0 st
for r1 be real number st r1 in dom(f|X) & r1 in N holds (f|X).r1 in N1;
suppose f is_non_increasing_on X;
then A65: f|X is_non_increasing_on X by RFUNCT_2:53;
now per cases by A7,TARSKI:def 1;
suppose (f|X).x0 in L;
then consider N2 being Neighbourhood of (f|X).x0 such that
A66: N2 c= L by RCOMP_1:39;
consider N3 being Neighbourhood of (f|X).x0 such that
A67: N3 c= N1 & N3 c= N2 by RCOMP_1:38;
consider r be real number such that
A68: r > 0 & N3 = ].(f|X).x0 - r,(f|X).x0 + r.[ by RCOMP_1:def 7;
reconsider r as Real by XREAL_0:def 1;
set M1 = (f|X).x0 - r/2;
set M2 = (f|X).x0 + r/2;
A69: r/2 > 0 by A68,SEQ_2:3;
then (f|X).x0 - r < (f|X).x0 - r + r/2 by REAL_1:69;
then (f|X).x0 - r < (f|X).x0 - (r/2 + r/2) + r/2 by XCMPLX_1:66;
then (f|X).x0 - r < (f|X).x0 - (r/2 + r/2 - r/2) by XCMPLX_1:37;
then A70: (f|X).x0 - r < (f|X).x0 - r/2 by XCMPLX_1:26;
A71: (f|X).x0 < (f|X).x0 + r/2 by A69,REAL_1:69;
then A72: (f|X).x0 - r/2 < (f|X).x0 by REAL_1:84;
A73: (f|X).x0 < (f|X).x0 + r by A68,REAL_1:69;
then (f|X).x0 - r/2 < (f|X).x0 + r by A72,AXIOMS:22;
then (f|X).x0 - r/2 in {s: (f|X).x0 - r < s & s < (f|X).x0 + r} by
A70;
then A74: M1 in ].(f|X).x0 - r,(f|X).x0 + r.[ by RCOMP_1:def 2;
(f|X).x0 + r/2 < (f|X).x0 + r/2 + r/2 by A69,REAL_1:69;
then (f|X).x0 + r/2 < (f|X).x0 + (r/2 + r/2) by XCMPLX_1:1;
then A75: (f|X).x0 + r/2 < (f|X).x0 + r by XCMPLX_1:66;
(f|X).x0 - r < (f|X).x0 + r - r by A73,REAL_1:54;
then (f|X).x0 - r < (f|X).x0 by XCMPLX_1:26;
then (f|X).x0 - r < (f|X).x0 + r/2 by A71,AXIOMS:22;
then (f|X).x0 + r/2 in {s: (f|X).x0 - r < s & s < (f|X).x0 + r} by
A75;
then A76: M2 in ].(f|X).x0 - r,(f|X).x0 + r.[ by RCOMP_1:def 2;
then A77: [.M1,M2.] c= ].(f|X).x0 - r,(f|X).x0 + r.[ by A74,RCOMP_1:
17;
M1 in N2 by A67,A68,A74;
then M1 in L by A66;
then consider r1 such that
A78: r1 in dom (f|X) & r1 in
X & M1 = (f|X).r1 by A2,A6,A8,PARTFUN2:78;
M2 in N2 by A67,A68,A76;
then M2 in L by A66;
then consider r2 such that
A79: r2 in dom (f|X) & r2 in
X & M2 = (f|X).r2 by A2,A6,A8,PARTFUN2:78;
set R = min(r1 - x0,x0 - r2);
A80: (f|X).x0 < (f|X).x0 + r/2 by A69,REAL_1:69;
then A81: M1 < (f|X).x0 by REAL_1:84;
A82: r1 <> x0 by A78,A80,REAL_1:84;
now assume
A83: x0 > r1;
A84: x0 in X /\ dom (f|X) by A3,A4,XBOOLE_0:def 3;
r1 in X /\ dom(f|X) by A78,XBOOLE_0:def 3;
hence contradiction by A9,A65,A78,A81,A83,A84,RFUNCT_2:def 5;
end;
then r1 > x0 by A82,REAL_1:def 5;
then A85: r1 - x0 > 0 by SQUARE_1:11;
A86: M2 > (f|X).x0 by A69,REAL_1:69;
A87: x0 <> r2 by A69,A79,REAL_1:69;
now assume
A88: r2 > x0;
A89: x0 in X /\ dom (f|X) by A3,A4,XBOOLE_0:def 3;
r2 in X /\ dom (f|X) by A79,XBOOLE_0:def 3;
hence contradiction by A9,A65,A79,A86,A88,A89,RFUNCT_2:def 5;
end;
then x0 > r2 by A87,REAL_1:def 5;
then x0 - r2 > 0 by SQUARE_1:11;
then R > 0 by A85,SQUARE_1:38;
then reconsider N =].x0 - R,x0 + R.[ as Neighbourhood of x0 by
RCOMP_1:def 7;
take N;
let x be real number; assume
A90: x in dom (f|X) & x in N;
then x in {s: x0 - R < s & s < x0 + R} by RCOMP_1:def 2;
then A91: ex s st s = x & x0 - R < s & s < x0 + R;
then x0 < R + x by REAL_1:84;
then x0 - x < R + x - x by REAL_1:54;
then A92: x0 - x < R by XCMPLX_1:26; R <= x0 - r2 by SQUARE_1:35;
then x0 - x < x0 - r2 by A92,AXIOMS:22;
then -(x0 - x) > -(x0 - r2) by REAL_1:50;
then x - x0 > - (x0 - r2) by XCMPLX_1:143;
then x - x0 > r2 - x0 by XCMPLX_1:143;
then x - x0 + x0 > r2 - x0 + x0 by REAL_1:53;
then x > r2 - x0 + x0 by XCMPLX_1:27;
then A93: x > r2 by XCMPLX_1:27;
A94: x - x0 < R by A91,REAL_1:84; R <= r1 - x0 by SQUARE_1:35;
then x - x0 < r1-x0 by A94,AXIOMS:22;
then x - x0 + x0 < r1 - x0 + x0 by REAL_1:53;
then x < r1 - x0 + x0 by XCMPLX_1:27;
then A95: x < r1 by XCMPLX_1:27;
dom (f|X) c= X by RELAT_1:87;
then A96: x in X /\ dom(f|X) by A90,XBOOLE_1:28;
A97: x is Real by XREAL_0:def 1;
r2 in X /\ dom(f|X) by A79,XBOOLE_0:def 3;
then A98: (f|X).x <= (f|X).r2 by A65,A93,A96,A97,RFUNCT_2:def 5;
r1 in X /\ dom(f|X) by A78,XBOOLE_0:def 3;
then (f|X).r1 <= (f|X).x by A65,A95,A96,A97,RFUNCT_2:def 5;
then (f|X).x in {s: M1 <= s & s <= M2} by A78,A79,A98;
then (f|X).x in [.M1,M2.] by RCOMP_1:def 1;
then (f|X).x in N3 by A68,A77;
hence (f|X).x in N1 by A67;
suppose A99: (f|X).x0 = p;
then consider r be real number such that
A100: r > 0 & N1 = ].p - r,p + r.[ by RCOMP_1:def 7;
reconsider r as Real by XREAL_0:def 1;
set R = r/2;
A101: 0 < R by A100,SEQ_2:3;
A102: R < r by A100,SEQ_2:4;
then A103: p + R < p + r by REAL_1:53;
A104: p - r < p by A100,SQUARE_1:29;
A105: p < p + R by A101,REAL_1:69; then p - r < p + R by A104,AXIOMS:
22;
then p + R in {s: p - r < s & s < p + r} by A103;
then A106: p + R in ].p - r, p + r.[ by RCOMP_1:def 2;
A107: p - R < p by A101,SQUARE_1:29; p < p + r by A100,REAL_1:69
;
then A108: p - R < p + r by A107,AXIOMS:22;
p - r < p - R by A102,REAL_1:92;
then p - R in {s: p - r < s & s < p + r} by A108;
then p - R in ].p - r, p + r.[ by RCOMP_1:def 2;
then A109: [.p - R, p + R.] c= N1 by A100,A106,RCOMP_1:17;
p - R in {s : s < p} by A107;
then p - R in L by PROB_1:def 15;
then consider r1 such that
A110: r1 in dom (f|X) & r1 in X & p - R = (f|X).r1 by A2,A6,A8,
PARTFUN2:78;
A111: r1 <> x0 by A99,A101,A110,SQUARE_1:29;
now assume
A112: x0 > r1;
A113: x0 in X /\ dom (f|X) by A3,A4,XBOOLE_0:def 3;
r1 in X /\ dom (f|X) by A110,XBOOLE_0:def 3;
hence contradiction by A9,A65,A99,A107,A110,A112,A113,RFUNCT_2:def
5;
end;
then r1 > x0 by A111,REAL_1:def 5; then r1 - x0 > 0 by SQUARE_1:11;
then reconsider N = ].x0 - (r1 - x0),x0 + (r1 - x0).[ as
Neighbourhood of x0 by RCOMP_1:def 7;
take N;
let x be real number such that
A114: x in dom(f|X) & x in N;
A115: x is Real by XREAL_0:def 1;
A116: dom (f|X) c= X by RELAT_1:87;
then (f|X).x in l by A2,A6,A114,FUNCT_1:def 12;
then (f|X).x in {s: s <= p} by LIMFUNC1:def 1;
then ex s st s = (f|X).x & s <= p;
then A117: (f|X).x <= p + R by A105,AXIOMS:22;
A118: x in X /\ dom (f|X) by A114,A116,XBOOLE_0:def 3;
A119: r1 in X /\ dom (f|X) by A110,XBOOLE_0:def 3;
x in {s: x0 - (r1-x0) < s & s < x0 + (r1-x0)} by A114,RCOMP_1:def 2
;
then ex s st s = x & x0 - (r1-x0) < s & s < x0 + (r1-x0);
then r1 > x by XCMPLX_1:27;
then p - R <= (f|X).x by A65,A110,A115,A118,A119,RFUNCT_2:def 5;
then (f|X).x in {s: p - R <= s & s <= p + R} by A117;
then (f|X).x in [.p - R, p + R.] by RCOMP_1:def 1;
hence (f|X).x in N1 by A109;
end;
hence ex N being Neighbourhood of x0 st
for r1 be real number st r1 in dom(f|X) & r1 in N holds (f|X).r1 in N1;
end;
hence ex N being Neighbourhood of x0 st
for r1 be real number st r1 in dom(f|X) & r1 in N holds (f|X).r1 in N1;
end;
hence thesis by A4,FCONT_1:4;
end;
hence f is_continuous_on X by A1,FCONT_1:def 2;
end;
theorem Th22:
X c= dom f & f is_monotone_on X &
(ex p st f.:X = right_closed_halfline(p)) implies f is_continuous_on X
proof assume
A1: X c= dom f & f is_monotone_on X;
given p such that
A2: f.:X = right_closed_halfline(p);
set l = right_closed_halfline(p);
set L = right_open_halfline(p);
for x0 be real number st x0 in X holds f|X is_continuous_in x0
proof let x0 be real number;
A3: x0 is Real by XREAL_0:def 1;
assume
A4: x0 in X;
then x0 in dom f /\ X by A1,XBOOLE_0:def 3;
then A5: x0 in dom (f|X) by RELAT_1:90;
then A6: (f|X).x0 in (f|X).:X by A4,FUNCT_1:def 12;
A7: (f|X).:X = f.:X by RFUNCT_2:5;
then (f|X).x0 in {p} \/ L by A2,A6,Th12;
then A8: (f|X).x0 in {p} or (f|X).x0 in L by XBOOLE_0:def 2;
A9: L c= l by LIMFUNC1:10;
now let N1 be Neighbourhood of (f|X).x0;
now per cases by A1,RFUNCT_2:def 6;
suppose f is_non_decreasing_on X;
then A10: f|X is_non_decreasing_on X by RFUNCT_2:52;
now per cases by A8,TARSKI:def 1;
suppose (f|X).x0 in L;
then consider N2 being Neighbourhood of (f|X).x0 such that
A11: N2 c= L by RCOMP_1:39;
consider N3 being Neighbourhood of (f|X).x0 such that
A12: N3 c= N1 & N3 c= N2 by RCOMP_1:38;
consider r be real number such that
A13: r>0 & N3 = ].(f|X).x0 - r,(f|X).x0 + r.[ by RCOMP_1:def 7;
reconsider r as Real by XREAL_0:def 1;
set M1 = (f|X).x0 - r/2;
set M2 = (f|X).x0 + r/2;
A14: r/2 > 0 by A13,SEQ_2:3;
then (f|X).x0 - r < (f|X).x0 - r + r/2 by REAL_1:69;
then (f|X).x0 - r < (f|X).x0 - (r/2 + r/2) + r/2 by XCMPLX_1:66;
then (f|X).x0 - r < (f|X).x0 - (r/2 + r/2 - r/2) by XCMPLX_1:37;
then A15: (f|X).x0 - r < (f|X).x0 - r/2 by XCMPLX_1:26;
A16: (f|X).x0 < (f|X).x0 + r/2 by A14,REAL_1:69;
then A17: (f|X).x0 - r/2 < (f|X).x0 by REAL_1:84;
A18: (f|X).x0 < (f|X).x0 + r by A13,REAL_1:69;
then (f|X).x0 - r/2 < (f|X).x0 + r by A17,AXIOMS:22;
then (f|X).x0 - r/2 in {s: (f|X).x0 - r < s & s < (f|X).x0 + r} by
A15
;
then A19: M1 in ].(f|X).x0 - r,(f|X).x0 + r.[ by RCOMP_1:def 2;
(f|X).x0 + r/2 < (f|X).x0 + r/2 + r/2 by A14,REAL_1:69;
then (f|X).x0 + r/2 < (f|X).x0 + (r/2 + r/2) by XCMPLX_1:1;
then A20: (f|X).x0 + r/2 < (f|X).x0 + r by XCMPLX_1:66;
(f|X).x0 - r < (f|X).x0 + r - r by A18,REAL_1:54;
then (f|X).x0 - r < (f|X).x0 by XCMPLX_1:26;
then (f|X).x0 - r < (f|X).x0 + r/2 by A16,AXIOMS:22;
then (f|X).x0 + r/2 in {s: (f|X).x0 - r < s & s < (f|X).x0 + r} by
A20
;
then A21: M2 in ].(f|X).x0 - r,(f|X).x0 + r.[ by RCOMP_1:def 2;
then A22: [.M1,M2.] c= ].(f|X).x0 - r,(f|X).x0 + r.[ by A19,RCOMP_1:
17;
M1 in N2 by A12,A13,A19;
then M1 in L by A11;
then consider r1 such that
A23: r1 in dom (f|X) & r1 in
X & M1 = (f|X).r1 by A2,A7,A9,PARTFUN2:78;
M2 in N2 by A12,A13,A21;
then M2 in L by A11;
then consider r2 such that
A24: r2 in dom (f|X) & r2 in
X & M2 = (f|X).r2 by A2,A7,A9,PARTFUN2:78;
set R = min(x0 - r1,r2 - x0);
A25: (f|X).x0 < (f|X).x0 + r/2 by A14,REAL_1:69;
then A26: M1 < (f|X).x0 by REAL_1:84;
A27: r1 <> x0 by A23,A25,REAL_1:84;
now assume
A28: x0 < r1;
A29: x0 in X /\ dom( f|X) by A4,A5,XBOOLE_0:def 3;
r1 in X /\ dom(f|X) by A23,XBOOLE_0:def 3;
hence contradiction by A3,A10,A23,A26,A28,A29,RFUNCT_2:def 4;
end;
then r1 < x0 by A27,REAL_1:def 5;
then A30: x0 - r1 > 0 by SQUARE_1:11;
A31: M2 > (f|X).x0 by A14,REAL_1:69;
A32: x0 <> r2 by A14,A24,REAL_1:69;
now assume
A33: r2 < x0;
A34: x0 in X /\ dom(f|X) by A4,A5,XBOOLE_0:def 3;
r2 in X /\ dom (f|X) by A24,XBOOLE_0:def 3;
hence contradiction by A3,A10,A24,A31,A33,A34,RFUNCT_2:def 4;
end;
then x0 < r2 by A32,REAL_1:def 5;
then r2 - x0 > 0 by SQUARE_1:11;
then R > 0 by A30,SQUARE_1:38;
then reconsider N = ].x0 - R,x0+ R.[ as Neighbourhood of x0 by
RCOMP_1:def 7;
take N;
let x be real number; assume
A35: x in dom (f|X) & x in N;
then x in {s: x0 - R < s & s < x0 + R} by RCOMP_1:def 2;
then A36: ex s st s = x & x0 - R < s & s < x0 + R;
then x0 < R + x by REAL_1:84;
then x0 - x < R + x - x by REAL_1:54
;
then A37: x0 - x < R by XCMPLX_1:26; R <= x0 - r1 by SQUARE_1:35;
then x0 - x < x0 - r1 by A37,AXIOMS:22;
then -(x0 - x) > -(x0 - r1) by REAL_1:50;
then x - x0 > -(x0 - r1) by XCMPLX_1:143;
then x - x0 > r1 - x0 by XCMPLX_1:143;
then x - x0 + x0 > r1 - x0 + x0 by REAL_1:53;
then x > r1 - x0 + x0 by XCMPLX_1:27;
then A38: x > r1 by XCMPLX_1:27;
A39: x is Real by XREAL_0:def 1;
A40: x - x0 < R by A36,REAL_1:84; R <= r2 - x0 by SQUARE_1:35;
then x - x0 < r2 - x0 by A40,AXIOMS:22;
then x - x0 + x0 < r2 - x0 + x0 by REAL_1:53;
then x < r2 - x0 + x0 by XCMPLX_1:27;
then A41: x < r2 by XCMPLX_1:27;
dom (f|X) c= X by RELAT_1:87;
then A42: x in X /\ dom (f|X) by A35,XBOOLE_1:28;
r2 in X /\ dom (f|X) by A24,XBOOLE_0:def 3;
then A43: (f|X).x <= (f|X).r2 by A10,A39,A41,A42,RFUNCT_2:def 4;
r1 in X /\ dom (f|X) by A23,XBOOLE_0:def 3;
then (f|X).r1 <= (f|X).x by A10,A38,A39,A42,RFUNCT_2:def 4;
then (f|X).x in {s: M1 <= s & s <= M2} by A23,A24,A43;
then (f|X).x in [.M1,M2.] by RCOMP_1:def 1;
then (f|X).x in N3 by A13,A22;
hence (f|X).x in N1 by A12;
suppose A44: (f|X).x0 = p;
then consider r be real number such that
A45: r > 0 & N1 = ].p - r,p + r.[ by RCOMP_1:def 7;
reconsider r as Real by XREAL_0:def 1;
set R = r/2;
A46: 0 < R by A45,SEQ_2:3;
A47: R < r by A45,SEQ_2:4;
then A48: p + R < p + r by REAL_1:53;
A49: p - r < p by A45,SQUARE_1:29;
A50: p < p + R by A46,REAL_1:69; then p - r < p + R by A49,AXIOMS:22
;
then p + R in {s: p - r < s & s < p + r} by A48;
then A51: p + R in ].p - r, p + r.[ by RCOMP_1:def 2;
A52: p - R < p by A46,SQUARE_1:29; p < p + r by A45,REAL_1:69;
then A53: p - R < p + r by A52,AXIOMS:22;
p - r < p - R by A47,REAL_1:92;
then p - R in {s: p - r < s & s < p + r} by A53;
then p - R in ].p - r, p + r.[ by RCOMP_1:def 2;
then A54: [.p - R, p + R.] c= N1 by A45,A51,RCOMP_1:17;
p + R in {s : p < s} by A50;
then p + R in L by LIMFUNC1:def 3;
then consider r1 such that
A55: r1 in dom (f|X) & r1 in
X & p + R = (f|X).r1 by A2,A7,A9,PARTFUN2:78;
A56: r1 <> x0 by A44,A46,A55,REAL_1:69;
now assume
A57: x0 > r1;
A58: x0 in X /\ dom (f|X) by A4,A5,XBOOLE_0:def 3;
r1 in X /\ dom (f|X) by A55,XBOOLE_0:def 3;
hence contradiction by A3,A10,A44,A50,A55,A57,A58,RFUNCT_2:def 4;
end;
then r1 > x0 by A56,REAL_1:def 5; then r1 - x0 > 0 by SQUARE_1:11;
then reconsider N = ].x0 - (r1 - x0),x0 + (r1 - x0).[ as
Neighbourhood of x0 by RCOMP_1:def 7;
take N;
let x be real number such that
A59: x in dom(f|X) & x in N;
A60: dom (f|X) c= X by RELAT_1:87;
then (f|X).x in l by A2,A7,A59,FUNCT_1:def 12;
then (f|X).x in {s: p <= s} by LIMFUNC1:def 2;
then ex s st s = (f|X).x & p <= s;
then A61: p - R <= (f|X).x by A52,AXIOMS:22;
A62: x in X /\ dom (f|X) by A59,A60,XBOOLE_0:def 3;
A63: r1 in X /\ dom (f|X) by A55,XBOOLE_0:def 3;
A64: x is Real by XREAL_0:def 1;
x in {s: x0 - (r1-x0) < s & s < x0 + (r1-x0)} by A59,RCOMP_1:def 2;
then ex s st s = x & x0 - (r1-x0) < s & s < x0 + (r1-x0);
then r1 > x by XCMPLX_1:27;
then p + R >= (f|X).x by A10,A55,A62,A63,A64,RFUNCT_2:def 4;
then (f|X).x in {s: p - R <= s & s <= p + R} by A61;
then (f|X).x in [.p - R, p + R.] by RCOMP_1:def 1;
hence (f|X).x in N1 by A54;
end;
hence ex N being Neighbourhood of x0 st
for r1 be real number st r1 in dom(f|X) & r1 in N holds (f|X).r1 in N1;
suppose f is_non_increasing_on X;
then A65: f|X is_non_increasing_on X by RFUNCT_2:53;
now per cases by A8,TARSKI:def 1;
suppose (f|X).x0 in L;
then consider N2 being Neighbourhood of (f|X).x0 such that
A66: N2 c= L by RCOMP_1:39;
consider N3 being Neighbourhood of (f|X).x0 such that
A67: N3 c= N1 & N3 c= N2 by RCOMP_1:38;
consider r be real number such that
A68: r > 0 & N3 = ].(f|X).x0 - r,(f|X).x0 + r.[ by RCOMP_1:def 7;
reconsider r as Real by XREAL_0:def 1;
set M1 = (f|X).x0 - r/2;
set M2 = (f|X).x0 + r/2;
A69: r/2 > 0 by A68,SEQ_2:3;
then (f|X).x0 - r < (f|X).x0 - r + r/2 by REAL_1:69;
then (f|X).x0 - r < (f|X).x0 - (r/2 + r/2) + r/2 by XCMPLX_1:66;
then (f|X).x0 - r < (f|X).x0 - (r/2 + r/2 - r/2) by XCMPLX_1:37;
then A70: (f|X).x0 - r < (f|X).x0 - r/2 by XCMPLX_1:26;
A71: (f|X).x0 < (f|X).x0 + r/2 by A69,REAL_1:69;
then A72: (f|X).x0 - r/2 < (f|X).x0 by REAL_1:84;
A73: (f|X).x0 < (f|X).x0 + r by A68,REAL_1:69;
then (f|X).x0 - r/2 < (f|X).x0 + r by A72,AXIOMS:22;
then (f|X).x0 - r/2 in {s: (f|X).x0 - r < s & s < (f|X).x0 + r} by
A70
;
then A74: M1 in ].(f|X).x0 - r,(f|X).x0 + r.[ by RCOMP_1:def 2;
(f|X).x0 + r/2 < (f|X).x0 + r/2 + r/2 by A69,REAL_1:69;
then (f|X).x0 + r/2 < (f|X).x0 + (r/2 + r/2) by XCMPLX_1:1;
then A75: (f|X).x0 + r/2 < (f|X).x0 + r by XCMPLX_1:66;
(f|X).x0 - r < (f|X).x0 + r - r by A73,REAL_1:54;
then (f|X).x0 - r < (f|X).x0 by XCMPLX_1:26;
then (f|X).x0 - r < (f|X).x0 + r/2 by A71,AXIOMS:22;
then (f|X).x0 + r/2 in {s: (f|X).x0 - r < s & s < (f|X).x0 + r} by
A75
;
then A76: M2 in ].(f|X).x0 - r,(f|X).x0 + r.[ by RCOMP_1:def 2;
then A77: [.M1,M2.] c= ].(f|X).x0 - r,(f|X).x0 + r.[ by A74,RCOMP_1:
17;
M1 in N2 by A67,A68,A74;
then M1 in L by A66;
then consider r1 such that
A78: r1 in dom (f|X) & r1 in
X & M1 = (f|X).r1 by A2,A7,A9,PARTFUN2:78;
M2 in N2 by A67,A68,A76;
then M2 in L by A66;
then consider r2 such that
A79: r2 in dom (f|X) & r2 in
X & M2 = (f|X).r2 by A2,A7,A9,PARTFUN2:78;
set R = min(r1 - x0,x0 - r2);
A80: (f|X).x0 < (f|X).x0 + r/2 by A69,REAL_1:69;
then A81: M1 < (f|X).x0 by REAL_1:84;
A82: r1 <> x0 by A78,A80,REAL_1:84;
now assume
A83: x0 > r1;
A84: x0 in X /\ dom (f|X) by A4,A5,XBOOLE_0:def 3;
r1 in X /\ dom(f|X) by A78,XBOOLE_0:def 3;
hence contradiction by A3,A65,A78,A81,A83,A84,RFUNCT_2:def 5;
end;
then r1 > x0 by A82,REAL_1:def 5;
then A85: r1 - x0 > 0 by SQUARE_1:11;
A86: M2 > (f|X).x0 by A69,REAL_1:69;
A87: x0 <> r2 by A69,A79,REAL_1:69;
now assume
A88: r2 > x0;
A89: x0 in X /\ dom (f|X) by A4,A5,XBOOLE_0:def 3;
r2 in X /\ dom (f|X) by A79,XBOOLE_0:def 3;
hence contradiction by A3,A65,A79,A86,A88,A89,RFUNCT_2:def 5;
end;
then x0 > r2 by A87,REAL_1:def 5;
then x0 - r2 > 0 by SQUARE_1:11;
then R > 0 by A85,SQUARE_1:38;
then reconsider N =].x0 - R,x0 + R.[ as Neighbourhood of x0 by
RCOMP_1:def 7;
take N;
let x be real number; assume
A90: x in dom (f|X) & x in N;
then x in {s: x0 - R < s & s < x0 + R} by RCOMP_1:def 2;
then A91: ex s st s = x & x0 - R < s & s < x0 + R;
then x0 < R + x by REAL_1:84;
then x0 - x < R + x - x by REAL_1:54;
then A92: x0 - x < R by XCMPLX_1:26; R <= x0 - r2 by SQUARE_1:35;
then x0 - x < x0 - r2 by A92,AXIOMS:22;
then -(x0 - x) > -(x0 - r2) by REAL_1:50;
then x - x0 > - (x0 - r2) by XCMPLX_1:143;
then x - x0 > r2 - x0 by XCMPLX_1:143;
then x - x0 + x0 > r2 - x0 + x0 by REAL_1:53;
then x > r2 - x0 + x0 by XCMPLX_1:27;
then A93: x > r2 by XCMPLX_1:27;
A94: x is Real by XREAL_0:def 1;
A95: x - x0 < R by A91,REAL_1:84; R <= r1 - x0 by SQUARE_1:35;
then x - x0 < r1-x0 by A95,AXIOMS:22;
then x - x0 + x0 < r1 - x0 + x0 by REAL_1:53;
then x < r1 - x0 + x0 by XCMPLX_1:27;
then A96: x < r1 by XCMPLX_1:27;
dom (f|X) c= X by RELAT_1:87;
then A97: x in X /\ dom(f|X) by A90,XBOOLE_1:28;
r2 in X /\ dom(f|X) by A79,XBOOLE_0:def 3;
then A98: (f|X).x <= (f|X).r2 by A65,A93,A94,A97,RFUNCT_2:def 5;
r1 in X /\ dom(f|X) by A78,XBOOLE_0:def 3;
then (f|X).r1 <= (f|X).x by A65,A94,A96,A97,RFUNCT_2:def 5;
then (f|X).x in {s: M1 <= s & s <= M2} by A78,A79,A98;
then (f|X).x in [.M1,M2.] by RCOMP_1:def 1;
then (f|X).x in N3 by A68,A77;
hence (f|X).x in N1 by A67;
suppose A99: (f|X).x0 = p;
then consider r be real number such that
A100: r > 0 & N1 = ].p - r,p + r.[ by RCOMP_1:def 7;
reconsider r as Real by XREAL_0:def 1;
set R = r/2;
A101: 0 < R by A100,SEQ_2:3;
A102: R < r by A100,SEQ_2:4;
then A103: p + R < p + r by REAL_1:53;
A104: p - r < p by A100,SQUARE_1:29;
A105: p < p + R by A101,REAL_1:69; then p - r < p + R by A104,AXIOMS:
22;
then p + R in {s: p - r < s & s < p + r} by A103;
then A106: p + R in ].p - r, p + r.[ by RCOMP_1:def 2;
A107: p - R < p by A101,SQUARE_1:29; p < p + r by A100,REAL_1:69
;
then A108: p - R < p + r by A107,AXIOMS:22;
p - r < p - R by A102,REAL_1:92;
then p - R in {s: p - r < s & s < p + r} by A108;
then p - R in ].p - r, p + r.[ by RCOMP_1:def 2;
then A109: [.p - R, p + R.] c= N1 by A100,A106,RCOMP_1:17;
p + R in {s : p < s} by A105;
then p + R in L by LIMFUNC1:def 3;
then consider r1 such that
A110: r1 in dom (f|X) & r1 in X & p + R = (f|X).r1 by A2,A7,A9,
PARTFUN2:78;
A111: r1 <> x0 by A99,A101,A110,REAL_1:69;
now assume
A112: x0 < r1;
A113: x0 in X /\ dom (f|X) by A4,A5,XBOOLE_0:def 3;
r1 in X /\ dom (f|X) by A110,XBOOLE_0:def 3;
hence contradiction by A3,A65,A99,A105,A110,A112,A113,RFUNCT_2:def
5;
end;
then r1 < x0 by A111,REAL_1:def 5; then x0 - r1 > 0 by SQUARE_1:11;
then reconsider N = ].x0 - (x0 - r1),x0 + (x0 - r1).[ as
Neighbourhood of x0 by RCOMP_1:def 7;
take N;
let x be real number such that
A114: x in dom(f|X) & x in N;
A115: x is Real by XREAL_0:def 1;
A116: dom (f|X) c= X by RELAT_1:87;
then (f|X).x in l by A2,A7,A114,FUNCT_1:def 12;
then (f|X).x in {s: p <= s} by LIMFUNC1:def 2;
then ex s st s = (f|X).x & p <= s;
then A117: p - R <= (f|X).x by A107,AXIOMS:22;
A118: x in X /\ dom (f|X) by A114,A116,XBOOLE_0:def 3;
A119: r1 in X /\ dom (f|X) by A110,XBOOLE_0:def 3;
x in {s: x0 - (x0-r1) < s & s < x0 + (x0-r1)} by A114,RCOMP_1:def 2
;
then ex s st s = x & x0 - (x0-r1) < s & s < x0 + (x0-r1);
then r1 < x by XCMPLX_1:18;
then p + R >= (f|X).x by A65,A110,A115,A118,A119,RFUNCT_2:def 5;
then (f|X).x in {s: p - R <= s & s <= p + R} by A117;
then (f|X).x in [.p - R, p + R.] by RCOMP_1:def 1;
hence (f|X).x in N1 by A109;
end;
hence ex N being Neighbourhood of x0 st
for r1 be real number st r1 in dom(f|X) & r1 in N holds (f|X).r1 in N1;
end;
hence ex N being Neighbourhood of x0 st
for r1 be real number st r1 in dom(f|X) & r1 in N holds (f|X).r1 in N1;
end;
hence thesis by A5,FCONT_1:4;
end;
hence f is_continuous_on X by A1,FCONT_1:def 2;
end;
theorem Th23:
X c= dom f & f is_monotone_on X & (ex p,g st f.:X = ].p,g.[) implies
f is_continuous_on X
proof assume
A1: X c= dom f & f is_monotone_on X;
given p,g such that
A2: f.:X = ].p,g.[;
set L = ].p,g.[;
now per cases by A1,RFUNCT_2:def 6;
suppose f is_non_decreasing_on X;
then A3: f|X is_non_decreasing_on X by RFUNCT_2:52;
for x0 be real number st x0 in X holds f|X is_continuous_in x0
proof let x0 be real number; assume
A4: x0 in X;
then x0 in dom f /\ X by A1,XBOOLE_0:def 3;
then A5: x0 in dom (f|X) by RELAT_1:90;
then A6: (f|X).x0 in (f|X).:X by A4,FUNCT_1:def 12;
A7: x0 is Real by XREAL_0:def 1;
A8: (f|X).:X = f.:X by RFUNCT_2:5;
A9: (f|X).x0 in L by A2,A6,RFUNCT_2:5;
now let N1 be Neighbourhood of (f|X).x0;
consider N2 being Neighbourhood of (f|X).x0 such that
A10: N2 c= L by A9,RCOMP_1:39;
consider N3 being Neighbourhood of (f|X).x0 such that
A11: N3 c= N1 & N3 c= N2 by RCOMP_1:38;
consider r be real number such that
A12: r>0 & N3 = ].(f|X).x0 - r,(f|X).x0 + r.[ by RCOMP_1:def 7;
reconsider r as Real by XREAL_0:def 1;
set M1 = (f|X).x0 - r/2;
set M2 = (f|X).x0 + r/2;
A13: r/2 > 0 by A12,SEQ_2:3;
then (f|X).x0 - r < (f|X).x0 - r + r/2 by REAL_1:69;
then (f|X).x0 - r < (f|X).x0 - (r/2 + r/2) + r/2 by XCMPLX_1:66;
then (f|X).x0 - r < (f|X).x0 - (r/2 + r/2 - r/2) by XCMPLX_1:37;
then A14: (f|X).x0 - r < (f|X).x0 - r/2 by XCMPLX_1:26;
A15: (f|X).x0 < (f|X).x0 + r/2 by A13,REAL_1:69;
then A16: (f|X).x0 - r/2 < (f|X).x0 by REAL_1:84;
A17: (f|X).x0 < (f|X).x0 + r by A12,REAL_1:69;
then (f|X).x0 - r/2 < (f|X).x0 + r by A16,AXIOMS:22;
then (f|X).x0 - r/2 in {s: (f|X).x0 - r < s & s < (f|X).x0 + r} by A14
;
then A18: M1 in ].(f|X).x0 - r,(f|X).x0 + r.[ by RCOMP_1:def 2;
(f|X).x0 + r/2 < (f|X).x0 + r/2 + r/2 by A13,REAL_1:69;
then (f|X).x0 + r/2 < (f|X).x0 + (r/2 + r/2) by XCMPLX_1:1;
then A19: (f|X).x0 + r/2 < (f|X).x0 + r by XCMPLX_1:66;
(f|X).x0 - r < (f|X).x0 + r - r by A17,REAL_1:54;
then (f|X).x0 - r < (f|X).x0 by XCMPLX_1:26;
then (f|X).x0 - r < (f|X).x0 + r/2 by A15,AXIOMS:22;
then (f|X).x0 + r/2 in {s: (f|X).x0 - r < s & s < (f|X).x0 + r} by A19
;
then A20: M2 in ].(f|X).x0 - r,(f|X).x0 + r.[ by RCOMP_1:def 2;
then A21: [.M1,M2.] c= ].(f|X).x0 - r,(f|X).x0 + r.[ by A18,RCOMP_1:17;
M1 in N2 by A11,A12,A18;
then consider r1 such that
A22: r1 in dom (f|X) & r1 in
X & M1 = (f|X).r1 by A2,A8,A10,PARTFUN2:78;
M2 in N2 by A11,A12,A20;
then consider r2 such that
A23: r2 in dom (f|X) & r2 in
X & M2 = (f|X).r2 by A2,A8,A10,PARTFUN2:78;
set R = min(x0 - r1,r2 - x0);
A24: (f|X).x0 < (f|X).x0 + r/2 by A13,REAL_1:69;
then A25: M1 < (f|X).x0 by REAL_1:84;
A26: r1 <> x0 by A22,A24,REAL_1:84;
now assume
A27: x0 < r1;
A28: x0 in X /\ dom( f|X) by A4,A5,XBOOLE_0:def 3;
r1 in X /\ dom(f|X) by A22,XBOOLE_0:def 3;
hence contradiction by A3,A7,A22,A25,A27,A28,RFUNCT_2:def 4;
end;
then r1 < x0 by A26,REAL_1:def 5;
then A29: x0 - r1 > 0 by SQUARE_1:11;
A30: M2 > (f|X).x0 by A13,REAL_1:69;
A31: x0 <> r2 by A13,A23,REAL_1:69;
now assume
A32: r2 < x0;
A33: x0 in X /\ dom(f|X) by A4,A5,XBOOLE_0:def 3;
r2 in X /\ dom (f|X) by A23,XBOOLE_0:def 3;
hence contradiction by A3,A7,A23,A30,A32,A33,RFUNCT_2:def 4;
end;
then x0 < r2 by A31,REAL_1:def 5;
then r2 - x0 > 0 by SQUARE_1:11;
then R > 0 by A29,SQUARE_1:38;
then reconsider N = ].x0 - R,x0 + R.[ as Neighbourhood of x0 by RCOMP_1
:def 7;
take N;
let x be real number; assume
A34: x in dom (f|X) & x in N;
then x in {s: x0 - R < s & s < x0 + R} by RCOMP_1:def 2;
then A35: ex s st s = x & x0 - R < s & s < x0 + R;
then x0 < R + x by REAL_1:84
; then x0 - x < R + x - x by REAL_1:54
;
then A36: x0 - x < R by XCMPLX_1:26; R <= x0 - r1 by SQUARE_1:35;
then x0 - x < x0 - r1 by A36,AXIOMS:22;
then -(x0 - x) > -(x0 - r1) by REAL_1:50;
then x - x0 > -(x0 - r1) by XCMPLX_1:143;
then x - x0 > r1 - x0 by XCMPLX_1:143;
then x - x0 + x0 > r1 - x0 + x0 by REAL_1:53;
then x > r1 - x0 + x0 by XCMPLX_1:27;
then A37: x > r1 by XCMPLX_1:27;
A38: x is Real by XREAL_0:def 1;
A39: x - x0 < R by A35,REAL_1:84; R <= r2 - x0 by SQUARE_1:35;
then x - x0 < r2 - x0 by A39,AXIOMS:22;
then x - x0 + x0 < r2 - x0 + x0 by REAL_1:53;
then x < r2 - x0 + x0 by XCMPLX_1:27;
then A40: x < r2 by XCMPLX_1:27;
dom (f|X) c= X by RELAT_1:87;
then A41: x in X /\ dom (f|X) by A34,XBOOLE_1:28;
r2 in X /\ dom (f|X) by A23,XBOOLE_0:def 3;
then A42: (f|X).x <= (f|X).r2 by A3,A38,A40,A41,RFUNCT_2:def 4;
r1 in X /\ dom (f|X) by A22,XBOOLE_0:def 3;
then (f|X).r1 <= (f|X).x by A3,A37,A38,A41,RFUNCT_2:def 4;
then (f|X).x in {s: M1<=s & s<=M2} by A22,A23,A42;
then (f|X).x in [.M1,M2.] by RCOMP_1:def 1;
then (f|X).x in N3 by A12,A21;
hence (f|X).x in N1 by A11;
end;
hence thesis by A5,FCONT_1:4;
end;
hence f is_continuous_on X by A1,FCONT_1:def 2;
suppose f is_non_increasing_on X;
then A43: f|X is_non_increasing_on X by RFUNCT_2:53;
for x0 be real number st x0 in X holds f|X is_continuous_in x0
proof let x0 be real number; assume
A44: x0 in X;
then x0 in dom f /\ X by A1,XBOOLE_0:def 3;
then A45: x0 in dom(f|X) by RELAT_1:90;
then A46: (f|X).x0 in (f|X).:X by A44,FUNCT_1:def 12;
A47: (f|X).:X = f.:X by RFUNCT_2:5;
A48: x0 is Real by XREAL_0:def 1;
A49: (f|X).x0 in L by A2,A46,RFUNCT_2:5;
now let N1 be Neighbourhood of (f|X).x0;
consider N2 being Neighbourhood of (f|X).x0 such that
A50: N2 c= L by A49,RCOMP_1:39;
consider N3 being Neighbourhood of (f|X).x0 such that
A51: N3 c= N1 & N3 c= N2 by RCOMP_1:38;
consider r be real number such that
A52: r > 0 & N3 = ].(f|X).x0 - r,(f|X).x0 + r.[ by RCOMP_1:def 7;
reconsider r as Real by XREAL_0:def 1;
set M1 = (f|X).x0 - r/2;
set M2 = (f|X).x0 + r/2;
A53: r/2 > 0 by A52,SEQ_2:3;
then (f|X).x0 - r < (f|X).x0 - r + r/2 by REAL_1:69;
then (f|X).x0 - r < (f|X).x0 - (r/2 + r/2) + r/2 by XCMPLX_1:66;
then (f|X).x0 - r < (f|X).x0 - (r/2 + r/2 - r/2) by XCMPLX_1:37;
then A54: (f|X).x0 - r < (f|X).x0 - r/2 by XCMPLX_1:26;
A55: (f|X).x0 < (f|X).x0 + r/2 by A53,REAL_1:69;
then A56: (f|X).x0 - r/2 < (f|X).x0 by REAL_1:84;
A57: (f|X).x0 < (f|X).x0 + r by A52,REAL_1:69;
then (f|X).x0 - r/2 < (f|X).x0 + r by A56,AXIOMS:22;
then (f|X).x0 - r/2 in {s: (f|X).x0 - r < s & s < (f|X).x0 + r} by A54
;
then A58: M1 in ].(f|X).x0 - r,(f|X).x0 + r.[ by RCOMP_1:def 2;
(f|X).x0 + r/2 < (f|X).x0 + r/2 + r/2 by A53,REAL_1:69;
then (f|X).x0 + r/2 < (f|X).x0 + (r/2 + r/2) by XCMPLX_1:1;
then A59: (f|X).x0 + r/2 < (f|X).x0 + r by XCMPLX_1:66;
(f|X).x0 - r < (f|X).x0 + r - r by A57,REAL_1:54;
then (f|X).x0 - r < (f|X).x0 by XCMPLX_1:26;
then (f|X).x0 - r < (f|X).x0 + r/2 by A55,AXIOMS:22;
then (f|X).x0 + r/2 in {s: (f|X).x0 - r < s & s < (f|X).x0 + r} by A59
;
then A60: M2 in ].(f|X).x0 - r,(f|X).x0 + r.[ by RCOMP_1:def 2;
then A61: [.M1,M2.] c= ].(f|X).x0 - r,(f|X).x0 + r.[ by A58,RCOMP_1:17;
M1 in N2 by A51,A52,A58;
then consider r1 such that
A62: r1 in dom (f|X) & r1 in
X & M1 = (f|X).r1 by A2,A47,A50,PARTFUN2:78;
M2 in N2 by A51,A52,A60;
then consider r2 such that
A63: r2 in dom (f|X) & r2 in
X & M2 = (f|X).r2 by A2,A47,A50,PARTFUN2:78;
set R = min(r1 - x0,x0 - r2);
A64: (f|X).x0 < (f|X).x0 + r/2 by A53,REAL_1:69;
then A65: M1 < (f|X).x0 by REAL_1:84;
A66: r1 <> x0 by A62,A64,REAL_1:84;
now assume
A67: x0 > r1;
A68: x0 in X /\ dom (f|X) by A44,A45,XBOOLE_0:def 3;
r1 in X /\ dom(f|X) by A62,XBOOLE_0:def 3;
hence contradiction by A43,A48,A62,A65,A67,A68,RFUNCT_2:def 5;
end;
then r1 > x0 by A66,REAL_1:def 5;
then A69: r1 - x0 > 0 by SQUARE_1:11;
A70: M2 > (f|X).x0 by A53,REAL_1:69;
A71: x0 <> r2 by A53,A63,REAL_1:69;
now assume
A72: r2 > x0;
A73: x0 in X /\ dom (f|X) by A44,A45,XBOOLE_0:def 3;
r2 in X /\ dom (f|X) by A63,XBOOLE_0:def 3;
hence contradiction by A43,A48,A63,A70,A72,A73,RFUNCT_2:def 5;
end;
then x0 > r2 by A71,REAL_1:def 5;
then x0 - r2 > 0 by SQUARE_1:11;
then R > 0 by A69,SQUARE_1:38;
then reconsider N = ].x0 - R,x0 + R.[ as Neighbourhood of x0 by RCOMP_1
:def 7;
take N;
let x be real number; assume
A74: x in dom (f|X) & x in N;
then x in {s: x0 - R < s & s < x0 + R} by RCOMP_1:def 2;
then A75: ex s st s = x & x0 - R < s & s < x0 + R;
then x0 < R + x by REAL_1:84;
then x0 - x < R + x - x by REAL_1:54
;
then A76: x0 - x < R by XCMPLX_1:26; R <= x0 - r2 by SQUARE_1:35;
then x0 - x < x0 - r2 by A76,AXIOMS:22;
then -(x0 - x) > -(x0 - r2) by REAL_1:50;
then x - x0 > - (x0 - r2) by XCMPLX_1:143;
then x - x0 > r2 - x0 by XCMPLX_1:143;
then x - x0 + x0 > r2 - x0 + x0 by REAL_1:53;
then x > r2 - x0 + x0 by XCMPLX_1:27;
then A77: x > r2 by XCMPLX_1:27;
A78: x is Real by XREAL_0:def 1;
A79: x - x0 < R by A75,REAL_1:84; R <= r1 - x0 by SQUARE_1:35;
then x - x0 < r1-x0 by A79,AXIOMS:22;
then x - x0 + x0 < r1 - x0 + x0 by REAL_1:53;
then x < r1 - x0 + x0 by XCMPLX_1:27;
then A80: x < r1 by XCMPLX_1:27;
dom (f|X) c= X by RELAT_1:87;
then A81: x in X /\ dom(f|X) by A74,XBOOLE_1:28;
r2 in X /\ dom(f|X) by A63,XBOOLE_0:def 3;
then A82: (f|X).x <= (f|X).r2 by A43,A77,A78,A81,RFUNCT_2:def 5;
r1 in X /\ dom(f|X) by A62,XBOOLE_0:def 3;
then (f|X).r1 <= (f|X).x by A43,A78,A80,A81,RFUNCT_2:def 5;
then (f|X).x in {s: M1 <= s & s <= M2} by A62,A63,A82;
then (f|X).x in [.M1,M2.] by RCOMP_1:def 1;
then (f|X).x in N3 by A52,A61;
hence (f|X).x in N1 by A51;
end;
hence thesis by A45,FCONT_1:4;
end;
hence f is_continuous_on X by A1,FCONT_1:def 2;
end;
hence thesis;
end;
theorem Th24:
X c= dom f & f is_monotone_on X & f.:X = REAL implies
f is_continuous_on X
proof assume
A1: X c= dom f & f is_monotone_on X & f.:X = REAL;
now per cases by A1,RFUNCT_2:def 6;
suppose f is_non_decreasing_on X;
then A2: f|X is_non_decreasing_on X by RFUNCT_2:52;
for x0 be real number st x0 in X holds f|X is_continuous_in x0
proof let x0 be real number; assume
A3: x0 in X;
then x0 in dom f /\ X by A1,XBOOLE_0:def 3;
then A4: x0 in dom (f|X) by RELAT_1:90;
A5: (f|X).:X = f.:X by RFUNCT_2:5;
A6: x0 is Real by XREAL_0:def 1;
now let N1 be Neighbourhood of (f|X).x0;
consider r be real number such that
A7: r>0 & N1 = ].(f|X).x0 - r,(f|X).x0 + r.[ by RCOMP_1:def 7;
reconsider r as Real by XREAL_0:def 1;
set M1 = (f|X).x0 - r/2;
set M2 = (f|X).x0 + r/2;
A8: r/2 > 0 by A7,SEQ_2:3;
then (f|X).x0 - r < (f|X).x0 - r + r/2 by REAL_1:69;
then (f|X).x0 - r < (f|X).x0 - (r/2 + r/2) + r/2 by XCMPLX_1:66;
then (f|X).x0 - r < (f|X).x0 - (r/2 + r/2 - r/2) by XCMPLX_1:37;
then A9: (f|X).x0 - r < (f|X).x0 - r/2 by XCMPLX_1:26;
A10: (f|X).x0 < (f|X).x0 + r/2 by A8,REAL_1:69;
then A11: (f|X).x0 - r/2 < (f|X).x0 by REAL_1:84;
A12: (f|X).x0 < (f|X).x0 + r by A7,REAL_1:69;
then (f|X).x0 - r/2 < (f|X).x0 + r by A11,AXIOMS:22;
then (f|X).x0 - r/2 in {s: (f|X).x0 - r < s & s < (f|X).x0 + r} by A9;
then A13: M1 in ].(f|X).x0 - r,(f|X).x0 + r.[ by RCOMP_1:def 2;
(f|X).x0 + r/2 < (f|X).x0 + r/2 + r/2 by A8,REAL_1:69;
then (f|X).x0 + r/2 < (f|X).x0 + (r/2 + r/2) by XCMPLX_1:1;
then A14: (f|X).x0 + r/2 < (f|X).x0 + r by XCMPLX_1:66;
(f|X).x0 - r < (f|X).x0 + r - r by A12,REAL_1:54;
then (f|X).x0 - r < (f|X).x0 by XCMPLX_1:26;
then (f|X).x0 - r < (f|X).x0 + r/2 by A10,AXIOMS:22;
then (f|X).x0 + r/2 in {s: (f|X).x0 - r < s & s < (f|X).x0 + r} by A14
;
then M2 in ].(f|X).x0 - r,(f|X).x0 + r.[ by RCOMP_1:def 2;
then A15: [.M1,M2.] c= ].(f|X).x0 - r,(f|X).x0 + r.[ by A13,RCOMP_1:17;
consider r1 such that
A16: r1 in dom (f|X) & r1 in X & M1 = (f|X).r1 by A1,A5,PARTFUN2:78;
consider r2 such that
A17: r2 in dom (f|X) & r2 in X & M2 = (f|X).r2 by A1,A5,PARTFUN2:78;
set R = min(x0 - r1,r2 - x0);
A18: (f|X).x0 < (f|X).x0 + r/2 by A8,REAL_1:69;
then A19: M1 < (f|X).x0 by REAL_1:84;
A20: r1 <> x0 by A16,A18,REAL_1:84;
now assume
A21: x0 < r1;
A22: x0 in X /\ dom (f|X) by A3,A4,XBOOLE_0:def 3;
r1 in X /\ dom(f|X) by A16,XBOOLE_0:def 3;
hence contradiction by A2,A6,A16,A19,A21,A22,RFUNCT_2:def 4;
end;
then r1 < x0 by A20,REAL_1:def 5;
then A23: x0 - r1 > 0 by SQUARE_1:11;
A24: M2 > (f|X).x0 by A8,REAL_1:69;
A25: x0 <> r2 by A8,A17,REAL_1:69;
now assume
A26: r2 < x0;
A27: x0 in X /\ dom(f|X) by A3,A4,XBOOLE_0:def 3;
r2 in X /\ dom (f|X) by A17,XBOOLE_0:def 3;
hence contradiction by A2,A6,A17,A24,A26,A27,RFUNCT_2:def 4;
end;
then x0 < r2 by A25,REAL_1:def 5;
then r2 - x0 > 0 by SQUARE_1:11;
then R > 0 by A23,SQUARE_1:38;
then reconsider N = ].x0 - R,x0 + R.[ as Neighbourhood of x0 by RCOMP_1
:def 7;
take N;
let x be real number; assume
A28: x in dom (f|X) & x in N;
then x in {s: x0 - R < s & s < x0 + R} by RCOMP_1:def 2;
then A29: ex s st s = x & x0 - R < s & s < x0 + R;
then x0 < R + x by REAL_1:84
; then x0 - x < R + x - x by REAL_1:54
;
then A30: x0 - x < R by XCMPLX_1:26; R <= x0 - r1 by SQUARE_1:35;
then x0 - x < x0 - r1 by A30,AXIOMS:22;
then -(x0 - x) > -(x0 - r1) by REAL_1:50;
then x - x0 > -(x0 - r1) by XCMPLX_1:143;
then x - x0 > r1 - x0 by XCMPLX_1:143;
then x - x0 + x0 > r1 - x0 + x0 by REAL_1:53;
then x > r1 - x0 + x0 by XCMPLX_1:27;
then A31: x > r1 by XCMPLX_1:27;
A32: x - x0 < R by A29,REAL_1:84; R <= r2 - x0 by SQUARE_1:35;
then x - x0 < r2 - x0 by A32,AXIOMS:22;
then x - x0 + x0 < r2 - x0 + x0 by REAL_1:53;
then x < r2 - x0 + x0 by XCMPLX_1:27;
then A33: x < r2 by XCMPLX_1:27;
A34: x is Real by XREAL_0:def 1;
dom (f|X) c= X by RELAT_1:87;
then A35: x in X /\ dom (f|X) by A28,XBOOLE_1:28;
r2 in X /\ dom (f|X) by A17,XBOOLE_0:def 3;
then A36: (f|X).x <= (f|X).r2 by A2,A33,A34,A35,RFUNCT_2:def 4;
r1 in X /\ dom (f|X) by A16,XBOOLE_0:def 3;
then (f|X).r1 <= (f|X).x by A2,A31,A34,A35,RFUNCT_2:def 4;
then (f|X).x in {s: M1<=s & s<=M2} by A16,A17,A36;
then (f|X).x in [.M1,M2.] by RCOMP_1:def 1;
hence (f|X).x in N1 by A7,A15;
end;
hence thesis by A4,FCONT_1:4;
end;
hence f is_continuous_on X by A1,FCONT_1:def 2;
suppose f is_non_increasing_on X;
then A37: f|X is_non_increasing_on X by RFUNCT_2:53;
for x0 be real number st x0 in X holds f|X is_continuous_in x0
proof let x0 be real number; assume
A38: x0 in X;
then x0 in dom f /\ X by A1,XBOOLE_0:def 3;
then A39: x0 in dom (f|X) by RELAT_1:90;
A40: (f|X).:X = f.:X by RFUNCT_2:5;
A41: x0 is Real by XREAL_0:def 1;
now let N1 be Neighbourhood of (f|X).x0;
consider r be real number such that
A42: r > 0 & N1 = ].(f|X).x0 - r,(f|X).x0 + r.[ by RCOMP_1:def 7;
reconsider r as Real by XREAL_0:def 1;
set M1 = (f|X).x0 - r/2;
set M2 = (f|X).x0 + r/2;
A43: r/2 > 0 by A42,SEQ_2:3;
then (f|X).x0 - r < (f|X).x0 - r + r/2 by REAL_1:69;
then (f|X).x0 - r < (f|X).x0 - (r/2 + r/2) + r/2 by XCMPLX_1:66;
then (f|X).x0 - r < (f|X).x0 - (r/2 + r/2 - r/2) by XCMPLX_1:37;
then A44: (f|X).x0 - r < (f|X).x0 - r/2 by XCMPLX_1:26;
A45: (f|X).x0 < (f|X).x0 + r/2 by A43,REAL_1:69;
then A46: (f|X).x0 - r/2 < (f|X).x0 by REAL_1:84;
A47: (f|X).x0 < (f|X).x0 + r by A42,REAL_1:69;
then (f|X).x0 - r/2 < (f|X).x0 + r by A46,AXIOMS:22;
then (f|X).x0 - r/2 in {s: (f|X).x0 - r < s & s < (f|X).x0 + r} by A44
;
then A48: M1 in ].(f|X).x0 - r,(f|X).x0 + r.[ by RCOMP_1:def 2;
(f|X).x0 + r/2 < (f|X).x0 + r/2 + r/2 by A43,REAL_1:69;
then (f|X).x0 + r/2 < (f|X).x0 + (r/2 + r/2) by XCMPLX_1:1;
then A49: (f|X).x0 + r/2 < (f|X).x0 + r by XCMPLX_1:66;
(f|X).x0 - r < (f|X).x0 + r - r by A47,REAL_1:54;
then (f|X).x0 - r < (f|X).x0 by XCMPLX_1:26;
then (f|X).x0 - r < (f|X).x0 + r/2 by A45,AXIOMS:22;
then (f|X).x0 + r/2 in {s: (f|X).x0 - r < s & s < (f|X).x0 + r} by A49
;
then M2 in ].(f|X).x0 - r,(f|X).x0 + r.[ by RCOMP_1:def 2;
then A50: [.M1,M2.] c= ].(f|X).x0 - r,(f|X).x0 + r.[ by A48,RCOMP_1:17;
consider r1 such that
A51: r1 in dom (f|X) & r1 in X & M1 = (f|X).r1 by A1,A40,PARTFUN2:78;
consider r2 such that
A52: r2 in dom (f|X) & r2 in X & M2 = (f|X).r2 by A1,A40,PARTFUN2:78;
set R = min(r1 - x0,x0 - r2);
A53: (f|X).x0 < (f|X).x0 + r/2 by A43,REAL_1:69;
then A54: M1 < (f|X).x0 by REAL_1:84;
A55: r1 <> x0 by A51,A53,REAL_1:84;
now assume
A56: x0 > r1;
A57: x0 in X /\ dom (f|X) by A38,A39,XBOOLE_0:def 3;
r1 in X /\ dom(f|X) by A51,XBOOLE_0:def 3;
hence contradiction by A37,A41,A51,A54,A56,A57,RFUNCT_2:def 5;
end;
then r1 > x0 by A55,REAL_1:def 5;
then A58: r1 - x0 > 0 by SQUARE_1:11;
A59: M2 > (f|X).x0 by A43,REAL_1:69;
A60: x0 <> r2 by A43,A52,REAL_1:69;
now assume
A61: r2 > x0;
A62: x0 in X /\ dom (f|X) by A38,A39,XBOOLE_0:def 3;
r2 in X /\ dom (f|X) by A52,XBOOLE_0:def 3;
hence contradiction by A37,A41,A52,A59,A61,A62,RFUNCT_2:def 5;
end;
then x0 > r2 by A60,REAL_1:def 5;
then x0 - r2 > 0 by SQUARE_1:11;
then R > 0 by A58,SQUARE_1:38;
then reconsider N = ].x0 - R,x0 + R.[ as Neighbourhood of x0 by RCOMP_1
:def 7;
take N;
let x be real number; assume
A63: x in dom (f|X) & x in N;
then x in {s: x0 - R < s & s < x0 + R} by RCOMP_1:def 2;
then A64: ex s st s = x & x0 - R < s & s < x0 + R;
then x0 < R + x by REAL_1:84;
then x0 - x < R + x - x by REAL_1:54
;
then A65: x0 - x < R by XCMPLX_1:26; R <= x0 - r2 by SQUARE_1:35;
then x0 - x < x0 - r2 by A65,AXIOMS:22;
then -(x0 - x) > -(x0 - r2) by REAL_1:50;
then x - x0 > - (x0 - r2) by XCMPLX_1:143;
then x - x0 > r2 - x0 by XCMPLX_1:143;
then x - x0 + x0 > r2 - x0 + x0 by REAL_1:53;
then x > r2 - x0 + x0 by XCMPLX_1:27;
then A66: x > r2 by XCMPLX_1:27;
A67: x - x0 < R by A64,REAL_1:84; R <= r1 - x0 by SQUARE_1:35;
then x - x0 < r1-x0 by A67,AXIOMS:22;
then x - x0 + x0 < r1 - x0 + x0 by REAL_1:53;
then x < r1 - x0 + x0 by XCMPLX_1:27;
then A68: x < r1 by XCMPLX_1:27;
A69: x is Real by XREAL_0:def 1;
dom (f|X) c= X by RELAT_1:87;
then A70: x in X /\ dom(f|X) by A63,XBOOLE_1:28;
r2 in X /\ dom(f|X) by A52,XBOOLE_0:def 3;
then A71: (f|X).x <= (f|X).r2 by A37,A66,A69,A70,RFUNCT_2:def 5;
r1 in X /\ dom(f|X) by A51,XBOOLE_0:def 3;
then (f|X).r1 <= (f|X).x by A37,A68,A69,A70,RFUNCT_2:def 5;
then (f|X).x in {s: M1 <= s & s <= M2} by A51,A52,A71;
then (f|X).x in [.M1,M2.] by RCOMP_1:def 1;
hence (f|X).x in N1 by A42,A50;
end;
hence thesis by A39,FCONT_1:4;
end;
hence f is_continuous_on X by A1,FCONT_1:def 2;
end;
hence thesis;
end;
theorem for f be one-to-one PartFunc of REAL,REAL st
(f is_increasing_on ].p,g.[ or f is_decreasing_on ].p,g.[) &
].p,g.[ c= dom f holds (f|].p,g.[)" is_continuous_on f.:].p,g.[
proof let f be one-to-one PartFunc of REAL,REAL;
assume that
A1: f is_increasing_on ].p,g.[ or f is_decreasing_on ].p,g.[ and
A2: ].p,g.[ c= dom f;
now per cases by A1;
suppose f is_increasing_on ].p,g.[;
then (f|].p,g.[)" is_increasing_on f.:].p,g.[ by Th17;
then (f|].p,g.[)" is_non_decreasing_on f.:].p,g.[ by RFUNCT_2:55;
then A3: (f|].p,g.[)" is_monotone_on f.:].p,g.[ by RFUNCT_2:def 6;
now let r; assume r in f.:].p,g.[;
then consider s such that
A4: s in dom f & s in ].p,g.[ & r = f.s by PARTFUN2:78;
s in dom f /\ ].p,g.[ & r = f.s by A4,XBOOLE_0:def 3;
then s in dom (f|].p,g.[) & r = f.s by RELAT_1:90;
then s in dom (f|].p,g.[) & r = (f|].p,g.[).s by FUNCT_1:68;
then r in rng (f|].p,g.[) by FUNCT_1:def 5;
hence r in dom ((f|].p,g.[)") by FUNCT_1:55;
end;
then A5: f.:].p,g.[ c= dom ((f|].p,g.[)") by SUBSET_1:7;
((f|].p,g.[)").:(f.:].p,g.[) = ((f|].p,g.[)").:(rng (f|].p,g.[))
by RELAT_1:148
.= ((f|].p,g.[)").:(dom ((f|].p,g.[)")) by FUNCT_1:55
.= rng ((f|].p,g.[)") by RELAT_1:146
.= dom (f|].p,g.[) by FUNCT_1:55
.= dom f /\ ].p,g.[ by RELAT_1:90
.= ].p,g.[ by A2,XBOOLE_1:28;
hence thesis by A3,A5,Th23;
suppose f is_decreasing_on ].p,g.[;
then (f|].p,g.[)" is_decreasing_on f.:].p,g.[ by Th18;
then (f|].p,g.[)" is_non_increasing_on f.:].p,g.[ by RFUNCT_2:56;
then A6: (f|].p,g.[)" is_monotone_on f.:].p,g.[ by RFUNCT_2:def 6;
now let r; assume r in f.:].p,g.[;
then consider s such that
A7: s in dom f & s in ].p,g.[ & r = f.s by PARTFUN2:78;
s in dom f /\ ].p,g.[ by A7,XBOOLE_0:def 3;
then s in dom (f|].p,g.[) by RELAT_1:90;
then s in dom (f|].p,g.[) & r = (f|].p,g.[).s by A7,FUNCT_1:68;
then r in rng (f|].p,g.[) by FUNCT_1:def 5;
hence r in dom ((f|].p,g.[)") by FUNCT_1:55;
end;
then A8: f.:].p,g.[ c= dom ((f|].p,g.[)") by SUBSET_1:7;
((f|].p,g.[)").:(f.:].p,g.[) = ((f|].p,g.[)").:(rng (f|].p,g.[))
by RELAT_1:148
.= ((f|].p,g.[)").:(dom ((f|].p,g.[)")) by FUNCT_1:55
.= rng ((f|].p,g.[)") by RELAT_1:146
.= dom (f|].p,g.[) by FUNCT_1:55
.= dom f /\ ].p,g.[ by RELAT_1:90
.= ].p,g.[ by A2,XBOOLE_1:28;
hence thesis by A6,A8,Th23;
end;
hence thesis;
end;
theorem
for f be one-to-one PartFunc of REAL,REAL st
(f is_increasing_on left_open_halfline(p) or
f is_decreasing_on left_open_halfline(p)) &
left_open_halfline(p) c= dom f holds
(f|left_open_halfline(p))" is_continuous_on f.:left_open_halfline(p)
proof let f be one-to-one PartFunc of REAL,REAL;
set L = left_open_halfline(p);assume that
A1: f is_increasing_on L or f is_decreasing_on L and
A2: L c= dom f;
now per cases by A1;
suppose f is_increasing_on L;
then (f|L)" is_increasing_on f.:L by Th17;
then (f|L)" is_non_decreasing_on f.:L by RFUNCT_2:55;
then A3: (f|L)" is_monotone_on f.:L by RFUNCT_2:def 6;
now let r; assume r in f.:L;
then consider s such that
A4: s in dom f & s in L & r = f.s by PARTFUN2:78;
s in dom f /\ L & r = f.s by A4,XBOOLE_0:def 3;
then s in dom (f|L) & r = f.s by RELAT_1:90;
then s in dom (f|L) & r = (f|L).s by FUNCT_1:68;
then r in rng (f|L) by FUNCT_1:def 5;
hence r in dom ((f|L)") by FUNCT_1:55;
end;
then A5: f.:L c= dom ((f|L)") by SUBSET_1:7;
((f|L)").:(f.:L) = ((f|L)").:(rng (f|L))
by RELAT_1:148
.= ((f|L)").:(dom ((f|L)")) by FUNCT_1:55
.= rng ((f|L)") by RELAT_1:146
.= dom (f|L) by FUNCT_1:55
.= dom f /\ L by RELAT_1:90
.= L by A2,XBOOLE_1:28;
hence thesis by A3,A5,Th19;
suppose f is_decreasing_on L;
then (f|L)" is_decreasing_on f.:L by Th18;
then (f|L)" is_non_increasing_on f.:L by RFUNCT_2:56;
then A6: (f|L)" is_monotone_on f.:L by RFUNCT_2:def 6;
now let r; assume r in f.:L;
then consider s such that
A7: s in dom f & s in L & r = f.s by PARTFUN2:78;
s in dom f /\ L by A7,XBOOLE_0:def 3;
then s in dom (f|L) by RELAT_1:90;
then s in dom (f|L) & r = (f|L).s by A7,FUNCT_1:68;
then r in rng (f|L) by FUNCT_1:def 5;
hence r in dom ((f|L)") by FUNCT_1:55;
end;
then A8: f.:L c= dom ((f|L)") by SUBSET_1:7;
((f|L)").:(f.:L) = ((f|L)").:(rng (f|L))
by RELAT_1:148
.= ((f|L)").:(dom ((f|L)")) by FUNCT_1:55
.= rng ((f|L)") by RELAT_1:146
.= dom (f|L) by FUNCT_1:55
.= dom f /\ L by RELAT_1:90
.= L by A2,XBOOLE_1:28;
hence thesis by A6,A8,Th19;
end;
hence thesis;
end;
theorem
for f be one-to-one PartFunc of REAL,REAL st
(f is_increasing_on right_open_halfline(p) or
f is_decreasing_on right_open_halfline(p)) &
right_open_halfline(p) c= dom f holds
(f|right_open_halfline(p))" is_continuous_on f.:right_open_halfline(p)
proof let f be one-to-one PartFunc of REAL,REAL;
set L = right_open_halfline(p); assume that
A1: f is_increasing_on L or f is_decreasing_on L and
A2: L c= dom f;
now per cases by A1;
suppose f is_increasing_on L;
then (f|L)" is_increasing_on f.:L by Th17;
then (f|L)" is_non_decreasing_on f.:L by RFUNCT_2:55;
then A3: (f|L)" is_monotone_on f.:L by RFUNCT_2:def 6;
now let r; assume r in f.:L;
then consider s such that
A4: s in dom f & s in L & r = f.s by PARTFUN2:78;
s in dom f /\ L & r = f.s by A4,XBOOLE_0:def 3;
then s in dom (f|L) & r = f.s by RELAT_1:90;
then s in dom (f|L) & r = (f|L).s by FUNCT_1:68;
then r in rng (f|L) by FUNCT_1:def 5;
hence r in dom ((f|L)") by FUNCT_1:55;
end;
then A5: f.:L c= dom ((f|L)") by SUBSET_1:7;
((f|L)").:(f.:L) = ((f|L)").:(rng (f|L))
by RELAT_1:148
.= ((f|L)").:(dom ((f|L)")) by FUNCT_1:55
.= rng ((f|L)") by RELAT_1:146
.= dom (f|L) by FUNCT_1:55
.= dom f /\ L by RELAT_1:90
.= L by A2,XBOOLE_1:28;
hence thesis by A3,A5,Th20;
suppose f is_decreasing_on L;
then (f|L)" is_decreasing_on f.:L by Th18;
then (f|L)" is_non_increasing_on f.:L by RFUNCT_2:56;
then A6: (f|L)" is_monotone_on f.:L by RFUNCT_2:def 6;
now let r; assume r in f.:L;
then consider s such that
A7: s in dom f & s in L & r = f.s by PARTFUN2:78;
s in dom f /\ L by A7,XBOOLE_0:def 3;
then s in dom (f|L) by RELAT_1:90;
then s in dom (f|L) & r = (f|L).s by A7,FUNCT_1:68;
then r in rng (f|L) by FUNCT_1:def 5;
hence r in dom ((f|L)") by FUNCT_1:55;
end;
then A8: f.:L c= dom ((f|L)") by SUBSET_1:7;
((f|L)").:(f.:L) = ((f|L)").:(rng (f|L))
by RELAT_1:148
.= ((f|L)").:(dom ((f|L)")) by FUNCT_1:55
.= rng ((f|L)") by RELAT_1:146
.= dom (f|L) by FUNCT_1:55
.= dom f /\ L by RELAT_1:90
.= L by A2,XBOOLE_1:28;
hence thesis by A6,A8,Th20;
end;
hence thesis;
end;
theorem
for f be one-to-one PartFunc of REAL,REAL st
(f is_increasing_on left_closed_halfline(p) or
f is_decreasing_on left_closed_halfline(p)) &
left_closed_halfline(p) c= dom f holds
(f|left_closed_halfline(p))" is_continuous_on f.:left_closed_halfline(p)
proof let f be one-to-one PartFunc of REAL,REAL;
set L = left_closed_halfline(p);assume that
A1: f is_increasing_on L or f is_decreasing_on L and
A2: L c= dom f;
now per cases by A1;
suppose f is_increasing_on L;
then (f|L)" is_increasing_on f.:L by Th17;
then (f|L)" is_non_decreasing_on f.:L by RFUNCT_2:55;
then A3: (f|L)" is_monotone_on f.:L by RFUNCT_2:def 6;
now let r; assume r in f.:L;
then consider s such that
A4: s in dom f & s in L & r = f.s by PARTFUN2:78;
s in dom f /\ L & r = f.s by A4,XBOOLE_0:def 3;
then s in dom (f|L) & r = f.s by RELAT_1:90;
then s in dom (f|L) & r = (f|L).s by FUNCT_1:68;
then r in rng (f|L) by FUNCT_1:def 5;
hence r in dom ((f|L)") by FUNCT_1:55;
end;
then A5: f.:L c= dom ((f|L)") by SUBSET_1:7;
((f|L)").:(f.:L) = ((f|L)").:(rng (f|L))
by RELAT_1:148
.= ((f|L)").:(dom ((f|L)")) by FUNCT_1:55
.= rng ((f|L)") by RELAT_1:146
.= dom (f|L) by FUNCT_1:55
.= dom f /\ L by RELAT_1:90
.= L by A2,XBOOLE_1:28;
hence thesis by A3,A5,Th21;
suppose f is_decreasing_on L;
then (f|L)" is_decreasing_on f.:L by Th18;
then (f|L)" is_non_increasing_on f.:L by RFUNCT_2:56;
then A6: (f|L)" is_monotone_on f.:L by RFUNCT_2:def 6;
now let r; assume r in f.:L;
then consider s such that
A7: s in dom f & s in L & r = f.s by PARTFUN2:78;
s in dom f /\ L by A7,XBOOLE_0:def 3;
then s in dom (f|L) by RELAT_1:90;
then s in dom (f|L) & r = (f|L).s by A7,FUNCT_1:68;
then r in rng (f|L) by FUNCT_1:def 5;
hence r in dom ((f|L)") by FUNCT_1:55;
end;
then A8: f.:L c= dom ((f|L)") by SUBSET_1:7;
((f|L)").:(f.:L) = ((f|L)").:(rng (f|L))
by RELAT_1:148
.= ((f|L)").:(dom ((f|L)")) by FUNCT_1:55
.= rng ((f|L)") by RELAT_1:146
.= dom (f|L) by FUNCT_1:55
.= dom f /\ L by RELAT_1:90
.= L by A2,XBOOLE_1:28;
hence thesis by A6,A8,Th21;
end;
hence thesis;
end;
theorem
for f be one-to-one PartFunc of REAL,REAL st
(f is_increasing_on right_closed_halfline(p) or
f is_decreasing_on right_closed_halfline(p)) &
right_closed_halfline(p) c= dom f holds
(f|right_closed_halfline(p))" is_continuous_on f.:right_closed_halfline(p)
proof let f be one-to-one PartFunc of REAL,REAL;
set L = right_closed_halfline(p); assume that
A1: f is_increasing_on L or f is_decreasing_on L and
A2: L c= dom f;
now per cases by A1;
suppose f is_increasing_on L;
then (f|L)" is_increasing_on f.:L by Th17;
then (f|L)" is_non_decreasing_on f.:L by RFUNCT_2:55;
then A3: (f|L)" is_monotone_on f.:L by RFUNCT_2:def 6;
now let r; assume r in f.:L;
then consider s such that
A4: s in dom f & s in L & r = f.s by PARTFUN2:78;
s in dom f /\ L & r = f.s by A4,XBOOLE_0:def 3;
then s in dom (f|L) & r = f.s by RELAT_1:90;
then s in dom (f|L) & r = (f|L).s by FUNCT_1:68;
then r in rng (f|L) by FUNCT_1:def 5;
hence r in dom ((f|L)") by FUNCT_1:55;
end;
then A5: f.:L c= dom ((f|L)") by SUBSET_1:7;
((f|L)").:(f.:L) = ((f|L)").:(rng (f|L))
by RELAT_1:148
.= ((f|L)").:(dom ((f|L)")) by FUNCT_1:55
.= rng ((f|L)") by RELAT_1:146
.= dom (f|L) by FUNCT_1:55
.= dom f /\ L by RELAT_1:90
.= L by A2,XBOOLE_1:28;
hence thesis by A3,A5,Th22;
suppose f is_decreasing_on L;
then (f|L)" is_decreasing_on f.:L by Th18;
then (f|L)" is_non_increasing_on f.:L by RFUNCT_2:56;
then A6: (f|L)" is_monotone_on f.:L by RFUNCT_2:def 6;
now let r; assume r in f.:L;
then consider s such that
A7: s in dom f & s in L & r = f.s by PARTFUN2:78;
s in dom f /\ L by A7,XBOOLE_0:def 3;
then s in dom (f|L) by RELAT_1:90;
then s in dom (f|L) & r = (f|L).s by A7,FUNCT_1:68;
then r in rng (f|L) by FUNCT_1:def 5;
hence r in dom ((f|L)") by FUNCT_1:55;
end;
then A8: f.:L c= dom ((f|L)") by SUBSET_1:7;
((f|L)").:(f.:L) = ((f|L)").:(rng (f|L))
by RELAT_1:148
.= ((f|L)").:(dom ((f|L)")) by FUNCT_1:55
.= rng ((f|L)") by RELAT_1:146
.= dom (f|L) by FUNCT_1:55
.= dom f /\ L by RELAT_1:90
.= L by A2,XBOOLE_1:28;
hence thesis by A6,A8,Th22;
end;
hence thesis;
end;
theorem
for f be one-to-one PartFunc of REAL,REAL st
(f is_increasing_on [#](REAL) or f is_decreasing_on [#]
(REAL)) & f is total holds
f" is_continuous_on rng f
proof let f be one-to-one PartFunc of REAL,REAL;
set L = [#] REAL; assume that
A1: f is_increasing_on [#](REAL) or f is_decreasing_on [#](REAL) and
A2: f is total;
A3: dom f = REAL by A2,PARTFUN1:def 4
.= [#] REAL by SUBSET_1:def 4;
now per cases by A1;
suppose f is_increasing_on L;
then (f|L)" is_increasing_on f.:L by Th17;
then (f|L)" is_non_decreasing_on f.:L by RFUNCT_2:55;
then A4: (f|L)" is_monotone_on f.:L by RFUNCT_2:def 6;
now let r; assume r in f.:L;
then consider s such that
A5: s in dom f & s in L & r = f.s by PARTFUN2:78;
s in dom f /\ L & r = f.s by A5,XBOOLE_0:def 3;
then s in dom (f|L) & r = f.s by RELAT_1:90;
then s in dom (f|L) & r = (f|L).s by FUNCT_1:68;
then r in rng (f|L) by FUNCT_1:def 5;
hence r in dom ((f|L)") by FUNCT_1:55;
end;
then A6: f.:L c= dom ((f|L)") by SUBSET_1:7;
((f|L)").:(f.:L) = ((f|L)").:(rng (f|L))
by RELAT_1:148
.= ((f|L)").:(dom ((f|L)")) by FUNCT_1:55
.= rng ((f|L)") by RELAT_1:146
.= dom (f|L) by FUNCT_1:55
.= dom f /\ L by RELAT_1:90
.= REAL by A3,SUBSET_1:def 4;
then (f|L)" is_continuous_on f.:L by A4,A6,Th24;
then (f|L)" is_continuous_on rng f by A3,RELAT_1:146;
hence thesis by A3,RELAT_1:97;
suppose f is_decreasing_on L;
then (f|L)" is_decreasing_on f.:L by Th18;
then (f|L)" is_non_increasing_on f.:L by RFUNCT_2:56;
then A7: (f|L)" is_monotone_on f.:L by RFUNCT_2:def 6;
now let r; assume r in f.:L;
then consider s such that
A8: s in dom f & s in L & r = f.s by PARTFUN2:78;
s in dom f /\ L by A8,XBOOLE_0:def 3;
then s in dom (f|L) by RELAT_1:90;
then s in dom (f|L) & r = (f|L).s by A8,FUNCT_1:68;
then r in rng (f|L) by FUNCT_1:def 5;
hence r in dom ((f|L)") by FUNCT_1:55;
end;
then A9: f.:L c= dom ((f|L)") by SUBSET_1:7;
((f|L)").:(f.:L) = ((f|L)").:(rng (f|L))
by RELAT_1:148
.= ((f|L)").:(dom ((f|L)")) by FUNCT_1:55
.= rng ((f|L)") by RELAT_1:146
.= dom (f|L) by FUNCT_1:55
.= dom f /\ L by RELAT_1:90
.= REAL by A3,SUBSET_1:def 4;
then (f|L)" is_continuous_on f.:L by A7,A9,Th24;
then (f|L)" is_continuous_on rng f by A3,RELAT_1:146;
hence thesis by A3,RELAT_1:97;
end;
hence thesis;
end;
theorem
f is_continuous_on ].p,g.[ &
(f is_increasing_on ].p,g.[ or f is_decreasing_on ].p,g.[) implies
rng (f|].p,g.[) is open
proof assume that
A1: f is_continuous_on ].p,g.[ and
A2: f is_increasing_on ].p,g.[ or f is_decreasing_on ].p,g.[;
now set f1 = f|].p,g.[;
let r1 be real number; assume r1 in rng f1;
then consider x0 such that
A3: x0 in dom f1 & f1.x0 = r1 by PARTFUN1:26;
A4: x0 in dom f /\ ].p,g.[ by A3,FUNCT_1:68;
then x0 in dom f & x0 in ].p,g.[ by XBOOLE_0:def 3;
then consider N be Neighbourhood of x0 such that
A5: N c= ].p,g.[ by RCOMP_1:39;
consider r be real number such that
A6: 0 < r & N = ].x0 - r, x0 + r.[ by RCOMP_1:def 7;
reconsider r as Real by XREAL_0:def 1;
A7: f is_continuous_on N by A1,A5,FCONT_1:17;
A8: r/2 < r by A6,SEQ_2:4;
then A9: x0 - r < x0 - r/2 by REAL_1:92;
A10: 0 < r/2 by A6,SEQ_2:3;
then A11: x0 - r/2 < x0 - 0 by REAL_1:92;
x0 < x0 + r by A6,REAL_2:174;
then x0 - r/2 < x0 + r by A11,AXIOMS:22;
then x0 - r/2 in {g1: x0 - r < g1 & g1 < x0 + r} by A9;
then A12: x0 - r/2 in ].x0 - r, x0 + r.[ by RCOMP_1:def 2;
A13: x0 + r/2 < x0 + r by A8,REAL_1:67;
A14: x0 - r < x0 by A6,REAL_2:174;
A15: x0 < x0 + r/2 by A10,REAL_2:174;
then x0 - r < x0 + r/2 by A14,AXIOMS:22;
then x0 + r/2 in {g2: x0 - r < g2 & g2 < x0 + r} by A13;
then A16: x0 + r/2 in ].x0 - r, x0 + r.[ by RCOMP_1:def 2;
then A17: [.x0 - r/2, x0 + r/2.] c= ].x0 - r, x0 + r.[ by A12,RCOMP_1:17;
then A18: f is_continuous_on [.x0 - r/2, x0 + r/2.] by A6,A7,FCONT_1:17;
set fm = f.(x0 - r/2);
set fp = f.(x0 + r/2);
A19: x0 - r/2 < x0 + r/2 by A11,A15,AXIOMS:22;
A20: N c= dom f by A7,FCONT_1:def 2;
then A21: x0 + r/2 in ].p,g.[ /\ dom f by A5,A6,A16,XBOOLE_0:def 3;
A22: x0 - r/2 in ].p,g.[ /\ dom f by A5,A6,A12,A20,XBOOLE_0:def 3;
A23: r1 = f.x0 by A3,FUNCT_1:68;
now per cases by A2;
suppose A24: f is_increasing_on ].p,g.[;
then fm < fp by A19,A21,A22,RFUNCT_2:def 2;
then [.fp,fm.] = {} by RCOMP_1:13;
then A25: [.fm,fp.] \/ [.fp,fm.] = [.fm,fp.];
fm < f.x0 by A4,A11,A22,A24,RFUNCT_2:def 2;
then A26: 0 < f.x0 - fm by SQUARE_1:11;
set R = min(f.x0 - fm,fp - f.x0);
f.x0 < fp by A4,A15,A21,A24,RFUNCT_2:def 2;
then 0 < fp - f.x0 by SQUARE_1:11;
then 0 < R by A26,SQUARE_1:38;
then reconsider N1 = ].r1 - R, r1 + R.[ as Neighbourhood of r1 by RCOMP_1
:def 7;
take N1;
thus N1 c= rng f1
proof let x; assume x in N1;
then x in {r2: r1 - R < r2 & r2 < r1 + R} by RCOMP_1:def 2;
then consider r2 such that
A27: r2 = x & f.x0 - R < r2 & r2 < f.x0 + R by A23;
A28: R <= f.x0 - fm & R <= fp - f.x0 by SQUARE_1:35;
then f.x0 - (f.x0 - fm) <= f.x0 - R by REAL_1:92;
then fm <= f.x0 - R by XCMPLX_1:18;
then A29: fm < r2 by A27,AXIOMS:22;
f.x0 + R <= f.x0 + (fp - f.x0) by A28,REAL_1:55;
then f.x0 + R <= fp by XCMPLX_1:27;
then r2 < fp by A27,AXIOMS:22;
then r2 in {g2: fm < g2 & g2 < fp} by A29;
then A30: r2 in ].fm,fp.[ by RCOMP_1:def 2;
].fm,fp.[ c= [.fm,fp.] by RCOMP_1:15;
then consider s such that
A31: s in [.x0 - r/2, x0 + r/2.] & x = f.s by A18,A19,A25,A27,A30,
FCONT_2:16;
s in N by A6,A17,A31; then s in dom f /\
].p,g.[ by A5,A20,XBOOLE_0:def 3
;
then A32: s in dom f1 by FUNCT_1:68;
then x = f1.s by A31,FUNCT_1:68;
hence thesis by A32,FUNCT_1:def 5;
end;
suppose A33: f is_decreasing_on ].p,g.[;
then fp < fm by A19,A21,A22,RFUNCT_2:def 3;
then [.fm,fp.] = {} by RCOMP_1:13;
then A34: [.fm,fp.] \/ [.fp,fm.] = [.fp,fm.];
f.x0 < fm by A4,A11,A22,A33,RFUNCT_2:def 3;
then A35: 0 < fm - f.x0 by SQUARE_1:11;
set R = min(fm - f.x0,f.x0 - fp);
fp < f.x0 by A4,A15,A21,A33,RFUNCT_2:def 3;
then 0 < f.x0 - fp by SQUARE_1:11;
then 0 < R by A35,SQUARE_1:38;
then reconsider N1 = ].r1 - R, r1 + R.[ as Neighbourhood of r1 by RCOMP_1
:def 7;
take N1;
thus N1 c= rng f1
proof let x; assume x in N1;
then x in {r2: r1 - R < r2 & r2 < r1 + R} by RCOMP_1:def 2;
then consider r2 such that
A36: r2 = x & f.x0 - R < r2 & r2 < f.x0 + R by A23;
A37: R <= fm - f.x0 & R <= f.x0 - fp by SQUARE_1:35;
then f.x0 - (f.x0 - fp) <= f.x0 - R by REAL_1:92;
then fp <= f.x0 - R by XCMPLX_1:18;
then A38: fp < r2 by A36,AXIOMS:22;
f.x0 + R <= f.x0 + (fm - f.x0) by A37,REAL_1:55;
then f.x0 + R <= fm by XCMPLX_1:27;
then r2 < fm by A36,AXIOMS:22;
then r2 in {g2: fp < g2 & g2 < fm} by A38;
then A39: r2 in ].fp,fm.[ by RCOMP_1:def 2;
].fp,fm.[ c= [.fp,fm.] by RCOMP_1:15;
then consider s such that
A40: s in [.x0 - r/2, x0 + r/2.] & x = f.s by A18,A19,A34,A36,A39,
FCONT_2:16;
s in N by A6,A17,A40; then s in dom f /\
].p,g.[ by A5,A20,XBOOLE_0:def 3
;
then A41: s in dom f1 by FUNCT_1:68;
then x = f1.s by A40,FUNCT_1:68;
hence thesis by A41,FUNCT_1:def 5;
end;
end;
hence ex N be Neighbourhood of r1 st N c= rng f1;
end;
hence thesis by RCOMP_1:41;
end;
theorem
f is_continuous_on left_open_halfline(p) &
(f is_increasing_on left_open_halfline(p) or
f is_decreasing_on left_open_halfline(p)) implies
rng (f|left_open_halfline(p)) is open
proof set L = left_open_halfline(p); assume that
A1: f is_continuous_on L and
A2: f is_increasing_on L or f is_decreasing_on L;
now set f1 = f|L;
let r1 be real number; assume r1 in rng f1;
then consider x0 such that
A3: x0 in dom f1 & f1.x0 = r1 by PARTFUN1:26;
A4: x0 in dom f /\ L by A3,FUNCT_1:68;
then x0 in dom f & x0 in L by XBOOLE_0:def 3;
then consider N be Neighbourhood of x0 such that
A5: N c= L by RCOMP_1:39;
consider r be real number such that
A6: 0 < r & N = ].x0 - r, x0 + r.[ by RCOMP_1:def 7;
reconsider r as Real by XREAL_0:def 1;
A7: f is_continuous_on N by A1,A5,FCONT_1:17;
A8: r/2 < r by A6,SEQ_2:4;
then A9: x0 - r < x0 - r/2 by REAL_1:92;
A10: 0 < r/2 by A6,SEQ_2:3;
then A11: x0 - r/2 < x0 - 0 by REAL_1:92;
x0 < x0 + r by A6,REAL_2:174;
then x0 - r/2 < x0 + r by A11,AXIOMS:22;
then x0 - r/2 in {g1: x0 - r < g1 & g1 < x0 + r} by A9;
then A12: x0 - r/2 in ].x0 - r, x0 + r.[ by RCOMP_1:def 2;
A13: x0 + r/2 < x0 + r by A8,REAL_1:67;
A14: x0 - r < x0 by A6,REAL_2:174;
A15: x0 < x0 + r/2 by A10,REAL_2:174;
then x0 - r < x0 + r/2 by A14,AXIOMS:22;
then x0 + r/2 in {g2: x0 - r < g2 & g2 < x0 + r} by A13;
then A16: x0 + r/2 in ].x0 - r, x0 + r.[ by RCOMP_1:def 2;
then A17: [.x0 - r/2, x0 + r/2.] c= ].x0 - r, x0 + r.[ by A12,RCOMP_1:17;
then A18: f is_continuous_on [.x0 - r/2, x0 + r/2.] by A6,A7,FCONT_1:17;
set fm = f.(x0 - r/2);
set fp = f.(x0 + r/2);
A19: x0 - r/2 < x0 + r/2 by A11,A15,AXIOMS:22;
A20: N c= dom f by A7,FCONT_1:def 2;
then A21: x0 + r/2 in L /\ dom f by A5,A6,A16,XBOOLE_0:def 3;
A22: x0 - r/2 in L /\ dom f by A5,A6,A12,A20,XBOOLE_0:def 3;
A23: r1 = f.x0 by A3,FUNCT_1:68;
now per cases by A2;
suppose A24: f is_increasing_on L;
then fm < fp by A19,A21,A22,RFUNCT_2:def 2;
then [.fp,fm.] = {} by RCOMP_1:13;
then A25: [.fm,fp.] \/ [.fp,fm.] = [.fm,fp.];
fm < f.x0 by A4,A11,A22,A24,RFUNCT_2:def 2;
then A26: 0 < f.x0 - fm by SQUARE_1:11;
set R = min(f.x0 - fm,fp - f.x0);
f.x0 < fp by A4,A15,A21,A24,RFUNCT_2:def 2;
then 0 < fp - f.x0 by SQUARE_1:11;
then 0 < R by A26,SQUARE_1:38;
then reconsider N1 = ].r1 - R, r1 + R.[ as Neighbourhood of r1 by RCOMP_1
:def 7;
take N1;
thus N1 c= rng f1
proof let x; assume x in N1;
then x in {r2: r1 - R < r2 & r2 < r1 + R} by RCOMP_1:def 2;
then consider r2 such that
A27: r2 = x & f.x0 - R < r2 & r2 < f.x0 + R by A23;
A28: R <= f.x0 - fm & R <= fp - f.x0 by SQUARE_1:35;
then f.x0 - (f.x0 - fm) <= f.x0 - R by REAL_1:92;
then fm <= f.x0 - R by XCMPLX_1:18;
then A29: fm < r2 by A27,AXIOMS:22;
f.x0 + R <= f.x0 + (fp - f.x0) by A28,REAL_1:55;
then f.x0 + R <= fp by XCMPLX_1:27;
then r2 < fp by A27,AXIOMS:22;
then r2 in {g2: fm < g2 & g2 < fp} by A29;
then A30: r2 in ].fm,fp.[ by RCOMP_1:def 2;
].fm,fp.[ c= [.fm,fp.] by RCOMP_1:15;
then consider s such that
A31: s in [.x0 - r/2, x0 + r/2.] & x = f.s by A18,A19,A25,A27,A30,
FCONT_2:16;
s in N by A6,A17,A31; then s in dom f /\
L by A5,A20,XBOOLE_0:def 3;
then A32: s in dom f1 by FUNCT_1:68;
then x = f1.s by A31,FUNCT_1:68;
hence thesis by A32,FUNCT_1:def 5;
end;
suppose A33: f is_decreasing_on L;
then fp < fm by A19,A21,A22,RFUNCT_2:def 3;
then [.fm,fp.] = {} by RCOMP_1:13;
then A34: [.fm,fp.] \/ [.fp,fm.] = [.fp,fm.];
f.x0 < fm by A4,A11,A22,A33,RFUNCT_2:def 3;
then A35: 0 < fm - f.x0 by SQUARE_1:11;
set R = min(fm - f.x0,f.x0 - fp);
fp < f.x0 by A4,A15,A21,A33,RFUNCT_2:def 3;
then 0 < f.x0 - fp by SQUARE_1:11;
then 0 < R by A35,SQUARE_1:38;
then reconsider N1 = ].r1 - R, r1 + R.[ as Neighbourhood of r1 by RCOMP_1
:def 7;
take N1;
thus N1 c= rng f1
proof let x; assume x in N1;
then x in {r2: r1 - R < r2 & r2 < r1 + R} by RCOMP_1:def 2;
then consider r2 such that
A36: r2 = x & f.x0 - R < r2 & r2 < f.x0 + R by A23;
A37: R <= fm - f.x0 & R <= f.x0 - fp by SQUARE_1:35;
then f.x0 - (f.x0 - fp) <= f.x0 - R by REAL_1:92;
then fp <= f.x0 - R by XCMPLX_1:18;
then A38: fp < r2 by A36,AXIOMS:22;
f.x0 + R <= f.x0 + (fm - f.x0) by A37,REAL_1:55;
then f.x0 + R <= fm by XCMPLX_1:27;
then r2 < fm by A36,AXIOMS:22;
then r2 in {g2: fp < g2 & g2 < fm} by A38;
then A39: r2 in ].fp,fm.[ by RCOMP_1:def 2;
].fp,fm.[ c= [.fp,fm.] by RCOMP_1:15;
then consider s such that
A40: s in [.x0 - r/2, x0 + r/2.] & x = f.s by A18,A19,A34,A36,A39,
FCONT_2:16;
s in N by A6,A17,A40; then s in dom f /\
L by A5,A20,XBOOLE_0:def 3;
then A41: s in dom f1 by FUNCT_1:68;
then x = f1.s by A40,FUNCT_1:68;
hence thesis by A41,FUNCT_1:def 5;
end;
end;
hence ex N be Neighbourhood of r1 st N c= rng f1;
end;
hence thesis by RCOMP_1:41;
end;
theorem
f is_continuous_on right_open_halfline(p) &
(f is_increasing_on right_open_halfline(p) or
f is_decreasing_on right_open_halfline(p)) implies
rng (f|right_open_halfline(p)) is open
proof set L = right_open_halfline(p); assume that
A1: f is_continuous_on L and
A2: f is_increasing_on L or f is_decreasing_on L;
now set f1 = f|L;
let r1 be real number; assume r1 in rng f1;
then consider x0 such that
A3: x0 in dom f1 & f1.x0 = r1 by PARTFUN1:26;
A4: x0 in dom f /\ L by A3,FUNCT_1:68;
then x0 in dom f & x0 in L by XBOOLE_0:def 3;
then consider N be Neighbourhood of x0 such that
A5: N c= L by RCOMP_1:39;
consider r be real number such that
A6: 0 < r & N = ].x0 - r, x0 + r.[ by RCOMP_1:def 7;
reconsider r as Real by XREAL_0:def 1;
A7: f is_continuous_on N by A1,A5,FCONT_1:17;
A8: r/2 < r by A6,SEQ_2:4;
then A9: x0 - r < x0 - r/2 by REAL_1:92;
A10: 0 < r/2 by A6,SEQ_2:3;
then A11: x0 - r/2 < x0 - 0 by REAL_1:92;
x0 < x0 + r by A6,REAL_2:174;
then x0 - r/2 < x0 + r by A11,AXIOMS:22;
then x0 - r/2 in {g1: x0 - r < g1 & g1 < x0 + r} by A9;
then A12: x0 - r/2 in ].x0 - r, x0 + r.[ by RCOMP_1:def 2;
A13: x0 + r/2 < x0 + r by A8,REAL_1:67;
A14: x0 - r < x0 by A6,REAL_2:174;
A15: x0 < x0 + r/2 by A10,REAL_2:174;
then x0 - r < x0 + r/2 by A14,AXIOMS:22;
then x0 + r/2 in {g2: x0 - r < g2 & g2 < x0 + r} by A13;
then A16: x0 + r/2 in ].x0 - r, x0 + r.[ by RCOMP_1:def 2;
then A17: [.x0 - r/2, x0 + r/2.] c= ].x0 - r, x0 + r.[ by A12,RCOMP_1:17;
then A18: f is_continuous_on [.x0 - r/2, x0 + r/2.] by A6,A7,FCONT_1:17;
set fm = f.(x0 - r/2);
set fp = f.(x0 + r/2);
A19: x0 - r/2 < x0 + r/2 by A11,A15,AXIOMS:22;
A20: N c= dom f by A7,FCONT_1:def 2;
then A21: x0 + r/2 in L /\ dom f by A5,A6,A16,XBOOLE_0:def 3;
A22: x0 - r/2 in L /\ dom f by A5,A6,A12,A20,XBOOLE_0:def 3;
A23: r1 = f.x0 by A3,FUNCT_1:68;
now per cases by A2;
suppose A24: f is_increasing_on L;
then fm < fp by A19,A21,A22,RFUNCT_2:def 2;
then [.fp,fm.] = {} by RCOMP_1:13;
then A25: [.fm,fp.] \/ [.fp,fm.] = [.fm,fp.];
fm < f.x0 by A4,A11,A22,A24,RFUNCT_2:def 2;
then A26: 0 < f.x0 - fm by SQUARE_1:11;
set R = min(f.x0 - fm,fp - f.x0);
f.x0 < fp by A4,A15,A21,A24,RFUNCT_2:def 2;
then 0 < fp - f.x0 by SQUARE_1:11;
then 0 < R by A26,SQUARE_1:38;
then reconsider N1 = ].r1 - R, r1 + R.[ as Neighbourhood of r1 by RCOMP_1
:def 7;
take N1;
thus N1 c= rng f1
proof let x; assume x in N1;
then x in {r2: r1 - R < r2 & r2 < r1 + R} by RCOMP_1:def 2;
then consider r2 such that
A27: r2 = x & f.x0 - R < r2 & r2 < f.x0 + R by A23;
A28: R <= f.x0 - fm & R <= fp - f.x0 by SQUARE_1:35;
then f.x0 - (f.x0 - fm) <= f.x0 - R by REAL_1:92;
then fm <= f.x0 - R by XCMPLX_1:18;
then A29: fm < r2 by A27,AXIOMS:22;
f.x0 + R <= f.x0 + (fp - f.x0) by A28,REAL_1:55;
then f.x0 + R <= fp by XCMPLX_1:27;
then r2 < fp by A27,AXIOMS:22;
then r2 in {g2: fm < g2 & g2 < fp} by A29;
then A30: r2 in ].fm,fp.[ by RCOMP_1:def 2;
].fm,fp.[ c= [.fm,fp.] by RCOMP_1:15;
then consider s such that
A31: s in [.x0 - r/2, x0 + r/2.] & x = f.s by A18,A19,A25,A27,A30,
FCONT_2:16;
s in N by A6,A17,A31; then s in dom f /\
L by A5,A20,XBOOLE_0:def 3;
then A32: s in dom f1 by FUNCT_1:68;
then x = f1.s by A31,FUNCT_1:68;
hence thesis by A32,FUNCT_1:def 5;
end;
suppose A33: f is_decreasing_on L;
then fp < fm by A19,A21,A22,RFUNCT_2:def 3;
then [.fm,fp.] = {} by RCOMP_1:13;
then A34: [.fm,fp.] \/ [.fp,fm.] = [.fp,fm.];
f.x0 < fm by A4,A11,A22,A33,RFUNCT_2:def 3;
then A35: 0 < fm - f.x0 by SQUARE_1:11;
set R = min(fm - f.x0,f.x0 - fp);
fp < f.x0 by A4,A15,A21,A33,RFUNCT_2:def 3;
then 0 < f.x0 - fp by SQUARE_1:11;
then 0 < R by A35,SQUARE_1:38;
then reconsider N1 = ].r1 - R, r1 + R.[ as Neighbourhood of r1 by RCOMP_1
:def 7;
take N1;
thus N1 c= rng f1
proof let x; assume x in N1;
then x in {r2: r1 - R < r2 & r2 < r1 + R} by RCOMP_1:def 2;
then consider r2 such that
A36: r2 = x & f.x0 - R < r2 & r2 < f.x0 + R by A23;
A37: R <= fm - f.x0 & R <= f.x0 - fp by SQUARE_1:35;
then f.x0 - (f.x0 - fp) <= f.x0 - R by REAL_1:92;
then fp <= f.x0 - R by XCMPLX_1:18;
then A38: fp < r2 by A36,AXIOMS:22;
f.x0 + R <= f.x0 + (fm - f.x0) by A37,REAL_1:55;
then f.x0 + R <= fm by XCMPLX_1:27;
then r2 < fm by A36,AXIOMS:22;
then r2 in {g2: fp < g2 & g2 < fm} by A38;
then A39: r2 in ].fp,fm.[ by RCOMP_1:def 2;
].fp,fm.[ c= [.fp,fm.] by RCOMP_1:15;
then consider s such that
A40: s in [.x0 - r/2, x0 + r/2.] & x = f.s by A18,A19,A34,A36,A39,
FCONT_2:16;
s in N by A6,A17,A40; then s in dom f /\
L by A5,A20,XBOOLE_0:def 3;
then A41: s in dom f1 by FUNCT_1:68;
then x = f1.s by A40,FUNCT_1:68;
hence thesis by A41,FUNCT_1:def 5;
end;
end;
hence ex N be Neighbourhood of r1 st N c= rng f1;
end;
hence thesis by RCOMP_1:41;
end;
theorem
f is_continuous_on [#](REAL) &
(f is_increasing_on [#](REAL) or f is_decreasing_on [#](REAL)) implies
rng f is open
proof set L = [#](REAL); assume that
A1: f is_continuous_on L and
A2: f is_increasing_on L or f is_decreasing_on L;
now dom f c= REAL;
then A3: dom f c= L by SUBSET_1:def 4;
let r1 be real number; assume r1 in rng f;
then consider x0 such that
A4: x0 in dom f & f.x0 = r1 by PARTFUN1:26;
consider N be Neighbourhood of x0 such that
A5: N c= [#] REAL by A3,A4,Th4,RCOMP_1:42;
consider r be real number such that
A6: 0 < r & N = ].x0 - r, x0 + r.[ by RCOMP_1:def 7;
reconsider r as Real by XREAL_0:def 1;
A7: f is_continuous_on N by A1,A5,FCONT_1:17;
A8: r/2 < r by A6,SEQ_2:4;
then A9: x0 - r < x0 - r/2 by REAL_1:92;
A10: 0 < r/2 by A6,SEQ_2:3;
then A11: x0 - r/2 < x0 - 0 by REAL_1:92;
x0 < x0 + r by A6,REAL_2:174;
then x0 - r/2 < x0 + r by A11,AXIOMS:22;
then x0 - r/2 in {g1: x0 - r < g1 & g1 < x0 + r} by A9;
then A12: x0 - r/2 in ].x0 - r, x0 + r.[ by RCOMP_1:def 2;
A13: x0 + r/2 < x0 + r by A8,REAL_1:67;
A14: x0 - r < x0 by A6,REAL_2:174;
A15: x0 < x0 + r/2 by A10,REAL_2:174;
then x0 - r < x0 + r/2 by A14,AXIOMS:22;
then x0 + r/2 in {g2: x0 - r < g2 & g2 < x0 + r} by A13;
then A16: x0 + r/2 in ].x0 - r, x0 + r.[ by RCOMP_1:def 2;
then A17: [.x0 - r/2, x0 + r/2.] c= ].x0 - r, x0 + r.[ by A12,RCOMP_1:17;
then A18: f is_continuous_on [.x0 - r/2, x0 + r/2.] by A6,A7,FCONT_1:17;
set fm = f.(x0 - r/2);
set fp = f.(x0 + r/2);
A19: x0 - r/2 < x0 + r/2 by A11,A15,AXIOMS:22;
A20: N c= dom f by A7,FCONT_1:def 2;
then A21: x0 + r/2 in L /\ dom f by A5,A6,A16,XBOOLE_0:def 3;
A22: x0 - r/2 in L /\ dom f by A5,A6,A12,A20,XBOOLE_0:def 3;
A23: x0 in L /\ dom f by A3,A4,XBOOLE_0:def 3;
now per cases by A2;
suppose A24: f is_increasing_on L;
then fm < fp by A19,A21,A22,RFUNCT_2:def 2;
then [.fp,fm.] = {} by RCOMP_1:13;
then A25: [.fm,fp.] \/ [.fp,fm.] = [.fm,fp.];
fm < f.x0 by A11,A22,A23,A24,RFUNCT_2:def 2;
then A26: 0 < f.x0 - fm by SQUARE_1:11;
set R = min(f.x0 - fm,fp - f.x0);
f.x0 < fp by A15,A21,A23,A24,RFUNCT_2:def 2;
then 0 < fp - f.x0 by SQUARE_1:11;
then 0 < R by A26,SQUARE_1:38;
then reconsider N1 = ].r1 - R, r1 + R.[ as Neighbourhood of r1 by RCOMP_1
:def 7;
take N1;
thus N1 c= rng f
proof let x; assume x in N1;
then x in {r2: r1 - R < r2 & r2 < r1 + R} by RCOMP_1:def 2;
then consider r2 such that
A27: r2 = x & f.x0 - R < r2 & r2 < f.x0 + R by A4;
A28: R <= f.x0 - fm & R <= fp - f.x0 by SQUARE_1:35;
then f.x0 - (f.x0 - fm) <= f.x0 - R by REAL_1:92;
then fm <= f.x0 - R by XCMPLX_1:18;
then A29: fm < r2 by A27,AXIOMS:22;
f.x0 + R <= f.x0 + (fp - f.x0) by A28,REAL_1:55;
then f.x0 + R <= fp by XCMPLX_1:27;
then r2 < fp by A27,AXIOMS:22;
then r2 in {g2: fm < g2 & g2 < fp} by A29;
then A30: r2 in ].fm,fp.[ by RCOMP_1:def 2;
].fm,fp.[ c= [.fm,fp.] by RCOMP_1:15;
then consider s such that
A31: s in [.x0 - r/2, x0 + r/2.] & x = f.s by A18,A19,A25,A27,A30,
FCONT_2:16;
s in N by A6,A17,A31; hence thesis by A20,A31,FUNCT_1:def 5;
end;
suppose A32: f is_decreasing_on L;
then fp < fm by A19,A21,A22,RFUNCT_2:def 3;
then [.fm,fp.] = {} by RCOMP_1:13;
then A33: [.fm,fp.] \/ [.fp,fm.] = [.fp,fm.];
f.x0 < fm by A11,A22,A23,A32,RFUNCT_2:def 3;
then A34: 0 < fm - f.x0 by SQUARE_1:11;
set R = min(fm - f.x0,f.x0 - fp);
fp < f.x0 by A15,A21,A23,A32,RFUNCT_2:def 3;
then 0 < f.x0 - fp by SQUARE_1:11;
then 0 < R by A34,SQUARE_1:38;
then reconsider N1 = ].r1 - R, r1 + R.[ as Neighbourhood of r1 by RCOMP_1
:def 7;
take N1;
thus N1 c= rng f
proof let x; assume x in N1;
then x in {r2: r1 - R < r2 & r2 < r1 + R} by RCOMP_1:def 2;
then consider r2 such that
A35: r2 = x & f.x0 - R < r2 & r2 < f.x0 + R by A4;
A36: R <= fm - f.x0 & R <= f.x0 - fp by SQUARE_1:35;
then f.x0 - (f.x0 - fp) <= f.x0 - R by REAL_1:92;
then fp <= f.x0 - R by XCMPLX_1:18;
then A37: fp < r2 by A35,AXIOMS:22;
f.x0 + R <= f.x0 + (fm - f.x0) by A36,REAL_1:55;
then f.x0 + R <= fm by XCMPLX_1:27;
then r2 < fm by A35,AXIOMS:22;
then r2 in {g2: fp < g2 & g2 < fm} by A37;
then A38: r2 in ].fp,fm.[ by RCOMP_1:def 2;
].fp,fm.[ c= [.fp,fm.] by RCOMP_1:15;
then consider s such that
A39: s in [.x0 - r/2, x0 + r/2.] & x = f.s by A18,A19,A33,A35,A38,
FCONT_2:16;
s in N by A6,A17,A39; hence thesis by A20,A39,FUNCT_1:def 5;
end;
end;
hence ex N be Neighbourhood of r1 st N c= rng f;
end;
hence thesis by RCOMP_1:41;
end;