:: Monotonic and Continuous Real Function
:: by Jaros{\l}aw Kotowicz
::
:: Received January 10, 1991
:: Copyright (c) 1991-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, REAL_1, SUBSET_1, SEQ_1, PARTFUN1, RCOMP_1, XBOOLE_0,
RELAT_1, TARSKI, SEQ_2, LIMFUNC1, FUNCT_1, XXREAL_0, ORDINAL2, CARD_1,
PROB_1, XXREAL_1, ARYTM_1, ARYTM_3, COMPLEX1, FCONT_1, FUNCT_2, VALUED_0,
SEQM_3, NAT_1, ASYMPT_1;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
COMPLEX1, PROB_1, REAL_1, FUNCT_1, FUNCT_2, FUNCOP_1, VALUED_1, SEQ_1,
RELSET_1, COMSEQ_2, SEQ_2, PARTFUN1, PARTFUN2, RCOMP_1, FCONT_1,
LIMFUNC1, XXREAL_0, RFUNCT_2;
constructors PARTFUN1, REAL_1, COMPLEX1, NAT_1, SEQ_2, PROB_1, RCOMP_1,
PARTFUN2, RFUNCT_2, FCONT_1, LIMFUNC1, VALUED_1, XXREAL_2, RELSET_1,
BINOP_2, RVSUM_1, COMSEQ_2, SEQ_1;
registrations ORDINAL1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0, MEMBERED,
RCOMP_1, RFUNCT_2, VALUED_1, FUNCT_2, VALUED_0, XXREAL_2, RELAT_1, SEQ_1,
SEQ_2;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, RCOMP_1;
equalities RCOMP_1, XBOOLE_0, SUBSET_1, PROB_1, LIMFUNC1;
expansions TARSKI, RCOMP_1;
theorems FUNCT_1, NAT_1, SEQ_2, SEQ_4, ABSVALUE, PARTFUN1, PARTFUN2, RCOMP_1,
RFUNCT_2, FCONT_1, SUBSET_1, FCONT_2, TARSKI, FUNCT_2, RELAT_1, XREAL_0,
XBOOLE_0, XBOOLE_1, XREAL_1, COMPLEX1, XXREAL_0, VALUED_1, XXREAL_1,
XXREAL_2, VALUED_0, ORDINAL1, SEQ_1;
schemes SEQ_1, FUNCT_2;
begin
reserve x,X for set;
reserve x0,r1,r2,g,g1,g2,p,s for Real;
reserve r for Real;
reserve n,m for Nat;
reserve a,b,d for Real_Sequence;
reserve f for PartFunc of REAL,REAL;
registration
cluster [#] REAL -> closed;
coherence
by XREAL_0:def 1;
cluster empty -> closed for Subset of REAL;
coherence
by XBOOLE_1:3;
end;
registration
cluster [#] REAL -> open;
coherence
proof
([#] REAL)` = {} REAL by XBOOLE_1:37;
hence thesis;
end;
cluster empty -> open for Subset of REAL;
coherence
proof
let S be Subset of REAL;
assume S is empty;
then S` = [#] REAL;
hence thesis;
end;
end;
registration
let r;
cluster right_closed_halfline(r) -> closed;
coherence
proof
set b = seq_const r;
let a such that
A1: rng a c= right_closed_halfline(r) and
A2: a is convergent;
A3: now
let n;
a.n in rng a by VALUED_0:28;
then a.n in right_closed_halfline(r) by A1;
then a.n in {g1: r <= g1} by XXREAL_1:232;
then ex r1 st a.n = r1 & r <= r1;
hence b.n <= a.n by SEQ_1:57;
end;
lim b = b.0 by SEQ_4:26
.= r by SEQ_1:57;
then r <= lim a by A2,A3,SEQ_2:18;
then (lim a) in {g1: r <= g1};
hence thesis by XXREAL_1:232;
end;
cluster left_closed_halfline(r) -> closed;
coherence
proof
set b = seq_const r;
let a such that
A4: rng a c= left_closed_halfline(r) and
A5: a is convergent;
A6: now
let n;
a.n in rng a by VALUED_0:28;
then a.n in left_closed_halfline(r) by A4;
then a.n in {g: g <= r} by XXREAL_1:231;
then ex r1 st a.n = r1 & r1 <= r;
hence a.n <= b.n by SEQ_1:57;
end;
lim b = b.0 by SEQ_4:26
.= r by SEQ_1:57;
then lim a <= r by A5,A6,SEQ_2:18;
then lim a in {g1: g1 <= r};
hence thesis by XXREAL_1:231;
end;
cluster right_open_halfline(r) -> open;
coherence
proof
(right_open_halfline(r))` = left_closed_halfline(r) by XXREAL_1:224,296;
hence thesis;
end;
cluster halfline(r) -> open;
coherence
proof
(left_open_halfline(r))` = right_closed_halfline(r) by XXREAL_1:224,290;
hence thesis;
end;
end;
theorem Th1:
g in ].x0 - r,x0 + r.[ implies |.g-x0.| < r
proof
assume g in ].x0 - r,x0 + r.[;
then
A1: ex g1 st g1 = g & x0 - r < g1 & g1 < x0 + r;
per cases;
suppose
A2: x0 <= g;
A3: g - x0 < x0 + r - x0 by A1,XREAL_1:14;
0 <= g - x0 by A2,XREAL_1:48;
hence thesis by A3,ABSVALUE:def 1;
end;
suppose
g <= x0;
then 0 <= x0 - g by XREAL_1:48;
then
A4: x0 - g = |.- (g - x0).| by ABSVALUE:def 1
.= |.g - x0.| by COMPLEX1:52;
x0 - g < x0 - (x0 - r) by A1,XREAL_1:15;
hence thesis by A4;
end;
end;
theorem
g in ].x0 - r,x0 + r.[ implies g - x0 in ].-r,r.[
proof
set r1 = g-x0;
assume g in ].x0 - r,x0 + r.[;
then
|.g-x0.| < r by Th1;
then |.r1 - 0.| < r;
then r1 in ].0 - r, 0 + r.[ by RCOMP_1:1;
hence thesis;
end;
theorem Th3:
g = x0 + r1 & |.r1.| < r implies 0 < r & g in ].x0 - r,x0 + r.[
proof
assume that
A1: g = x0 + r1 and
A2: |.r1.| < r;
thus 0 < r by A2,COMPLEX1:46;
|.g - x0.| < r by A1,A2;
hence thesis by RCOMP_1:1;
end;
theorem
g - x0 in ].-r,r.[ implies 0 < r & g in ].x0 - r,x0 + r.[
proof
set r1 = g - x0;
assume r1 in ].-r,r.[;
then ex g1 st g1 = r1 & -r < g1 & g1 < r;
then
A1: |.r1.| < r by SEQ_2:1;
x0 + r1 = g;
hence thesis by A1,Th3;
end;
theorem Th5:
for x0 be Real holds (for n holds a.n = x0 - p/(n+1))
implies a is convergent & lim a = x0
proof
let x0 be Real;
deffunc F(Nat) = p/($1+1);
consider d such that
A1: for n holds d.n = F(n) from SEQ_1:sch 1;
set b = seq_const x0;
assume
A2: for n holds a.n = x0 - p/(n+1);
now
let n be Element of NAT;
thus (b - d).n = b.n - d.n by VALUED_1:15
.= x0 - d.n by SEQ_1:57
.= x0 - p/(n+1) by A1
.=a.n by A2;
end;
then
A3: a = b - d by FUNCT_2:63;
A4: d is convergent by A1,SEQ_4:31;
hence a is convergent by A3;
A5: lim b = b.0 by SEQ_4:26
.= x0 by SEQ_1:57;
lim d = 0 by A1,SEQ_4:31;
hence lim a = x0 - 0 by A4,A5,A3,SEQ_2:12
.= x0;
end;
theorem Th6:
for x0 be Real holds (for n holds a.n = x0 + p/(n+1))
implies a is convergent & lim a = x0
proof
let x0 be Real;
deffunc F(Nat) = p/($1+1);
consider d such that
A1: for n holds d.n = F(n) from SEQ_1:sch 1;
set b = seq_const x0;
assume
A2: for n holds a.n = x0 + p/(n+1);
now
let n be Element of NAT;
thus (b + d).n = b.n + d.n by VALUED_1:1
.= x0 + d.n by SEQ_1:57
.= x0 + p/(n+1) by A1
.=a.n by A2;
end;
then
A3: a = b + d by FUNCT_2:63;
A4: d is convergent by A1,SEQ_4:31;
hence a is convergent by A3;
A5: lim b = b.0 by SEQ_4:26
.= x0 by SEQ_1:57;
lim d = 0 by A1,SEQ_4:31;
hence lim a = x0 + 0 by A4,A5,A3,SEQ_2:6
.= 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 that
A1: f is_continuous_in x0 and
A2: f.x0 <> r;
given N be Neighbourhood of x0 such that
A3: N c= dom f;
consider p be Real such that
A4: 0 < p and
A5: N = ].x0 - p,x0 + p.[ by RCOMP_1:def 6;
defpred P[Nat,Real] means x0 - p/($1+1) < $2 & $2 < x0 + p
/($1+1) & f.$2 = r & $2 in dom f;
assume
A6: for N be Neighbourhood of x0 holds not N c= dom f or ex g st g in N
& f.g = r;
A7: for n being Element of NAT ex g be Element of REAL st P[n,g]
proof
let n be Element of NAT;
A8: 0 <= n by NAT_1:2;
then reconsider
Nn = ].x0 - p/(n+1),x0 + p/(n+1).[ as Neighbourhood of x0 by A4,
RCOMP_1:def 6,XREAL_1:139;
A9: Nn c= dom f
proof
let x be object;
assume x in Nn;
then consider g2 such that
A10: g2 = x and
A11: x0 - p/(n+1) < g2 and
A12: g2 < x0 + p/(n+1);
0 + 1 <= n + 1 by A8,XREAL_1:7;
then
A13: p/(n+1) <= p/1 by A4,XREAL_1:118;
then x0 + p/(n+1) <= x0 + p by XREAL_1:7;
then
A14: g2 < x0 + p by A12,XXREAL_0:2;
x0 - p <= x0 - p/(n+1) by A13,XREAL_1:13;
then x0 - p < g2 by A11,XXREAL_0:2;
then x in N by A5,A10,A14;
hence thesis by A3;
end;
then consider g such that
A15: g in Nn and
A16: f.g = r by A6;
reconsider g as Element of REAL by XREAL_0:def 1;
take g;
ex g1 st g1 = g & x0 - p/(n+1) < g1 & g1 <x0 + p/(n+1) by A15;
hence x0 - p/(n+1) < g & g <x0 + p/(n+1);
thus f.g = r by A16;
thus thesis by A9,A15;
end;
consider d such that
A17: for n being Element of NAT holds P[n,d.n] from FUNCT_2:sch 3(A7);
A18: rng d c= dom f
proof
let x be object;
assume x in rng d;
then ex n being Element of NAT st x = d.n by FUNCT_2:113;
hence thesis by A17;
end;
A19: now
let r2 be Real such that
A20: 0 < r2;
reconsider n = 0 as Nat;
take n;
let m be Nat such that
n <= m;
A21: m in NAT by ORDINAL1:def 12;
|.(f/*d).m - r.| = |.f.(d.m) - r.| by A18,FUNCT_2:108,A21
.= |.r - r.| by A17,A21
.= 0 by ABSVALUE:2;
hence |.(f/*d).m - r.| < r2 by A20;
end;
deffunc F(Nat) = x0 - p/($1+1);
consider a such that
A22: for n holds a.n = F(n) from SEQ_1:sch 1;
deffunc F(Nat) = x0 + p/($1+1);
consider b such that
A23: for n holds b.n = F(n) from SEQ_1:sch 1;
A24: now
let n;
n in NAT by ORDINAL1:def 12;
then x0 - p/(n+1) < d.n & d.n < x0 + p/(n+1) by A17;
hence a.n <= d.n & d.n <= b.n by A22,A23;
end;
A25: b is convergent & lim b = x0 by A23,Th6;
a is convergent & lim a = x0 by A22,Th5;
then d is convergent & lim d = x0 by A25,A24,SEQ_2:19,20;
then f/*d is convergent & f.x0 = lim (f/*d) by A1,A18,FCONT_1:def 1;
hence contradiction by A2,A19,SEQ_2:def 7;
end;
theorem
f|X is increasing or f|X is decreasing implies f|X is one-to-one
proof
assume
A1: f|X is increasing or f|X is decreasing;
now
per cases by A1;
suppose
A2: f|X is increasing;
now
given r1,r2 being Element of REAL such that
A3: r1 in dom (f|X) and
A4: r2 in dom (f|X) and
A5: (f|X).r1 = (f|X).r2 and
A6: r1 <> r2;
A7: r1 in X /\ dom f & r2 in X /\ dom f by A3,A4,RELAT_1:61;
now
per cases by A6,XXREAL_0:1;
suppose
r1 < r2;
then f.r1 < f.r2 by A2,A7,RFUNCT_2:20;
then (f|X).r1 < f.r2 by A3,FUNCT_1:47;
hence contradiction by A4,A5,FUNCT_1:47;
end;
suppose
r2 < r1;
then f.r2 < f.r1 by A2,A7,RFUNCT_2:20;
then (f|X).r2 < f.r1 by A4,FUNCT_1:47;
hence contradiction by A3,A5,FUNCT_1:47;
end;
end;
hence contradiction;
end;
hence thesis by PARTFUN1:8;
end;
suppose
A8: f|X is decreasing;
now
given r1,r2 being Element of REAL such that
A9: r1 in dom (f|X) and
A10: r2 in dom (f|X) and
A11: (f|X).r1 = (f|X).r2 and
A12: r1 <> r2;
A13: r1 in X /\ dom f & r2 in X /\ dom f by A9,A10,RELAT_1:61;
now
per cases by A12,XXREAL_0:1;
suppose
r1 < r2;
then f.r2 < f.r1 by A8,A13,RFUNCT_2:21;
then (f|X).r2 < f.r1 by A10,FUNCT_1:47;
hence contradiction by A9,A11,FUNCT_1:47;
end;
suppose
r2 < r1;
then f.r1 < f.r2 by A8,A13,RFUNCT_2:21;
then (f|X).r1 < f.r2 by A9,FUNCT_1:47;
hence contradiction by A10,A11,FUNCT_1:47;
end;
end;
hence contradiction;
end;
hence thesis by PARTFUN1:8;
end;
end;
hence thesis;
end;
theorem Th9:
for f be one-to-one PartFunc of REAL,REAL st f|X is increasing
holds (f|X)"|(f.:X) is increasing
proof
let f be one-to-one PartFunc of REAL,REAL;
assume that
A1: f|X is increasing and
A2: not (f|X)"|(f.:X) is increasing;
consider r1,r2 such that
A3: r1 in f.:X /\ dom ((f|X)") and
A4: r2 in f.:X /\ dom((f|X)") and
A5: r1 < r2 and
A6: ((f|X)").r1 >= ((f|X)").r2 by A2,RFUNCT_2:20;
A7: f.:X = rng (f|X) by RELAT_1:115;
then
A8: r1 in rng (f|X) by A3,XBOOLE_0:def 4;
A9: r2 in rng (f|X) by A4,A7,XBOOLE_0:def 4;
A10: f|X|X is increasing by A1;
now
per cases;
suppose
((f|X)").r1 = ((f|X)").r2;
then r1 = (f|X).(((f|X)").r2) by A8,FUNCT_1:35
.= r2 by A9,FUNCT_1:35;
hence contradiction by A5;
end;
suppose
A11: ((f|X)").r1 <> ((f|X)").r2;
A12: dom (f|X) = dom ((f|X)|X)
.= X /\ dom (f|X) by RELAT_1:61;
r1 in REAL & r2 in REAL &
((f|X)").r2 in REAL & ((f|X)").r1 in REAL by XREAL_0:def 1;
then
A13: ((f|X)").r2 in dom (f|X) & ((f|X)").r1 in dom (f|X) by A8,A9,PARTFUN2:60;
((f|X)").r2 < ((f|X)").r1 by A6,A11,XXREAL_0:1;
then (f|X).(((f|X)").r2) < (f|X).(((f|X)").r1) by A10,A13,A12,RFUNCT_2:20
;
then r2 < (f|X).(((f|X)").r1) by A9,FUNCT_1:35;
hence contradiction by A5,A8,FUNCT_1:35;
end;
end;
hence contradiction;
end;
theorem Th10:
for f be one-to-one PartFunc of REAL,REAL st f|X is decreasing
holds (f|X)"|(f.:X) is decreasing
proof
let f be one-to-one PartFunc of REAL,REAL;
assume that
A1: f|X is decreasing and
A2: not (f|X)"|(f.:X) is decreasing;
consider r1,r2 such that
A3: r1 in f.:X /\ dom ((f|X)") and
A4: r2 in f.:X /\ dom((f|X)") and
A5: r1 < r2 and
A6: ((f|X)").r1 <= ((f|X)").r2 by A2,RFUNCT_2:21;
A7: f.:X = rng (f|X) by RELAT_1:115;
then
A8: r1 in rng (f|X) by A3,XBOOLE_0:def 4;
A9: r2 in rng (f|X) by A4,A7,XBOOLE_0:def 4;
A10: f|X|X is decreasing by A1;
now
per cases;
suppose
((f|X)").r1 = ((f|X)").r2;
then r1 = (f|X).(((f|X)").r2) by A8,FUNCT_1:35
.= r2 by A9,FUNCT_1:35;
hence contradiction by A5;
end;
suppose
A11: ((f|X)").r1 <> ((f|X)").r2;
A12: dom (f|X) = dom ((f|X)|X)
.= X /\ dom (f|X) by RELAT_1:61;
r1 in REAL & r2 in REAL &
((f|X)").r2 in REAL & ((f|X)").r1 in REAL by XREAL_0:def 1;
then
A13: ((f|X)").r2 in dom (f|X) & ((f|X)").r1 in dom (f|X) by A8,A9,PARTFUN2:60;
((f|X)").r2 > ((f|X)").r1 by A6,A11,XXREAL_0:1;
then (f|X).(((f|X)").r2) < (f|X).(((f|X)").r1)
by A10,A13,A12,RFUNCT_2:21;
then r2 < (f|X).(((f|X)").r1) by A9,FUNCT_1:35;
hence contradiction by A5,A8,FUNCT_1:35;
end;
end;
hence contradiction;
end;
theorem Th11:
X c= dom f & f|X is monotone & (ex p st f.:X =
left_open_halfline(p)) implies f|X is continuous
proof
assume that
A1: X c= dom f and
A2: f|X is monotone;
given p such that
A3: f.:X = left_open_halfline(p);
set L = left_open_halfline(p);
now
per cases by A2,RFUNCT_2:def 5;
suppose
f|X is non-decreasing;
then
A4: f|X|X is non-decreasing;
for x0 be Real st x0 in dom(f|X) holds f|X is_continuous_in x0
proof
let x0 be Real;
A5: (f|X).:X = f.:X by RELAT_1:129;
assume x0 in dom(f|X);
then
x0 in X;
then x0 in dom f /\ X by A1,XBOOLE_0:def 4;
then
A6: x0 in dom (f|X) by RELAT_1:61;
then (f|X).x0 in (f|X).:X by FUNCT_1:def 6;
then
A7: (f|X).x0 in L by A3,RELAT_1:129;
now
let N1 be Neighbourhood of (f|X).x0;
consider N2 being Neighbourhood of (f|X).x0 such that
A8: N2 c= L by A7,RCOMP_1:18;
consider N3 being Neighbourhood of (f|X).x0 such that
A9: N3 c= N1 and
A10: N3 c= N2 by RCOMP_1:17;
consider r be Real such that
A11: r>0 and
A12: N3 = ].(f|X).x0 - r,(f|X).x0 + r.[ by RCOMP_1:def 6;
reconsider r as Real;
A13: (f|X).x0 + r/2 < (f|X).x0 + r/2 + r/2 by A11,XREAL_1:29,215;
set M2 = (f|X).x0 + r/2;
A14: (f|X).x0 < (f|X).x0 + r/2 by A11,XREAL_1:29,215;
A15: (f|X).x0 < (f|X).x0 + r by A11,XREAL_1:29;
then (f|X).x0 - r < (f|X).x0 + r - r by XREAL_1:9;
then (f|X).x0 - r < (f|X).x0 + r/2 by A14,XXREAL_0:2;
then
A16: M2 in ].(f|X).x0 - r,(f|X).x0 + r.[ by A13;
then M2 in N2 by A10,A12;
then consider r2 being Element of REAL such that
A17: r2 in dom (f|X) & r2 in X and
A18: M2 = (f|X).r2 by A3,A5,A8,PARTFUN2:59;
A19: M2 > (f|X).x0 by A11,XREAL_1:29,215;
A20: now
assume
A21: r2 < x0;
x0 in X /\ dom(f|X) & r2 in X /\ dom (f|X) by A6,A17,XBOOLE_0:def 4
;
hence contradiction by A4,A18,A19,A21,RFUNCT_2:22;
end;
set M1 = (f|X).x0 - r/2;
A22: (f|X).x0 - r < (f|X).x0 - r + r/2 by A11,XREAL_1:29,215;
(f|X).x0 - r/2 < (f|X).x0 by A14,XREAL_1:19;
then (f|X).x0 - r/2 < (f|X).x0 + r by A15,XXREAL_0:2;
then
A23: M1 in ].(f|X).x0 - r,(f|X).x0 + r.[ by A22;
then M1 in N2 by A10,A12;
then consider r1 being Element of REAL such that
A24: r1 in dom (f|X) & r1 in X and
A25: M1 = (f|X).r1 by A3,A5,A8,PARTFUN2:59;
A26: (f|X).x0 < (f|X).x0 + r/2 by A11,XREAL_1:29,215;
then
A27: M1 < (f|X).x0 by XREAL_1:19;
A28: now
assume
A29: x0 < r1;
x0 in X /\ dom( f|X) & r1 in X /\ dom(f|X) by A6,A24,XBOOLE_0:def 4
;
hence contradiction by A4,A25,A27,A29,RFUNCT_2:22;
end;
x0 <> r2 by A11,A18,XREAL_1:29,215;
then x0 < r2 by A20,XXREAL_0:1;
then
A30: r2 - x0 > 0 by XREAL_1:50;
set R = min(x0 - r1,r2 - x0);
A31: R <= r2 - x0 by XXREAL_0:17;
r1 <> x0 by A25,A26,XREAL_1:19;
then r1 < x0 by A28,XXREAL_0:1;
then x0 - r1 > 0 by XREAL_1:50;
then R > 0 by A30,XXREAL_0:15;
then reconsider N = ].x0 - R,x0 + R.[ as Neighbourhood of x0 by
RCOMP_1:def 6;
take N;
let x be Real;
assume that
A32: x in dom (f|X) and
A33: x in N;
A34: x in X /\ dom (f|X) by A32,XBOOLE_1:28;
A35: ex s st s = x & x0 - R < s & s < x0 + R by A33;
then x0 < R + x by XREAL_1:19;
then
A36: x0 - x < R + x - x by XREAL_1:9;
R <= x0 - r1 by XXREAL_0:17;
then x0 - x < x0 - r1 by A36,XXREAL_0:2;
then -(x0 - x) > -(x0 - r1) by XREAL_1:24;
then
A37: x - x0 + x0 > r1 - x0 + x0 by XREAL_1:6;
r1 in X /\ dom (f|X) by A24,XBOOLE_0:def 4;
then
A38: (f|X).r1 <= (f|X).x by A4,A37,A34,RFUNCT_2:22;
x - x0 < R by A35,XREAL_1:19;
then x - x0 < r2 - x0 by A31,XXREAL_0:2;
then
A39: x - x0 + x0 < r2 - x0 + x0 by XREAL_1:6;
r2 in X /\ dom (f|X) by A17,XBOOLE_0:def 4;
then (f|X).x <= (f|X).r2 by A4,A39,A34,RFUNCT_2:22;
then
A40: (f|X).x in [.M1,M2.] by A25,A18,A38;
[.M1,M2.] c= ].(f|X).x0 - r,(f|X).x0 + r.[ by A23,A16,XXREAL_2:def 12
;
then (f|X).x in N3 by A12,A40;
hence (f|X).x in N1 by A9;
end;
hence thesis by FCONT_1:4;
end;
hence thesis by FCONT_1:def 2;
end;
suppose
f|X is non-increasing;
then
A41: f|X|X is non-increasing;
for x0 be Real st x0 in dom(f|X) holds f|X is_continuous_in x0
proof
let x0 be Real;
A42: (f|X).:X = f.:X by RELAT_1:129;
assume x0 in dom(f|X);
then
x0 in X;
then x0 in dom f /\ X by A1,XBOOLE_0:def 4;
then
A43: x0 in dom(f|X) by RELAT_1:61;
then (f|X).x0 in (f|X).:X by FUNCT_1:def 6;
then
A44: (f|X).x0 in L by A3,RELAT_1:129;
now
let N1 be Neighbourhood of (f|X).x0;
consider N2 being Neighbourhood of (f|X).x0 such that
A45: N2 c= L by A44,RCOMP_1:18;
consider N3 being Neighbourhood of (f|X).x0 such that
A46: N3 c= N1 and
A47: N3 c= N2 by RCOMP_1:17;
consider r be Real such that
A48: r > 0 and
A49: N3 = ].(f|X).x0 - r,(f|X).x0 + r.[ by RCOMP_1:def 6;
reconsider r as Real;
A50: (f|X).x0 + r/2 < (f|X).x0 + r/2 + r/2 by A48,XREAL_1:29,215;
set M2 = (f|X).x0 + r/2;
A51: (f|X).x0 < (f|X).x0 + r/2 by A48,XREAL_1:29,215;
A52: (f|X).x0 < (f|X).x0 + r by A48,XREAL_1:29;
then (f|X).x0 - r < (f|X).x0 + r - r by XREAL_1:9;
then (f|X).x0 - r < (f|X).x0 + r/2 by A51,XXREAL_0:2;
then
A53: M2 in ].(f|X).x0 - r,(f|X).x0 + r.[ by A50;
then M2 in N2 by A47,A49;
then consider r2 being Element of REAL such that
A54: r2 in dom (f|X) & r2 in X and
A55: M2 = (f|X).r2 by A3,A42,A45,PARTFUN2:59;
A56: M2 > (f|X).x0 by A48,XREAL_1:29,215;
A57: now
assume
A58: r2 > x0;
x0 in X /\ dom (f|X) & r2 in X /\ dom (f|X)
by A43,A54,XBOOLE_0:def 4;
hence contradiction by A41,A55,A56,A58,RFUNCT_2:23;
end;
set M1 = (f|X).x0 - r/2;
A59: (f|X).x0 - r < (f|X).x0 - r + r/2 by A48,XREAL_1:29,215;
(f|X).x0 - r/2 < (f|X).x0 by A51,XREAL_1:19;
then (f|X).x0 - r/2 < (f|X).x0 + r by A52,XXREAL_0:2;
then
A60: M1 in ].(f|X).x0 - r,(f|X).x0 + r.[ by A59;
then M1 in N2 by A47,A49;
then consider r1 being Element of REAL such that
A61: r1 in dom (f|X) & r1 in X and
A62: M1 = (f|X).r1 by A3,A42,A45,PARTFUN2:59;
A63: (f|X).x0 < (f|X).x0 + r/2 by A48,XREAL_1:29,215;
then
A64: M1 < (f|X).x0 by XREAL_1:19;
A65: now
assume
A66: x0 > r1;
x0 in X /\ dom (f|X) & r1 in X /\ dom(f|X)
by A43,A61,XBOOLE_0:def 4;
hence contradiction by A41,A62,A64,A66,RFUNCT_2:23;
end;
x0 <> r2 by A48,A55,XREAL_1:29,215;
then x0 > r2 by A57,XXREAL_0:1;
then
A67: x0 - r2 > 0 by XREAL_1:50;
set R = min(r1 - x0,x0 - r2);
A68: R <= r1 - x0 by XXREAL_0:17;
r1 <> x0 by A62,A63,XREAL_1:19;
then r1 > x0 by A65,XXREAL_0:1;
then r1 - x0 > 0 by XREAL_1:50;
then R > 0 by A67,XXREAL_0:15;
then reconsider N = ].x0 - R,x0 + R.[ as Neighbourhood of x0 by
RCOMP_1:def 6;
take N;
let x be Real;
assume that
A69: x in dom (f|X) and
A70: x in N;
A71: x in X /\ dom(f|X) by A69,XBOOLE_1:28;
A72: ex s st s = x & x0 - R < s & s < x0 + R by A70;
then x0 < R + x by XREAL_1:19;
then
A73: x0 - x < R + x - x by XREAL_1:9;
x - x0 < R by A72,XREAL_1:19;
then x - x0 < r1-x0 by A68,XXREAL_0:2;
then
A74: x - x0 + x0 < r1 - x0 + x0 by XREAL_1:6;
r1 in X /\ dom(f|X) by A61,XBOOLE_0:def 4;
then
A75: (f|X).r1 <= (f|X).x by A41,A74,A71,RFUNCT_2:23;
R <= x0 - r2 by XXREAL_0:17;
then x0 - x < x0 - r2 by A73,XXREAL_0:2;
then -(x0 - x) > -(x0 - r2) by XREAL_1:24;
then
A76: x - x0 + x0 > r2 - x0 + x0 by XREAL_1:6;
r2 in X /\ dom(f|X) by A54,XBOOLE_0:def 4;
then (f|X).x <= (f|X).r2 by A41,A76,A71,RFUNCT_2:23;
then
A77: (f|X).x in [.M1,M2.] by A62,A55,A75;
[.M1,M2.] c= ].(f|X).x0 - r,(f|X).x0 + r.[ by A60,A53,XXREAL_2:def 12
;
then (f|X).x in N3 by A49,A77;
hence (f|X).x in N1 by A46;
end;
hence thesis by FCONT_1:4;
end;
hence thesis by FCONT_1:def 2;
end;
end;
hence thesis;
end;
theorem Th12:
X c= dom f & f|X is monotone & (ex p st f.:X =
right_open_halfline(p)) implies f|X is continuous
proof
assume that
A1: X c= dom f and
A2: f|X is monotone;
given p such that
A3: f.:X = right_open_halfline(p);
set L = right_open_halfline(p);
now
per cases by A2,RFUNCT_2:def 5;
suppose
f|X is non-decreasing;
then
A4: f|X|X is non-decreasing;
for x0 be Real st x0 in dom(f|X) holds f|X is_continuous_in x0
proof
let x0 be Real;
A5: (f|X).:X = f.:X by RELAT_1:129;
assume x0 in dom(f|X);
then
x0 in X;
then x0 in dom f /\ X by A1,XBOOLE_0:def 4;
then
A6: x0 in dom (f|X) by RELAT_1:61;
then (f|X).x0 in (f|X).:X by FUNCT_1:def 6;
then
A7: (f|X).x0 in L by A3,RELAT_1:129;
now
let N1 be Neighbourhood of (f|X).x0;
consider N2 being Neighbourhood of (f|X).x0 such that
A8: N2 c= L by A7,RCOMP_1:18;
consider N3 being Neighbourhood of (f|X).x0 such that
A9: N3 c= N1 and
A10: N3 c= N2 by RCOMP_1:17;
consider r be Real such that
A11: r>0 and
A12: N3 = ].(f|X).x0 - r,(f|X).x0 + r.[ by RCOMP_1:def 6;
reconsider r as Real;
A13: (f|X).x0 + r/2 < (f|X).x0 + r/2 + r/2 by A11,XREAL_1:29,215;
set M2 = (f|X).x0 + r/2;
A14: (f|X).x0 < (f|X).x0 + r/2 by A11,XREAL_1:29,215;
A15: (f|X).x0 < (f|X).x0 + r by A11,XREAL_1:29;
then (f|X).x0 - r < (f|X).x0 + r - r by XREAL_1:9;
then (f|X).x0 - r < (f|X).x0 + r/2 by A14,XXREAL_0:2;
then
A16: M2 in ].(f|X).x0 - r,(f|X).x0 + r.[ by A13;
then M2 in N2 by A10,A12;
then consider r2 being Element of REAL such that
A17: r2 in dom (f|X) & r2 in X and
A18: M2 = (f|X).r2 by A3,A5,A8,PARTFUN2:59;
A19: M2 > (f|X).x0 by A11,XREAL_1:29,215;
A20: now
assume
A21: r2 < x0;
x0 in X /\ dom(f|X) & r2 in X /\ dom (f|X) by A6,A17,XBOOLE_0:def 4
;
hence contradiction by A4,A18,A19,A21,RFUNCT_2:22;
end;
set M1 = (f|X).x0 - r/2;
A22: (f|X).x0 - r < (f|X).x0 - r + r/2 by A11,XREAL_1:29,215;
(f|X).x0 - r/2 < (f|X).x0 by A14,XREAL_1:19;
then (f|X).x0 - r/2 < (f|X).x0 + r by A15,XXREAL_0:2;
then
A23: M1 in ].(f|X).x0 - r,(f|X).x0 + r.[ by A22;
then M1 in N2 by A10,A12;
then consider r1 being Element of REAL such that
A24: r1 in dom (f|X) & r1 in X and
A25: M1 = (f|X).r1 by A3,A5,A8,PARTFUN2:59;
A26: (f|X).x0 < (f|X).x0 + r/2 by A11,XREAL_1:29,215;
then
A27: M1 < (f|X).x0 by XREAL_1:19;
A28: now
assume
A29: x0 < r1;
x0 in X /\ dom( f|X) & r1 in X /\ dom(f|X) by A6,A24,XBOOLE_0:def 4
;
hence contradiction by A4,A25,A27,A29,RFUNCT_2:22;
end;
x0 <> r2 by A11,A18,XREAL_1:29,215;
then x0 < r2 by A20,XXREAL_0:1;
then
A30: r2 - x0 > 0 by XREAL_1:50;
set R = min(x0 - r1,r2 - x0);
A31: R <= r2 - x0 by XXREAL_0:17;
r1 <> x0 by A25,A26,XREAL_1:19;
then r1 < x0 by A28,XXREAL_0:1;
then x0 - r1 > 0 by XREAL_1:50;
then R > 0 by A30,XXREAL_0:15;
then reconsider N = ].x0 - R,x0 + R.[ as Neighbourhood of x0 by
RCOMP_1:def 6;
take N;
let x be Real;
assume that
A32: x in dom (f|X) and
A33: x in N;
A34: x in X /\ dom (f|X) by A32,XBOOLE_1:28;
A35: ex s st s = x & x0 - R < s & s < x0 + R by A33;
then x0 < R + x by XREAL_1:19;
then
A36: x0 - x < R + x - x by XREAL_1:9;
R <= x0 - r1 by XXREAL_0:17;
then x0 - x < x0 - r1 by A36,XXREAL_0:2;
then -(x0 - x) > -(x0 - r1) by XREAL_1:24;
then
A37: x - x0 + x0 > r1 - x0 + x0 by XREAL_1:6;
r1 in X /\ dom (f|X) by A24,XBOOLE_0:def 4;
then
A38: (f|X).r1 <= (f|X).x by A4,A37,A34,RFUNCT_2:22;
x - x0 < R by A35,XREAL_1:19;
then x - x0 < r2 - x0 by A31,XXREAL_0:2;
then
A39: x - x0 + x0 < r2 - x0 + x0 by XREAL_1:6;
r2 in X /\ dom (f|X) by A17,XBOOLE_0:def 4;
then (f|X).x <= (f|X).r2 by A4,A39,A34,RFUNCT_2:22;
then
A40: (f|X).x in [.M1,M2.] by A25,A18,A38;
[.M1,M2.] c= ].(f|X).x0 - r,(f|X).x0 + r.[ by A23,A16,XXREAL_2:def 12
;
then (f|X).x in N3 by A12,A40;
hence (f|X).x in N1 by A9;
end;
hence thesis by FCONT_1:4;
end;
hence thesis by FCONT_1:def 2;
end;
suppose
f|X is non-increasing;
then
A41: f|X|X is non-increasing;
for x0 be Real st x0 in dom(f|X) holds f|X is_continuous_in x0
proof
let x0 be Real;
A42: (f|X).:X = f.:X by RELAT_1:129;
assume x0 in dom(f|X);
then
x0 in X;
then x0 in dom f /\ X by A1,XBOOLE_0:def 4;
then
A43: x0 in dom(f|X) by RELAT_1:61;
then (f|X).x0 in (f|X).:X by FUNCT_1:def 6;
then
A44: (f|X).x0 in L by A3,RELAT_1:129;
now
let N1 be Neighbourhood of (f|X).x0;
consider N2 being Neighbourhood of (f|X).x0 such that
A45: N2 c= L by A44,RCOMP_1:18;
consider N3 being Neighbourhood of (f|X).x0 such that
A46: N3 c= N1 and
A47: N3 c= N2 by RCOMP_1:17;
consider r be Real such that
A48: r > 0 and
A49: N3 = ].(f|X).x0 - r,(f|X).x0 + r.[ by RCOMP_1:def 6;
reconsider r as Real;
A50: (f|X).x0 + r/2 < (f|X).x0 + r/2 + r/2 by A48,XREAL_1:29,215;
set M2 = (f|X).x0 + r/2;
A51: (f|X).x0 < (f|X).x0 + r/2 by A48,XREAL_1:29,215;
A52: (f|X).x0 < (f|X).x0 + r by A48,XREAL_1:29;
then (f|X).x0 - r < (f|X).x0 + r - r by XREAL_1:9;
then (f|X).x0 - r < (f|X).x0 + r/2 by A51,XXREAL_0:2;
then
A53: M2 in ].(f|X).x0 - r,(f|X).x0 + r.[ by A50;
then M2 in N2 by A47,A49;
then consider r2 being Element of REAL such that
A54: r2 in dom (f|X) & r2 in X and
A55: M2 = (f|X).r2 by A3,A42,A45,PARTFUN2:59;
A56: M2 > (f|X).x0 by A48,XREAL_1:29,215;
A57: now
assume
A58: r2 > x0;
x0 in X /\ dom (f|X) & r2 in X /\ dom (f|X)
by A43,A54,XBOOLE_0:def 4;
hence contradiction by A41,A55,A56,A58,RFUNCT_2:23;
end;
set M1 = (f|X).x0 - r/2;
A59: (f|X).x0 - r < (f|X).x0 - r + r/2 by A48,XREAL_1:29,215;
(f|X).x0 - r/2 < (f|X).x0 by A51,XREAL_1:19;
then (f|X).x0 - r/2 < (f|X).x0 + r by A52,XXREAL_0:2;
then
A60: M1 in ].(f|X).x0 - r,(f|X).x0 + r.[ by A59;
then M1 in N2 by A47,A49;
then consider r1 being Element of REAL such that
A61: r1 in dom (f|X) & r1 in X and
A62: M1 = (f|X).r1 by A3,A42,A45,PARTFUN2:59;
A63: (f|X).x0 < (f|X).x0 + r/2 by A48,XREAL_1:29,215;
then
A64: M1 < (f|X).x0 by XREAL_1:19;
A65: now
assume
A66: x0 > r1;
x0 in X /\ dom (f|X) & r1 in X /\ dom(f|X)
by A43,A61,XBOOLE_0:def 4;
hence contradiction by A41,A62,A64,A66,RFUNCT_2:23;
end;
x0 <> r2 by A48,A55,XREAL_1:29,215;
then x0 > r2 by A57,XXREAL_0:1;
then
A67: x0 - r2 > 0 by XREAL_1:50;
set R = min(r1 - x0,x0 - r2);
A68: R <= r1 - x0 by XXREAL_0:17;
r1 <> x0 by A62,A63,XREAL_1:19;
then r1 > x0 by A65,XXREAL_0:1;
then r1 - x0 > 0 by XREAL_1:50;
then R > 0 by A67,XXREAL_0:15;
then reconsider N = ].x0 - R,x0 + R.[ as Neighbourhood of x0 by
RCOMP_1:def 6;
take N;
let x be Real;
assume that
A69: x in dom (f|X) and
A70: x in N;
A71: x in X /\ dom(f|X) by A69,XBOOLE_1:28;
A72: ex s st s = x & x0 - R < s & s < x0 + R by A70;
then x0 < R + x by XREAL_1:19;
then
A73: x0 - x < R + x - x by XREAL_1:9;
x - x0 < R by A72,XREAL_1:19;
then x - x0 < r1-x0 by A68,XXREAL_0:2;
then
A74: x - x0 + x0 < r1 - x0 + x0 by XREAL_1:6;
r1 in X /\ dom(f|X) by A61,XBOOLE_0:def 4;
then
A75: (f|X).r1 <= (f|X).x by A41,A74,A71,RFUNCT_2:23;
R <= x0 - r2 by XXREAL_0:17;
then x0 - x < x0 - r2 by A73,XXREAL_0:2;
then -(x0 - x) > -(x0 - r2) by XREAL_1:24;
then
A76: x - x0 + x0 > r2 - x0 + x0 by XREAL_1:6;
r2 in X /\ dom(f|X) by A54,XBOOLE_0:def 4;
then (f|X).x <= (f|X).r2 by A41,A76,A71,RFUNCT_2:23;
then
A77: (f|X).x in [.M1,M2.] by A62,A55,A75;
[.M1,M2.] c= ].(f|X).x0 - r,(f|X).x0 + r.[ by A60,A53,XXREAL_2:def 12
;
then (f|X).x in N3 by A49,A77;
hence (f|X).x in N1 by A46;
end;
hence thesis by FCONT_1:4;
end;
hence thesis by FCONT_1:def 2;
end;
end;
hence thesis;
end;
theorem Th13:
X c= dom f & f|X is monotone & (ex p st f.:X =
left_closed_halfline(p)) implies f|X is continuous
proof
assume that
A1: X c= dom f and
A2: f|X is monotone;
given p such that
A3: f.:X = left_closed_halfline(p);
set L = left_open_halfline(p);
set l = left_closed_halfline(p);
for x0 be Real st x0 in dom(f|X) holds f|X is_continuous_in x0
proof
let x0 be Real;
A4: (f|X).:X = f.:X by RELAT_1:129;
A5: L c= l by XXREAL_1:21;
assume x0 in dom(f|X);
then
x0 in X;
then x0 in dom f /\ X by A1,XBOOLE_0:def 4;
then
A6: x0 in dom (f|X) by RELAT_1:61;
then (f|X).x0 in (f|X).:X by FUNCT_1:def 6;
then (f|X).x0 in {p} \/ L by A3,A4,XXREAL_1:423;
then
A7: (f|X).x0 in {p} or (f|X).x0 in L by XBOOLE_0:def 3;
now
let N1 be Neighbourhood of (f|X).x0;
now
per cases by A2,RFUNCT_2:def 5;
suppose
f|X is non-decreasing;
then
A8: f|X|X is non-decreasing;
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
A9: N2 c= L by RCOMP_1:18;
consider N3 being Neighbourhood of (f|X).x0 such that
A10: N3 c= N1 and
A11: N3 c= N2 by RCOMP_1:17;
consider r be Real such that
A12: r>0 and
A13: N3 = ].(f|X).x0 - r,(f|X).x0 + r.[ by RCOMP_1:def 6;
reconsider r as Real;
A14: (f|X).x0 + r/2 < (f|X).x0 + r/2 + r/2 by A12,XREAL_1:29,215;
set M2 = (f|X).x0 + r/2;
A15: (f|X).x0 < (f|X).x0 + r/2 by A12,XREAL_1:29,215;
A16: (f|X).x0 < (f|X).x0 + r by A12,XREAL_1:29;
then (f|X).x0 - r < (f|X).x0 + r - r by XREAL_1:9;
then (f|X).x0 - r < (f|X).x0 + r/2 by A15,XXREAL_0:2;
then
A17: M2 in ].(f|X).x0 - r,(f|X).x0 + r.[ by A14;
then M2 in N2 by A11,A13;
then M2 in L by A9;
then consider r2 being Element of REAL such that
A18: r2 in dom (f|X) & r2 in X and
A19: M2 = (f|X).r2 by A3,A4,A5,PARTFUN2:59;
A20: M2 > (f|X).x0 by A12,XREAL_1:29,215;
A21: now
assume
A22: r2 < x0;
x0 in X /\ dom(f|X) & r2 in X /\ dom (f|X) by A6,A18,
XBOOLE_0:def 4;
hence contradiction by A8,A19,A20,A22,RFUNCT_2:22;
end;
set M1 = (f|X).x0 - r/2;
A23: (f|X).x0 - r < (f|X).x0 - r + r/2 by A12,XREAL_1:29,215;
(f|X).x0 - r/2 < (f|X).x0 by A15,XREAL_1:19;
then (f|X).x0 - r/2 < (f|X).x0 + r by A16,XXREAL_0:2;
then
A24: M1 in ].(f|X).x0 - r,(f|X).x0 + r.[ by A23;
then M1 in N2 by A11,A13;
then M1 in L by A9;
then consider r1 being Element of REAL such that
A25: r1 in dom (f|X) & r1 in X and
A26: M1 = (f|X).r1 by A3,A4,A5,PARTFUN2:59;
A27: (f|X).x0 < (f|X).x0 + r/2 by A12,XREAL_1:29,215;
then
A28: M1 < (f|X).x0 by XREAL_1:19;
A29: now
assume
A30: x0 < r1;
x0 in X /\ dom( f|X) & r1 in X /\ dom(f|X) by A6,A25,
XBOOLE_0:def 4;
hence contradiction by A8,A26,A28,A30,RFUNCT_2:22;
end;
x0 <> r2 by A12,A19,XREAL_1:29,215;
then x0 < r2 by A21,XXREAL_0:1;
then
A31: r2 - x0 > 0 by XREAL_1:50;
set R = min(x0 - r1,r2 - x0);
A32: R <= r2 - x0 by XXREAL_0:17;
r1 <> x0 by A26,A27,XREAL_1:19;
then r1 < x0 by A29,XXREAL_0:1;
then x0 - r1 > 0 by XREAL_1:50;
then R > 0 by A31,XXREAL_0:15;
then reconsider N = ].x0 - R,x0+ R.[ as Neighbourhood of x0 by
RCOMP_1:def 6;
take N;
let x be Real;
assume that
A33: x in dom (f|X) and
A34: x in N;
A35: x in X /\ dom (f|X) by A33,XBOOLE_1:28;
A36: ex s st s = x & x0 - R < s & s < x0 + R by A34;
then x0 < R + x by XREAL_1:19;
then
A37: x0 - x < R + x - x by XREAL_1:9;
R <= x0 - r1 by XXREAL_0:17;
then x0 - x < x0 - r1 by A37,XXREAL_0:2;
then -(x0 - x) > -(x0 - r1) by XREAL_1:24;
then
A38: x - x0 + x0 > r1 - x0 + x0 by XREAL_1:6;
r1 in X /\ dom (f|X) by A25,XBOOLE_0:def 4;
then
A39: (f|X).r1 <= (f|X).x by A8,A38,A35,RFUNCT_2:22;
x - x0 < R by A36,XREAL_1:19;
then x - x0 < r2 - x0 by A32,XXREAL_0:2;
then
A40: x - x0 + x0 < r2 - x0 + x0 by XREAL_1:6;
r2 in X /\ dom (f|X) by A18,XBOOLE_0:def 4;
then (f|X).x <= (f|X).r2 by A8,A40,A35,RFUNCT_2:22;
then
A41: (f|X).x in [.M1,M2.] by A26,A19,A39;
[.M1,M2.] c= ].(f|X).x0 - r,(f|X).x0 + r.[ by A24,A17,
XXREAL_2:def 12;
then (f|X).x in N3 by A13,A41;
hence (f|X).x in N1 by A10;
end;
suppose
A42: (f|X).x0 = p;
then consider r be Real such that
A43: r > 0 and
A44: N1 = ].p - r,p + r.[ by RCOMP_1:def 6;
reconsider r as Real;
set R = r/2;
A45: p < p + R by A43,XREAL_1:29,215;
A46: p - R < p by A43,XREAL_1:44,215;
then p - R in {s : s < p};
then p - R in L by XXREAL_1:229;
then consider r1 being Element of REAL such that
A47: r1 in dom (f|X) & r1 in X and
A48: p - R = (f|X).r1 by A3,A4,A5,PARTFUN2:59;
A49: r1 in X /\ dom (f|X) by A47,XBOOLE_0:def 4;
A50: now
assume
A51: x0 < r1;
x0 in X /\ dom (f|X) & r1 in X /\ dom (f|X) by A6,A47,
XBOOLE_0:def 4;
hence contradiction by A8,A42,A46,A48,A51,RFUNCT_2:22;
end;
r1 <> x0 by A42,A43,A48,XREAL_1:44,215;
then r1 < x0 by A50,XXREAL_0:1;
then reconsider N = ].x0 - (x0 - r1),x0 + (x0 - r1).[ as
Neighbourhood of x0 by RCOMP_1:def 6,XREAL_1:50;
take N;
let x be Real such that
A52: x in dom(f|X) and
A53: x in N;
A54: ex s st s = x & x0 - (x0-r1) < s & s < x0 + (x0-r1) by A53;
A55: R < r by A43,XREAL_1:216;
then
A56: p - r < p - R by XREAL_1:15;
(f|X).x in l by A3,A4,A52,FUNCT_1:def 6;
then (f|X).x in {s: s <= p} by XXREAL_1:231;
then ex s st s = (f|X).x & s <= p;
then
A57: (f|X).x <= p + R by A45,XXREAL_0:2;
x in X /\ dom (f|X) by A52,XBOOLE_0:def 4;
then p - R <= (f|X).x by A8,A48,A49,A54,RFUNCT_2:22;
then
A58: (f|X).x in [.p - R, p + R.] by A57;
p < p + r by A43,XREAL_1:29;
then p - R < p + r by A46,XXREAL_0:2;
then
A59: p - R in ].p - r, p + r.[ by A56;
A60: p + R < p + r by A55,XREAL_1:6;
p - r < p by A43,XREAL_1:44;
then p - r < p + R by A45,XXREAL_0:2;
then p + R in ].p - r, p + r.[ by A60;
then [.p - R, p + R.] c= N1 by A44,A59,XXREAL_2:def 12;
hence (f|X).x in N1 by A58;
end;
end;
hence ex N being Neighbourhood of x0 st for r1 be Real st r1
in dom(f|X) & r1 in N holds (f|X).r1 in N1;
end;
suppose
f|X is non-increasing;
then
A61: f|X|X is non-increasing;
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
A62: N2 c= L by RCOMP_1:18;
consider N3 being Neighbourhood of (f|X).x0 such that
A63: N3 c= N1 and
A64: N3 c= N2 by RCOMP_1:17;
consider r be Real such that
A65: r > 0 and
A66: N3 = ].(f|X).x0 - r,(f|X).x0 + r.[ by RCOMP_1:def 6;
reconsider r as Real;
A67: (f|X).x0 + r/2 < (f|X).x0 + r/2 + r/2 by A65,XREAL_1:29,215;
set M2 = (f|X).x0 + r/2;
A68: (f|X).x0 < (f|X).x0 + r/2 by A65,XREAL_1:29,215;
A69: (f|X).x0 < (f|X).x0 + r by A65,XREAL_1:29;
then (f|X).x0 - r < (f|X).x0 + r - r by XREAL_1:9;
then (f|X).x0 - r < (f|X).x0 + r/2 by A68,XXREAL_0:2;
then
A70: M2 in ].(f|X).x0 - r,(f|X).x0 + r.[ by A67;
then M2 in N2 by A64,A66;
then M2 in L by A62;
then consider r2 being Element of REAL such that
A71: r2 in dom (f|X) & r2 in X and
A72: M2 = (f|X).r2 by A3,A4,A5,PARTFUN2:59;
A73: M2 > (f|X).x0 by A65,XREAL_1:29,215;
A74: now
assume
A75: r2 > x0;
x0 in X /\ dom (f|X) & r2 in X /\ dom (f|X) by A6,A71,
XBOOLE_0:def 4;
hence contradiction by A61,A72,A73,A75,RFUNCT_2:23;
end;
set M1 = (f|X).x0 - r/2;
A76: (f|X).x0 - r < (f|X).x0 - r + r/2 by A65,XREAL_1:29,215;
(f|X).x0 - r/2 < (f|X).x0 by A68,XREAL_1:19;
then (f|X).x0 - r/2 < (f|X).x0 + r by A69,XXREAL_0:2;
then
A77: M1 in ].(f|X).x0 - r,(f|X).x0 + r.[ by A76;
then M1 in N2 by A64,A66;
then M1 in L by A62;
then consider r1 being Element of REAL such that
A78: r1 in dom (f|X) & r1 in X and
A79: M1 = (f|X).r1 by A3,A4,A5,PARTFUN2:59;
A80: (f|X).x0 < (f|X).x0 + r/2 by A65,XREAL_1:29,215;
then
A81: M1 < (f|X).x0 by XREAL_1:19;
A82: now
assume
A83: x0 > r1;
x0 in X /\ dom (f|X) & r1 in X /\ dom(f|X) by A6,A78,
XBOOLE_0:def 4;
hence contradiction by A61,A79,A81,A83,RFUNCT_2:23;
end;
x0 <> r2 by A65,A72,XREAL_1:29,215;
then x0 > r2 by A74,XXREAL_0:1;
then
A84: x0 - r2 > 0 by XREAL_1:50;
set R = min(r1 - x0,x0 - r2);
A85: R <= r1 - x0 by XXREAL_0:17;
r1 <> x0 by A79,A80,XREAL_1:19;
then r1 > x0 by A82,XXREAL_0:1;
then r1 - x0 > 0 by XREAL_1:50;
then R > 0 by A84,XXREAL_0:15;
then reconsider N =].x0 - R,x0 + R.[ as Neighbourhood of x0 by
RCOMP_1:def 6;
take N;
let x be Real;
assume that
A86: x in dom (f|X) and
A87: x in N;
A88: x in X /\ dom(f|X) by A86,XBOOLE_1:28;
A89: ex s st s = x & x0 - R < s & s < x0 + R by A87;
then x0 < R + x by XREAL_1:19;
then
A90: x0 - x < R + x - x by XREAL_1:9;
x - x0 < R by A89,XREAL_1:19;
then x - x0 < r1-x0 by A85,XXREAL_0:2;
then
A91: x - x0 + x0 < r1 - x0 + x0 by XREAL_1:6;
r1 in X /\ dom(f|X) by A78,XBOOLE_0:def 4;
then
A92: (f|X).r1 <= (f|X).x by A61,A91,A88,RFUNCT_2:23;
R <= x0 - r2 by XXREAL_0:17;
then x0 - x < x0 - r2 by A90,XXREAL_0:2;
then -(x0 - x) > -(x0 - r2) by XREAL_1:24;
then
A93: x - x0 + x0 > r2 - x0 + x0 by XREAL_1:6;
r2 in X /\ dom(f|X) by A71,XBOOLE_0:def 4;
then (f|X).x <= (f|X).r2 by A61,A93,A88,RFUNCT_2:23;
then
A94: (f|X).x in [.M1,M2.] by A79,A72,A92;
[.M1,M2.] c= ].(f|X).x0 - r,(f|X).x0 + r.[ by A77,A70,
XXREAL_2:def 12;
then (f|X).x in N3 by A66,A94;
hence (f|X).x in N1 by A63;
end;
suppose
A95: (f|X).x0 = p;
then consider r be Real such that
A96: r > 0 and
A97: N1 = ].p - r,p + r.[ by RCOMP_1:def 6;
reconsider r as Real;
set R = r/2;
A98: p < p + R by A96,XREAL_1:29,215;
A99: p - R < p by A96,XREAL_1:44,215;
then p - R in {s : s < p};
then p - R in L by XXREAL_1:229;
then consider r1 being Element of REAL such that
A100: r1 in dom (f|X) & r1 in X and
A101: p - R = (f|X).r1 by A3,A4,A5,PARTFUN2:59;
A102: r1 in X /\ dom (f|X) by A100,XBOOLE_0:def 4;
A103: now
assume
A104: x0 > r1;
x0 in X /\ dom (f|X) & r1 in X /\ dom (f|X) by A6,A100,
XBOOLE_0:def 4;
hence contradiction by A61,A95,A99,A101,A104,RFUNCT_2:23;
end;
r1 <> x0 by A95,A96,A101,XREAL_1:44,215;
then r1 > x0 by A103,XXREAL_0:1;
then reconsider N = ].x0 - (r1 - x0),x0 + (r1 - x0).[ as
Neighbourhood of x0 by RCOMP_1:def 6,XREAL_1:50;
take N;
let x be Real such that
A105: x in dom(f|X) and
A106: x in N;
A107: ex s st s = x & x0 - (r1-x0) < s & s < x0 + (r1-x0) by A106;
A108: R < r by A96,XREAL_1:216;
then
A109: p - r < p - R by XREAL_1:15;
(f|X).x in l by A3,A4,A105,FUNCT_1:def 6;
then (f|X).x in {s: s <= p} by XXREAL_1:231;
then ex s st s = (f|X).x & s <= p;
then
A110: (f|X).x <= p + R by A98,XXREAL_0:2;
x in X /\ dom (f|X) by A105,XBOOLE_0:def 4;
then p - R <= (f|X).x by A61,A101,A102,A107,RFUNCT_2:23;
then
A111: (f|X).x in [.p - R, p + R.] by A110;
p < p + r by A96,XREAL_1:29;
then p - R < p + r by A99,XXREAL_0:2;
then
A112: p - R in ].p - r, p + r.[ by A109;
A113: p + R < p + r by A108,XREAL_1:6;
p - r < p by A96,XREAL_1:44;
then p - r < p + R by A98,XXREAL_0:2;
then p + R in ].p - r, p + r.[ by A113;
then [.p - R, p + R.] c= N1 by A97,A112,XXREAL_2:def 12;
hence (f|X).x in N1 by A111;
end;
end;
hence ex N being Neighbourhood of x0 st for r1 be Real st r1
in dom(f|X) & r1 in N holds (f|X).r1 in N1;
end;
end;
hence ex N being Neighbourhood of x0 st for r1 be Real st r1 in
dom(f|X) & r1 in N holds (f|X).r1 in N1;
end;
hence thesis by FCONT_1:4;
end;
hence thesis by FCONT_1:def 2;
end;
theorem Th14:
X c= dom f & f|X is monotone & (ex p st f.:X =
right_closed_halfline(p)) implies f|X is continuous
proof
assume that
A1: X c= dom f and
A2: f|X is monotone;
given p such that
A3: f.:X = right_closed_halfline(p);
set L = right_open_halfline(p);
set l = right_closed_halfline(p);
for x0 be Real st x0 in dom(f|X) holds f|X is_continuous_in x0
proof
let x0 be Real;
A4: (f|X).:X = f.:X by RELAT_1:129;
A5: L c= l by XXREAL_1:22;
assume x0 in dom(f|X);
then
x0 in X;
then x0 in dom f /\ X by A1,XBOOLE_0:def 4;
then
A6: x0 in dom (f|X) by RELAT_1:61;
then (f|X).x0 in (f|X).:X by FUNCT_1:def 6;
then (f|X).x0 in {p} \/ L by A3,A4,XXREAL_1:427;
then
A7: (f|X).x0 in {p} or (f|X).x0 in L by XBOOLE_0:def 3;
now
let N1 be Neighbourhood of (f|X).x0;
now
per cases by A2,RFUNCT_2:def 5;
suppose
f|X is non-decreasing;
then
A8: f|X|X is non-decreasing;
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
A9: N2 c= L by RCOMP_1:18;
consider N3 being Neighbourhood of (f|X).x0 such that
A10: N3 c= N1 and
A11: N3 c= N2 by RCOMP_1:17;
consider r be Real such that
A12: r>0 and
A13: N3 = ].(f|X).x0 - r,(f|X).x0 + r.[ by RCOMP_1:def 6;
reconsider r as Real;
A14: (f|X).x0 + r/2 < (f|X).x0 + r/2 + r/2 by A12,XREAL_1:29,215;
set M2 = (f|X).x0 + r/2;
A15: (f|X).x0 < (f|X).x0 + r/2 by A12,XREAL_1:29,215;
A16: (f|X).x0 < (f|X).x0 + r by A12,XREAL_1:29;
then (f|X).x0 - r < (f|X).x0 + r - r by XREAL_1:9;
then (f|X).x0 - r < (f|X).x0 + r/2 by A15,XXREAL_0:2;
then
A17: M2 in ].(f|X).x0 - r,(f|X).x0 + r.[ by A14;
then M2 in N2 by A11,A13;
then M2 in L by A9;
then consider r2 being Element of REAL such that
A18: r2 in dom (f|X) & r2 in X and
A19: M2 = (f|X).r2 by A3,A4,A5,PARTFUN2:59;
A20: M2 > (f|X).x0 by A12,XREAL_1:29,215;
A21: now
assume
A22: r2 < x0;
x0 in X /\ dom(f|X) & r2 in X /\ dom (f|X)
by A6,A18,XBOOLE_0:def 4;
hence contradiction by A8,A19,A20,A22,RFUNCT_2:22;
end;
set M1 = (f|X).x0 - r/2;
A23: (f|X).x0 - r < (f|X).x0 - r + r/2 by A12,XREAL_1:29,215;
(f|X).x0 - r/2 < (f|X).x0 by A15,XREAL_1:19;
then (f|X).x0 - r/2 < (f|X).x0 + r by A16,XXREAL_0:2;
then
A24: M1 in ].(f|X).x0 - r,(f|X).x0 + r.[ by A23;
then M1 in N2 by A11,A13;
then M1 in L by A9;
then consider r1 being Element of REAL such that
A25: r1 in dom (f|X) & r1 in X and
A26: M1 = (f|X).r1 by A3,A4,A5,PARTFUN2:59;
A27: (f|X).x0 < (f|X).x0 + r/2 by A12,XREAL_1:29,215;
then
A28: M1 < (f|X).x0 by XREAL_1:19;
A29: now
assume
A30: x0 < r1;
x0 in X /\ dom( f|X) & r1 in X /\ dom(f|X)
by A6,A25,XBOOLE_0:def 4;
hence contradiction by A8,A26,A28,A30,RFUNCT_2:22;
end;
x0 <> r2 by A12,A19,XREAL_1:29,215;
then x0 < r2 by A21,XXREAL_0:1;
then
A31: r2 - x0 > 0 by XREAL_1:50;
set R = min(x0 - r1,r2 - x0);
A32: R <= r2 - x0 by XXREAL_0:17;
r1 <> x0 by A26,A27,XREAL_1:19;
then r1 < x0 by A29,XXREAL_0:1;
then x0 - r1 > 0 by XREAL_1:50;
then R > 0 by A31,XXREAL_0:15;
then reconsider N = ].x0 - R,x0+ R.[ as Neighbourhood of x0 by
RCOMP_1:def 6;
take N;
let x be Real;
assume that
A33: x in dom (f|X) and
A34: x in N;
A35: x in X /\ dom (f|X) by A33,XBOOLE_1:28;
A36: ex s st s = x & x0 - R < s & s < x0 + R by A34;
then x0 < R + x by XREAL_1:19;
then
A37: x0 - x < R + x - x by XREAL_1:9;
R <= x0 - r1 by XXREAL_0:17;
then x0 - x < x0 - r1 by A37,XXREAL_0:2;
then -(x0 - x) > -(x0 - r1) by XREAL_1:24;
then
A38: x - x0 + x0 > r1 - x0 + x0 by XREAL_1:6;
r1 in X /\ dom (f|X) by A25,XBOOLE_0:def 4;
then
A39: (f|X).r1 <= (f|X).x by A8,A38,A35,RFUNCT_2:22;
x - x0 < R by A36,XREAL_1:19;
then x - x0 < r2 - x0 by A32,XXREAL_0:2;
then
A40: x - x0 + x0 < r2 - x0 + x0 by XREAL_1:6;
r2 in X /\ dom (f|X) by A18,XBOOLE_0:def 4;
then (f|X).x <= (f|X).r2 by A8,A40,A35,RFUNCT_2:22;
then
A41: (f|X).x in [.M1,M2.] by A26,A19,A39;
[.M1,M2.] c= ].(f|X).x0 - r,(f|X).x0 + r.[ by A24,A17,
XXREAL_2:def 12;
then (f|X).x in N3 by A13,A41;
hence (f|X).x in N1 by A10;
end;
suppose
A42: (f|X).x0 = p;
then consider r be Real such that
A43: r > 0 and
A44: N1 = ].p - r,p + r.[ by RCOMP_1:def 6;
reconsider r as Real;
set R = r/2;
A45: p - R < p by A43,XREAL_1:44,215;
A46: p < p + R by A43,XREAL_1:29,215;
then p + R in {s : p < s};
then p + R in L by XXREAL_1:230;
then consider r1 being Element of REAL such that
A47: r1 in dom (f|X) & r1 in X and
A48: p + R = (f|X).r1 by A3,A4,A5,PARTFUN2:59;
A49: now
assume
A50: x0 > r1;
x0 in X /\ dom (f|X) &
r1 in X /\ dom (f|X) by A6,A47,XBOOLE_0:def 4;
hence contradiction by A8,A42,A46,A48,A50,RFUNCT_2:22;
end;
r1 <> x0 by A42,A43,A48,XREAL_1:29,215;
then r1 > x0 by A49,XXREAL_0:1;
then reconsider N = ].x0 - (r1 - x0),x0 + (r1 - x0).[ as
Neighbourhood of x0 by RCOMP_1:def 6,XREAL_1:50;
take N;
let x be Real such that
A51: x in dom(f|X) and
A52: x in N;
A53: ex s st s = x & x0 - (r1-x0) < s & s < x0 + (r1-x0) by A52;
(f|X).x in l by A3,A4,A51,FUNCT_1:def 6;
then (f|X).x in {s: p <= s} by XXREAL_1:232;
then ex s st s = (f|X).x & p <= s;
then
A54: p - R <= (f|X).x by A45,XXREAL_0:2;
A55: r1 in X /\ dom (f|X) by A47,XBOOLE_0:def 4;
x in X /\ dom (f|X) by A51,XBOOLE_0:def 4;
then p + R >= (f|X).x by A8,A48,A55,A53,RFUNCT_2:22;
then
A56: (f|X).x in [.p - R, p + R.] by A54;
A57: R < r by A43,XREAL_1:216;
then
A58: p - r < p - R by XREAL_1:15;
p < p + r by A43,XREAL_1:29;
then p - R < p + r by A45,XXREAL_0:2;
then
A59: p - R in ].p - r, p + r.[ by A58;
A60: p + R < p + r by A57,XREAL_1:6;
p - r < p by A43,XREAL_1:44;
then p - r < p + R by A46,XXREAL_0:2;
then p + R in ].p - r, p + r.[ by A60;
then [.p - R, p + R.] c= N1 by A44,A59,XXREAL_2:def 12;
hence (f|X).x in N1 by A56;
end;
end;
hence ex N being Neighbourhood of x0 st for r1 be Real st r1
in dom(f|X) & r1 in N holds (f|X).r1 in N1;
end;
suppose
f|X is non-increasing;
then
A61: f|X|X is non-increasing;
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
A62: N2 c= L by RCOMP_1:18;
consider N3 being Neighbourhood of (f|X).x0 such that
A63: N3 c= N1 and
A64: N3 c= N2 by RCOMP_1:17;
consider r be Real such that
A65: r > 0 and
A66: N3 = ].(f|X).x0 - r,(f|X).x0 + r.[ by RCOMP_1:def 6;
reconsider r as Real;
A67: (f|X).x0 + r/2 < (f|X).x0 + r/2 + r/2 by A65,XREAL_1:29,215;
set M2 = (f|X).x0 + r/2;
A68: (f|X).x0 < (f|X).x0 + r/2 by A65,XREAL_1:29,215;
A69: (f|X).x0 < (f|X).x0 + r by A65,XREAL_1:29;
then (f|X).x0 - r < (f|X).x0 + r - r by XREAL_1:9;
then (f|X).x0 - r < (f|X).x0 + r/2 by A68,XXREAL_0:2;
then
A70: M2 in ].(f|X).x0 - r,(f|X).x0 + r.[ by A67;
then M2 in N2 by A64,A66;
then M2 in L by A62;
then consider r2 being Element of REAL such that
A71: r2 in dom (f|X) & r2 in X and
A72: M2 = (f|X).r2 by A3,A4,A5,PARTFUN2:59;
A73: M2 > (f|X).x0 by A65,XREAL_1:29,215;
A74: now
assume
A75: r2 > x0;
x0 in X /\ dom (f|X) & r2 in X /\ dom (f|X)
by A6,A71,XBOOLE_0:def 4;
hence contradiction by A61,A72,A73,A75,RFUNCT_2:23;
end;
set M1 = (f|X).x0 - r/2;
A76: (f|X).x0 - r < (f|X).x0 - r + r/2 by A65,XREAL_1:29,215;
(f|X).x0 - r/2 < (f|X).x0 by A68,XREAL_1:19;
then (f|X).x0 - r/2 < (f|X).x0 + r by A69,XXREAL_0:2;
then
A77: M1 in ].(f|X).x0 - r,(f|X).x0 + r.[ by A76;
then M1 in N2 by A64,A66;
then M1 in L by A62;
then consider r1 being Element of REAL such that
A78: r1 in dom (f|X) & r1 in X and
A79: M1 = (f|X).r1 by A3,A4,A5,PARTFUN2:59;
A80: (f|X).x0 < (f|X).x0 + r/2 by A65,XREAL_1:29,215;
then
A81: M1 < (f|X).x0 by XREAL_1:19;
A82: now
assume
A83: x0 > r1;
x0 in X /\ dom (f|X) & r1 in X /\ dom(f|X)
by A6,A78,XBOOLE_0:def 4;
hence contradiction by A61,A79,A81,A83,RFUNCT_2:23;
end;
x0 <> r2 by A65,A72,XREAL_1:29,215;
then x0 > r2 by A74,XXREAL_0:1;
then
A84: x0 - r2 > 0 by XREAL_1:50;
set R = min(r1 - x0,x0 - r2);
A85: R <= r1 - x0 by XXREAL_0:17;
r1 <> x0 by A79,A80,XREAL_1:19;
then r1 > x0 by A82,XXREAL_0:1;
then r1 - x0 > 0 by XREAL_1:50;
then R > 0 by A84,XXREAL_0:15;
then reconsider N =].x0 - R,x0 + R.[ as Neighbourhood of x0 by
RCOMP_1:def 6;
take N;
let x be Real;
assume that
A86: x in dom (f|X) and
A87: x in N;
A88: x in X /\ dom(f|X) by A86,XBOOLE_1:28;
A89: ex s st s = x & x0 - R < s & s < x0 + R by A87;
then x0 < R + x by XREAL_1:19;
then
A90: x0 - x < R + x - x by XREAL_1:9;
x - x0 < R by A89,XREAL_1:19;
then x - x0 < r1-x0 by A85,XXREAL_0:2;
then
A91: x - x0 + x0 < r1 - x0 + x0 by XREAL_1:6;
r1 in X /\ dom(f|X) by A78,XBOOLE_0:def 4;
then
A92: (f|X).r1 <= (f|X).x by A61,A91,A88,RFUNCT_2:23;
R <= x0 - r2 by XXREAL_0:17;
then x0 - x < x0 - r2 by A90,XXREAL_0:2;
then -(x0 - x) > -(x0 - r2) by XREAL_1:24;
then
A93: x - x0 + x0 > r2 - x0 + x0 by XREAL_1:6;
r2 in X /\ dom(f|X) by A71,XBOOLE_0:def 4;
then (f|X).x <= (f|X).r2 by A61,A93,A88,RFUNCT_2:23;
then
A94: (f|X).x in [.M1,M2.] by A79,A72,A92;
[.M1,M2.] c= ].(f|X).x0 - r,(f|X).x0 + r.[ by A77,A70,
XXREAL_2:def 12;
then (f|X).x in N3 by A66,A94;
hence (f|X).x in N1 by A63;
end;
suppose
A95: (f|X).x0 = p;
then consider r be Real such that
A96: r > 0 and
A97: N1 = ].p - r,p + r.[ by RCOMP_1:def 6;
reconsider r as Real;
set R = r/2;
A98: p - R < p by A96,XREAL_1:44,215;
A99: p < p + R by A96,XREAL_1:29,215;
then p + R in {s : p < s};
then p + R in L by XXREAL_1:230;
then consider r1 being Element of REAL such that
A100: r1 in dom (f|X) & r1 in X and
A101: p + R = (f|X).r1 by A3,A4,A5,PARTFUN2:59;
A102: now
assume
A103: x0 < r1;
x0 in X /\ dom (f|X) & r1 in X /\ dom (f|X)
by A6,A100,XBOOLE_0:def 4;
hence contradiction by A61,A95,A99,A101,A103,RFUNCT_2:23;
end;
r1 <> x0 by A95,A96,A101,XREAL_1:29,215;
then r1 < x0 by A102,XXREAL_0:1;
then reconsider N = ].x0 - (x0 - r1),x0 + (x0 - r1).[ as
Neighbourhood of x0 by RCOMP_1:def 6,XREAL_1:50;
take N;
let x be Real such that
A104: x in dom(f|X) and
A105: x in N;
A106: ex s st s = x & x0 - (x0-r1) < s & s < x0 + (x0-r1) by A105;
(f|X).x in l by A3,A4,A104,FUNCT_1:def 6;
then (f|X).x in {s: p <= s} by XXREAL_1:232;
then ex s st s = (f|X).x & p <= s;
then
A107: p - R <= (f|X).x by A98,XXREAL_0:2;
A108: r1 in X /\ dom (f|X) by A100,XBOOLE_0:def 4;
x in X /\ dom (f|X) by A104,XBOOLE_0:def 4;
then p + R >= (f|X).x by A61,A101,A108,A106,RFUNCT_2:23;
then
A109: (f|X).x in [.p - R, p + R.] by A107;
A110: R < r by A96,XREAL_1:216;
then
A111: p - r < p - R by XREAL_1:15;
p < p + r by A96,XREAL_1:29;
then p - R < p + r by A98,XXREAL_0:2;
then
A112: p - R in ].p - r, p + r.[ by A111;
A113: p + R < p + r by A110,XREAL_1:6;
p - r < p by A96,XREAL_1:44;
then p - r < p + R by A99,XXREAL_0:2;
then p + R in ].p - r, p + r.[ by A113;
then [.p - R, p + R.] c= N1 by A97,A112,XXREAL_2:def 12;
hence (f|X).x in N1 by A109;
end;
end;
hence ex N being Neighbourhood of x0 st for r1 be Real st r1
in dom(f|X) & r1 in N holds (f|X).r1 in N1;
end;
end;
hence ex N being Neighbourhood of x0 st for r1 be Real st r1 in
dom(f|X) & r1 in N holds (f|X).r1 in N1;
end;
hence thesis by FCONT_1:4;
end;
hence thesis by FCONT_1:def 2;
end;
theorem Th15:
X c= dom f & f|X is monotone & (ex p,g st f.:X = ].p,g.[)
implies f|X is continuous
proof
assume that
A1: X c= dom f and
A2: f|X is monotone;
given p,g such that
A3: f.:X = ].p,g.[;
set L = ].p,g.[;
now
per cases by A2,RFUNCT_2:def 5;
suppose
f|X is non-decreasing;
then
A4: f|X|X is non-decreasing;
for x0 be Real st x0 in dom(f|X) holds f|X is_continuous_in x0
proof
let x0 be Real;
A5: (f|X).:X = f.:X by RELAT_1:129;
assume x0 in dom(f|X);
then
x0 in X;
then x0 in dom f /\ X by A1,XBOOLE_0:def 4;
then
A6: x0 in dom (f|X) by RELAT_1:61;
then (f|X).x0 in (f|X).:X by FUNCT_1:def 6;
then
A7: (f|X).x0 in L by A3,RELAT_1:129;
now
let N1 be Neighbourhood of (f|X).x0;
consider N2 being Neighbourhood of (f|X).x0 such that
A8: N2 c= L by A7,RCOMP_1:18;
consider N3 being Neighbourhood of (f|X).x0 such that
A9: N3 c= N1 and
A10: N3 c= N2 by RCOMP_1:17;
consider r be Real such that
A11: r>0 and
A12: N3 = ].(f|X).x0 - r,(f|X).x0 + r.[ by RCOMP_1:def 6;
reconsider r as Real;
A13: (f|X).x0 + r/2 < (f|X).x0 + r/2 + r/2 by A11,XREAL_1:29,215;
set M2 = (f|X).x0 + r/2;
A14: (f|X).x0 < (f|X).x0 + r/2 by A11,XREAL_1:29,215;
A15: (f|X).x0 < (f|X).x0 + r by A11,XREAL_1:29;
then (f|X).x0 - r < (f|X).x0 + r - r by XREAL_1:9;
then (f|X).x0 - r < (f|X).x0 + r/2 by A14,XXREAL_0:2;
then
A16: M2 in ].(f|X).x0 - r,(f|X).x0 + r.[ by A13;
then M2 in N2 by A10,A12;
then consider r2 being Element of REAL such that
A17: r2 in dom (f|X) & r2 in X and
A18: M2 = (f|X).r2 by A3,A5,A8,PARTFUN2:59;
A19: M2 > (f|X).x0 by A11,XREAL_1:29,215;
A20: now
assume
A21: r2 < x0;
x0 in X /\ dom(f|X) & r2 in X /\ dom (f|X) by A6,A17,XBOOLE_0:def 4
;
hence contradiction by A4,A18,A19,A21,RFUNCT_2:22;
end;
set M1 = (f|X).x0 - r/2;
A22: (f|X).x0 - r < (f|X).x0 - r + r/2 by A11,XREAL_1:29,215;
(f|X).x0 - r/2 < (f|X).x0 by A14,XREAL_1:19;
then (f|X).x0 - r/2 < (f|X).x0 + r by A15,XXREAL_0:2;
then
A23: M1 in ].(f|X).x0 - r,(f|X).x0 + r.[ by A22;
then M1 in N2 by A10,A12;
then consider r1 being Element of REAL such that
A24: r1 in dom (f|X) & r1 in X and
A25: M1 = (f|X).r1 by A3,A5,A8,PARTFUN2:59;
A26: (f|X).x0 < (f|X).x0 + r/2 by A11,XREAL_1:29,215;
then
A27: M1 < (f|X).x0 by XREAL_1:19;
A28: now
assume
A29: x0 < r1;
x0 in X /\ dom( f|X) & r1 in X /\ dom(f|X) by A6,A24,XBOOLE_0:def 4
;
hence contradiction by A4,A25,A27,A29,RFUNCT_2:22;
end;
x0 <> r2 by A11,A18,XREAL_1:29,215;
then x0 < r2 by A20,XXREAL_0:1;
then
A30: r2 - x0 > 0 by XREAL_1:50;
set R = min(x0 - r1,r2 - x0);
A31: R <= r2 - x0 by XXREAL_0:17;
r1 <> x0 by A25,A26,XREAL_1:19;
then r1 < x0 by A28,XXREAL_0:1;
then x0 - r1 > 0 by XREAL_1:50;
then R > 0 by A30,XXREAL_0:15;
then reconsider N = ].x0 - R,x0 + R.[ as Neighbourhood of x0 by
RCOMP_1:def 6;
take N;
let x be Real;
assume that
A32: x in dom (f|X) and
A33: x in N;
A34: x in X /\ dom (f|X) by A32,XBOOLE_1:28;
A35: ex s st s = x & x0 - R < s & s < x0 + R by A33;
then x0 < R + x by XREAL_1:19;
then
A36: x0 - x < R + x - x by XREAL_1:9;
R <= x0 - r1 by XXREAL_0:17;
then x0 - x < x0 - r1 by A36,XXREAL_0:2;
then -(x0 - x) > -(x0 - r1) by XREAL_1:24;
then
A37: x - x0 + x0 > r1 - x0 + x0 by XREAL_1:6;
r1 in X /\ dom (f|X) by A24,XBOOLE_0:def 4;
then
A38: (f|X).r1 <= (f|X).x by A4,A37,A34,RFUNCT_2:22;
x - x0 < R by A35,XREAL_1:19;
then x - x0 < r2 - x0 by A31,XXREAL_0:2;
then
A39: x - x0 + x0 < r2 - x0 + x0 by XREAL_1:6;
r2 in X /\ dom (f|X) by A17,XBOOLE_0:def 4;
then (f|X).x <= (f|X).r2 by A4,A39,A34,RFUNCT_2:22;
then
A40: (f|X).x in [.M1,M2.] by A25,A18,A38;
[.M1,M2.] c= ].(f|X).x0 - r,(f|X).x0 + r.[ by A23,A16,XXREAL_2:def 12
;
then (f|X).x in N3 by A12,A40;
hence (f|X).x in N1 by A9;
end;
hence thesis by FCONT_1:4;
end;
hence thesis by FCONT_1:def 2;
end;
suppose
f|X is non-increasing;
then
A41: f|X|X is non-increasing;
for x0 be Real st x0 in dom(f|X) holds f|X is_continuous_in x0
proof
let x0 be Real;
A42: (f|X).:X = f.:X by RELAT_1:129;
assume x0 in dom(f|X);
then
x0 in X;
then x0 in dom f /\ X by A1,XBOOLE_0:def 4;
then
A43: x0 in dom(f|X) by RELAT_1:61;
then (f|X).x0 in (f|X).:X by FUNCT_1:def 6;
then
A44: (f|X).x0 in L by A3,RELAT_1:129;
now
let N1 be Neighbourhood of (f|X).x0;
consider N2 being Neighbourhood of (f|X).x0 such that
A45: N2 c= L by A44,RCOMP_1:18;
consider N3 being Neighbourhood of (f|X).x0 such that
A46: N3 c= N1 and
A47: N3 c= N2 by RCOMP_1:17;
consider r be Real such that
A48: r > 0 and
A49: N3 = ].(f|X).x0 - r,(f|X).x0 + r.[ by RCOMP_1:def 6;
reconsider r as Real;
A50: (f|X).x0 + r/2 < (f|X).x0 + r/2 + r/2 by A48,XREAL_1:29,215;
set M2 = (f|X).x0 + r/2;
A51: (f|X).x0 < (f|X).x0 + r/2 by A48,XREAL_1:29,215;
A52: (f|X).x0 < (f|X).x0 + r by A48,XREAL_1:29;
then (f|X).x0 - r < (f|X).x0 + r - r by XREAL_1:9;
then (f|X).x0 - r < (f|X).x0 + r/2 by A51,XXREAL_0:2;
then
A53: M2 in ].(f|X).x0 - r,(f|X).x0 + r.[ by A50;
then M2 in N2 by A47,A49;
then consider r2 being Element of REAL such that
A54: r2 in dom (f|X) & r2 in X and
A55: M2 = (f|X).r2 by A3,A42,A45,PARTFUN2:59;
A56: M2 > (f|X).x0 by A48,XREAL_1:29,215;
A57: now
assume
A58: r2 > x0;
x0 in X /\ dom (f|X) & r2 in X /\ dom (f|X) by A43,A54,
XBOOLE_0:def 4;
hence contradiction by A41,A55,A56,A58,RFUNCT_2:23;
end;
set M1 = (f|X).x0 - r/2;
A59: (f|X).x0 - r < (f|X).x0 - r + r/2 by A48,XREAL_1:29,215;
(f|X).x0 - r/2 < (f|X).x0 by A51,XREAL_1:19;
then (f|X).x0 - r/2 < (f|X).x0 + r by A52,XXREAL_0:2;
then
A60: M1 in ].(f|X).x0 - r,(f|X).x0 + r.[ by A59;
then M1 in N2 by A47,A49;
then consider r1 being Element of REAL such that
A61: r1 in dom (f|X) & r1 in X and
A62: M1 = (f|X).r1 by A3,A42,A45,PARTFUN2:59;
A63: (f|X).x0 < (f|X).x0 + r/2 by A48,XREAL_1:29,215;
then
A64: M1 < (f|X).x0 by XREAL_1:19;
A65: now
assume
A66: x0 > r1;
x0 in X /\ dom (f|X) & r1 in X /\ dom(f|X) by A43,A61,
XBOOLE_0:def 4;
hence contradiction by A41,A62,A64,A66,RFUNCT_2:23;
end;
x0 <> r2 by A48,A55,XREAL_1:29,215;
then x0 > r2 by A57,XXREAL_0:1;
then
A67: x0 - r2 > 0 by XREAL_1:50;
set R = min(r1 - x0,x0 - r2);
A68: R <= r1 - x0 by XXREAL_0:17;
r1 <> x0 by A62,A63,XREAL_1:19;
then r1 > x0 by A65,XXREAL_0:1;
then r1 - x0 > 0 by XREAL_1:50;
then R > 0 by A67,XXREAL_0:15;
then reconsider N = ].x0 - R,x0 + R.[ as Neighbourhood of x0 by
RCOMP_1:def 6;
take N;
let x be Real;
assume that
A69: x in dom (f|X) and
A70: x in N;
A71: x in X /\ dom(f|X) by A69,XBOOLE_1:28;
A72: ex s st s = x & x0 - R < s & s < x0 + R by A70;
then x0 < R + x by XREAL_1:19;
then
A73: x0 - x < R + x - x by XREAL_1:9;
x - x0 < R by A72,XREAL_1:19;
then x - x0 < r1-x0 by A68,XXREAL_0:2;
then
A74: x - x0 + x0 < r1 - x0 + x0 by XREAL_1:6;
r1 in X /\ dom(f|X) by A61,XBOOLE_0:def 4;
then
A75: (f|X).r1 <= (f|X).x by A41,A74,A71,RFUNCT_2:23;
R <= x0 - r2 by XXREAL_0:17;
then x0 - x < x0 - r2 by A73,XXREAL_0:2;
then -(x0 - x) > -(x0 - r2) by XREAL_1:24;
then
A76: x - x0 + x0 > r2 - x0 + x0 by XREAL_1:6;
r2 in X /\ dom(f|X) by A54,XBOOLE_0:def 4;
then (f|X).x <= (f|X).r2 by A41,A76,A71,RFUNCT_2:23;
then
A77: (f|X).x in [.M1,M2.] by A62,A55,A75;
[.M1,M2.] c= ].(f|X).x0 - r,(f|X).x0 + r.[ by A60,A53,XXREAL_2:def 12
;
then (f|X).x in N3 by A49,A77;
hence (f|X).x in N1 by A46;
end;
hence thesis by FCONT_1:4;
end;
hence thesis by FCONT_1:def 2;
end;
end;
hence thesis;
end;
theorem Th16:
X c= dom f & f|X is monotone & f.:X = REAL implies f|X is continuous
proof
assume that
A1: X c= dom f and
A2: f|X is monotone and
A3: f.:X = REAL;
now
per cases by A2,RFUNCT_2:def 5;
suppose
f|X is non-decreasing;
then
A4: f|X|X is non-decreasing;
for x0 be Real st x0 in dom(f|X) holds f|X is_continuous_in x0
proof
let x0 be Real;
A5: (f|X).:X = f.:X by RELAT_1:129;
assume x0 in dom(f|X);
then
x0 in X;
then x0 in dom f /\ X by A1,XBOOLE_0:def 4;
then
A6: x0 in dom (f|X) by RELAT_1:61;
now
let N1 be Neighbourhood of (f|X).x0;
consider r be Real such that
A7: r>0 and
A8: N1 = ].(f|X).x0 - r,(f|X).x0 + r.[ by RCOMP_1:def 6;
reconsider r as Real;
A9: (f|X).x0 < (f|X).x0 + r/2 by A7,XREAL_1:29,215;
reconsider M1 = (f|X).x0 - r/2 as Element of REAL by XREAL_0:def 1;
consider r1 being Element of REAL such that
A10: r1 in dom (f|X) & r1 in X and
A11: M1 = (f|X).r1 by A3,A5,PARTFUN2:59;
A12: (f|X).x0 < (f|X).x0 + r/2 by A7,XREAL_1:29,215;
then
A13: M1 < (f|X).x0 by XREAL_1:19;
A14: now
assume
A15: x0 < r1;
x0 in X /\ dom (f|X) & r1 in X /\ dom(f|X) by A6,A10,XBOOLE_0:def 4
;
hence contradiction by A4,A11,A13,A15,RFUNCT_2:22;
end;
reconsider M2 = (f|X).x0 + r/2 as Element of REAL by XREAL_0:def 1;
consider r2 being Element of REAL such that
A16: r2 in dom (f|X) & r2 in X and
A17: M2 = (f|X).r2 by A3,A5,PARTFUN2:59;
A18: M2 > (f|X).x0 by A7,XREAL_1:29,215;
A19: now
assume
A20: r2 < x0;
x0 in X /\ dom(f|X) & r2 in X /\ dom (f|X) by A6,A16,XBOOLE_0:def 4
;
hence contradiction by A4,A17,A18,A20,RFUNCT_2:22;
end;
x0 <> r2 by A7,A17,XREAL_1:29,215;
then x0 < r2 by A19,XXREAL_0:1;
then
A21: r2 - x0 > 0 by XREAL_1:50;
set R = min(x0 - r1,r2 - x0);
A22: R <= r2 - x0 by XXREAL_0:17;
r1 <> x0 by A11,A12,XREAL_1:19;
then r1 < x0 by A14,XXREAL_0:1;
then x0 - r1 > 0 by XREAL_1:50;
then R > 0 by A21,XXREAL_0:15;
then reconsider N = ].x0 - R,x0 + R.[ as Neighbourhood of x0 by
RCOMP_1:def 6;
take N;
let x be Real;
assume that
A23: x in dom (f|X) and
A24: x in N;
A25: x in X /\ dom (f|X) by A23,XBOOLE_1:28;
A26: (f|X).x0 + r/2 < (f|X).x0 + r/2 + r/2 by A7,XREAL_1:29,215;
A27: (f|X).x0 < (f|X).x0 + r by A7,XREAL_1:29;
then (f|X).x0 - r < (f|X).x0 + r - r by XREAL_1:9;
then (f|X).x0 - r < (f|X).x0 + r/2 by A9,XXREAL_0:2;
then
A28: M2 in ].(f|X).x0 - r,(f|X).x0 + r.[ by A26;
A29: (f|X).x0 - r < (f|X).x0 - r + r/2 by A7,XREAL_1:29,215;
(f|X).x0 - r/2 < (f|X).x0 by A9,XREAL_1:19;
then (f|X).x0 - r/2 < (f|X).x0 + r by A27,XXREAL_0:2;
then M1 in ].(f|X).x0 - r,(f|X).x0 + r.[ by A29;
then
A30: [.M1,M2.] c= ].(f|X).x0 - r,(f|X).x0 + r.[ by A28,XXREAL_2:def 12;
A31: ex s st s = x & x0 - R < s & s < x0 + R by A24;
then x0 < R + x by XREAL_1:19;
then
A32: x0 - x < R + x - x by XREAL_1:9;
R <= x0 - r1 by XXREAL_0:17;
then x0 - x < x0 - r1 by A32,XXREAL_0:2;
then -(x0 - x) > -(x0 - r1) by XREAL_1:24;
then
A33: x - x0 + x0 > r1 - x0 + x0 by XREAL_1:6;
r1 in X /\ dom (f|X) by A10,XBOOLE_0:def 4;
then
A34: (f|X).r1 <= (f|X).x by A4,A33,A25,RFUNCT_2:22;
x - x0 < R by A31,XREAL_1:19;
then x - x0 < r2 - x0 by A22,XXREAL_0:2;
then
A35: x - x0 + x0 < r2 - x0 + x0 by XREAL_1:6;
r2 in X /\ dom (f|X) by A16,XBOOLE_0:def 4;
then (f|X).x <= (f|X).r2 by A4,A35,A25,RFUNCT_2:22;
then (f|X).x in [.M1,M2.] by A11,A17,A34;
hence (f|X).x in N1 by A8,A30;
end;
hence thesis by FCONT_1:4;
end;
hence thesis by FCONT_1:def 2;
end;
suppose
f|X is non-increasing;
then
A36: f|X|X is non-increasing;
for x0 be Real st x0 in dom(f|X) holds f|X is_continuous_in x0
proof
let x0 be Real;
A37: (f|X).:X = f.:X by RELAT_1:129;
assume x0 in dom(f|X);
then
x0 in X;
then x0 in dom f /\ X by A1,XBOOLE_0:def 4;
then
A38: x0 in dom (f|X) by RELAT_1:61;
now
let N1 be Neighbourhood of (f|X).x0;
consider r be Real such that
A39: r > 0 and
A40: N1 = ].(f|X).x0 - r,(f|X).x0 + r.[ by RCOMP_1:def 6;
reconsider r as Element of REAL by XREAL_0:def 1;
A41: (f|X).x0 < (f|X).x0 + r/2 by A39,XREAL_1:29,215;
reconsider M1 = (f|X).x0 - r/2 as Element of REAL by XREAL_0:def 1;
consider r1 being Element of REAL such that
A42: r1 in dom (f|X) & r1 in X and
A43: M1 = (f|X).r1 by A3,A37,PARTFUN2:59;
A44: (f|X).x0 < (f|X).x0 + r/2 by A39,XREAL_1:29,215;
then
A45: M1 < (f|X).x0 by XREAL_1:19;
A46: now
assume
A47: x0 > r1;
x0 in X /\ dom (f|X) & r1 in X /\ dom(f|X) by A38,A42,
XBOOLE_0:def 4;
hence contradiction by A36,A43,A45,A47,RFUNCT_2:23;
end;
reconsider M2 = (f|X).x0 + r/2 as Element of REAL by XREAL_0:def 1;
consider r2 being Element of REAL such that
A48: r2 in dom (f|X) & r2 in X and
A49: M2 = (f|X).r2 by A3,A37,PARTFUN2:59;
A50: M2 > (f|X).x0 by A39,XREAL_1:29,215;
A51: now
assume
A52: r2 > x0;
x0 in X /\ dom (f|X) & r2 in X /\ dom (f|X) by A38,A48,
XBOOLE_0:def 4;
hence contradiction by A36,A49,A50,A52,RFUNCT_2:23;
end;
x0 <> r2 by A39,A49,XREAL_1:29,215;
then x0 > r2 by A51,XXREAL_0:1;
then
A53: x0 - r2 > 0 by XREAL_1:50;
set R = min(r1 - x0,x0 - r2);
A54: R <= r1 - x0 by XXREAL_0:17;
r1 <> x0 by A43,A44,XREAL_1:19;
then r1 > x0 by A46,XXREAL_0:1;
then r1 - x0 > 0 by XREAL_1:50;
then R > 0 by A53,XXREAL_0:15;
then reconsider N = ].x0 - R,x0 + R.[ as Neighbourhood of x0 by
RCOMP_1:def 6;
take N;
let x be Real;
assume that
A55: x in dom (f|X) and
A56: x in N;
A57: x in X /\ dom(f|X) by A55,XBOOLE_1:28;
A58: (f|X).x0 + r/2 < (f|X).x0 + r/2 + r/2 by A39,XREAL_1:29,215;
A59: (f|X).x0 < (f|X).x0 + r by A39,XREAL_1:29;
then (f|X).x0 - r < (f|X).x0 + r - r by XREAL_1:9;
then (f|X).x0 - r < (f|X).x0 + r/2 by A41,XXREAL_0:2;
then
A60: M2 in ].(f|X).x0 - r,(f|X).x0 + r.[ by A58;
A61: (f|X).x0 - r < (f|X).x0 - r + r/2 by A39,XREAL_1:29,215;
(f|X).x0 - r/2 < (f|X).x0 by A41,XREAL_1:19;
then (f|X).x0 - r/2 < (f|X).x0 + r by A59,XXREAL_0:2;
then M1 in ].(f|X).x0 - r,(f|X).x0 + r.[ by A61;
then
A62: [.M1,M2.] c= ].(f|X).x0 - r,(f|X).x0 + r.[ by A60,XXREAL_2:def 12;
A63: ex s st s = x & x0 - R < s & s < x0 + R by A56;
then x0 < R + x by XREAL_1:19;
then
A64: x0 - x < R + x - x by XREAL_1:9;
x - x0 < R by A63,XREAL_1:19;
then x - x0 < r1-x0 by A54,XXREAL_0:2;
then
A65: x - x0 + x0 < r1 - x0 + x0 by XREAL_1:6;
r1 in X /\ dom(f|X) by A42,XBOOLE_0:def 4;
then
A66: (f|X).r1 <= (f|X).x by A36,A65,A57,RFUNCT_2:23;
R <= x0 - r2 by XXREAL_0:17;
then x0 - x < x0 - r2 by A64,XXREAL_0:2;
then -(x0 - x) > -(x0 - r2) by XREAL_1:24;
then
A67: x - x0 + x0 > r2 - x0 + x0 by XREAL_1:6;
r2 in X /\ dom(f|X) by A48,XBOOLE_0:def 4;
then (f|X).x <= (f|X).r2 by A36,A67,A57,RFUNCT_2:23;
then (f|X).x in [.M1,M2.] by A43,A49,A66;
hence (f|X).x in N1 by A40,A62;
end;
hence thesis by FCONT_1:4;
end;
hence thesis by FCONT_1:def 2;
end;
end;
hence thesis;
end;
theorem
for f be one-to-one PartFunc of REAL,REAL st (f|].p,g.[ is increasing
or f|].p,g.[ is decreasing) & ].p,g.[ c= dom f holds (f|].p,g.[)"|(f.:].p,g.[)
is continuous
proof
let f be one-to-one PartFunc of REAL,REAL;
assume that
A1: f|].p,g.[ is increasing or f|].p,g.[ is decreasing and
A2: ].p,g.[ c= dom f;
now
per cases by A1;
suppose
A3: f|].p,g.[ is increasing;
A4: now
let r be Element of REAL;
assume r in f.:].p,g.[;
then consider s being Element of REAL such that
A5: s in dom f & s in ].p,g.[ and
A6: r = f.s by PARTFUN2:59;
s in dom f /\ ].p,g.[ by A5,XBOOLE_0:def 4;
then
A7: s in dom (f|].p,g.[) by RELAT_1:61;
then r = (f|].p,g.[).s by A6,FUNCT_1:47;
then r in rng (f|].p,g.[) by A7,FUNCT_1:def 3;
hence r in dom ((f|].p,g.[)") by FUNCT_1:33;
end;
A8: ((f|].p,g.[)").:(f.:].p,g.[) = ((f|].p,g.[)").:(rng (f|].p,g.[)) by
RELAT_1:115
.= ((f|].p,g.[)").:(dom ((f|].p,g.[)")) by FUNCT_1:33
.= rng ((f|].p,g.[)") by RELAT_1:113
.= dom (f|].p,g.[) by FUNCT_1:33
.= dom f /\ ].p,g.[ by RELAT_1:61
.= ].p,g.[ by A2,XBOOLE_1:28;
(f|].p,g.[)"|(f.:].p,g.[) is increasing by A3,Th9;
hence thesis by A4,A8,Th15,SUBSET_1:2;
end;
suppose
A9: f|].p,g.[ is decreasing;
A10: now
let r be Element of REAL;
assume r in f.:].p,g.[;
then consider s being Element of REAL such that
A11: s in dom f & s in ].p,g.[ and
A12: r = f.s by PARTFUN2:59;
s in dom f /\ ].p,g.[ by A11,XBOOLE_0:def 4;
then
A13: s in dom (f|].p,g.[) by RELAT_1:61;
then r = (f|].p,g.[).s by A12,FUNCT_1:47;
then r in rng (f|].p,g.[) by A13,FUNCT_1:def 3;
hence r in dom ((f|].p,g.[)") by FUNCT_1:33;
end;
A14: ((f|].p,g.[)").:(f.:].p,g.[) = ((f|].p,g.[)").:(rng (f|].p,g.[)) by
RELAT_1:115
.= ((f|].p,g.[)").:(dom ((f|].p,g.[)")) by FUNCT_1:33
.= rng ((f|].p,g.[)") by RELAT_1:113
.= dom (f|].p,g.[) by FUNCT_1:33
.= dom f /\ ].p,g.[ by RELAT_1:61
.= ].p,g.[ by A2,XBOOLE_1:28;
(f|].p,g.[)"|(f.:].p,g.[) is decreasing by A9,Th10;
hence thesis by A10,A14,Th15,SUBSET_1:2;
end;
end;
hence thesis;
end;
theorem
for f be one-to-one PartFunc of REAL,REAL st (f|left_open_halfline p
is increasing or f|left_open_halfline p is decreasing) & left_open_halfline(p)
c= dom f holds (f|left_open_halfline(p))"|(f.:left_open_halfline(p)) is
continuous
proof
let f be one-to-one PartFunc of REAL,REAL;
set L = left_open_halfline(p);
assume that
A1: f|L is increasing or f|L is decreasing and
A2: L c= dom f;
now
per cases by A1;
suppose
A3: f|L is increasing;
A4: now
let r be Element of REAL;
assume r in f.:L;
then consider s being Element of REAL such that
A5: s in dom f & s in L and
A6: r = f.s by PARTFUN2:59;
s in dom f /\ L by A5,XBOOLE_0:def 4;
then
A7: s in dom (f|L) by RELAT_1:61;
then r = (f|L).s by A6,FUNCT_1:47;
then r in rng (f|L) by A7,FUNCT_1:def 3;
hence r in dom ((f|L)") by FUNCT_1:33;
end;
A8: ((f|L)").:(f.:L) = ((f|L)").:(rng (f|L)) by RELAT_1:115
.= ((f|L)").:(dom ((f|L)")) by FUNCT_1:33
.= rng ((f|L)") by RELAT_1:113
.= dom (f|L) by FUNCT_1:33
.= dom f /\ L by RELAT_1:61
.= L by A2,XBOOLE_1:28;
(f|L)"|(f.:L) is increasing by A3,Th9;
hence thesis by A4,A8,Th11,SUBSET_1:2;
end;
suppose
A9: f|L is decreasing;
A10: now
let r be Element of REAL;
assume r in f.:L;
then consider s being Element of REAL such that
A11: s in dom f & s in L and
A12: r = f.s by PARTFUN2:59;
s in dom f /\ L by A11,XBOOLE_0:def 4;
then
A13: s in dom (f|L) by RELAT_1:61;
then r = (f|L).s by A12,FUNCT_1:47;
then r in rng (f|L) by A13,FUNCT_1:def 3;
hence r in dom ((f|L)") by FUNCT_1:33;
end;
A14: ((f|L)").:(f.:L) = ((f|L)").:(rng (f|L)) by RELAT_1:115
.= ((f|L)").:(dom ((f|L)")) by FUNCT_1:33
.= rng ((f|L)") by RELAT_1:113
.= dom (f|L) by FUNCT_1:33
.= dom f /\ L by RELAT_1:61
.= L by A2,XBOOLE_1:28;
(f|L)"|(f.:L) is decreasing by A9,Th10;
hence thesis by A10,A14,Th11,SUBSET_1:2;
end;
end;
hence thesis;
end;
theorem
for f be one-to-one PartFunc of REAL,REAL st (f|right_open_halfline p
is increasing or f|right_open_halfline p is decreasing) & right_open_halfline(p
) c= dom f holds (f|right_open_halfline(p))"|(f.:right_open_halfline(p)) is
continuous
proof
let f be one-to-one PartFunc of REAL,REAL;
set L = right_open_halfline(p);
assume that
A1: f|L is increasing or f|L is decreasing and
A2: L c= dom f;
now
per cases by A1;
suppose
A3: f|L is increasing;
A4: now
let r be Element of REAL;
assume r in f.:L;
then consider s being Element of REAL such that
A5: s in dom f & s in L and
A6: r = f.s by PARTFUN2:59;
s in dom f /\ L by A5,XBOOLE_0:def 4;
then
A7: s in dom (f|L) by RELAT_1:61;
then r = (f|L).s by A6,FUNCT_1:47;
then r in rng (f|L) by A7,FUNCT_1:def 3;
hence r in dom ((f|L)") by FUNCT_1:33;
end;
A8: ((f|L)").:(f.:L) = ((f|L)").:(rng (f|L)) by RELAT_1:115
.= ((f|L)").:(dom ((f|L)")) by FUNCT_1:33
.= rng ((f|L)") by RELAT_1:113
.= dom (f|L) by FUNCT_1:33
.= dom f /\ L by RELAT_1:61
.= L by A2,XBOOLE_1:28;
(f|L)"|(f.:L) is increasing by A3,Th9;
hence thesis by A4,A8,Th12,SUBSET_1:2;
end;
suppose
A9: f|L is decreasing;
A10: now
let r be Element of REAL;
assume r in f.:L;
then consider s being Element of REAL such that
A11: s in dom f & s in L and
A12: r = f.s by PARTFUN2:59;
s in dom f /\ L by A11,XBOOLE_0:def 4;
then
A13: s in dom (f|L) by RELAT_1:61;
then r = (f|L).s by A12,FUNCT_1:47;
then r in rng (f|L) by A13,FUNCT_1:def 3;
hence r in dom ((f|L)") by FUNCT_1:33;
end;
A14: ((f|L)").:(f.:L) = ((f|L)").:(rng (f|L)) by RELAT_1:115
.= ((f|L)").:(dom ((f|L)")) by FUNCT_1:33
.= rng ((f|L)") by RELAT_1:113
.= dom (f|L) by FUNCT_1:33
.= dom f /\ L by RELAT_1:61
.= L by A2,XBOOLE_1:28;
(f|L)"|(f.:L) is decreasing by A9,Th10;
hence thesis by A10,A14,Th12,SUBSET_1:2;
end;
end;
hence thesis;
end;
theorem
for f be one-to-one PartFunc of REAL,REAL st (f|left_closed_halfline p
is increasing or f|left_closed_halfline p is decreasing) & left_closed_halfline
(p) c= dom f holds (f|left_closed_halfline(p))"|(f.:left_closed_halfline(p)) is
continuous
proof
let f be one-to-one PartFunc of REAL,REAL;
set L = left_closed_halfline(p);
assume that
A1: f|L is increasing or f|L is decreasing and
A2: L c= dom f;
now
per cases by A1;
suppose
A3: f|L is increasing;
A4: now
let r be Element of REAL;
assume r in f.:L;
then consider s being Element of REAL such that
A5: s in dom f & s in L and
A6: r = f.s by PARTFUN2:59;
s in dom f /\ L by A5,XBOOLE_0:def 4;
then
A7: s in dom (f|L) by RELAT_1:61;
then r = (f|L).s by A6,FUNCT_1:47;
then r in rng (f|L) by A7,FUNCT_1:def 3;
hence r in dom ((f|L)") by FUNCT_1:33;
end;
A8: ((f|L)").:(f.:L) = ((f|L)").:(rng (f|L)) by RELAT_1:115
.= ((f|L)").:(dom ((f|L)")) by FUNCT_1:33
.= rng ((f|L)") by RELAT_1:113
.= dom (f|L) by FUNCT_1:33
.= dom f /\ L by RELAT_1:61
.= L by A2,XBOOLE_1:28;
(f|L)"|(f.:L) is increasing by A3,Th9;
hence thesis by A4,A8,Th13,SUBSET_1:2;
end;
suppose
A9: f|L is decreasing;
A10: now
let r be Element of REAL;
assume r in f.:L;
then consider s being Element of REAL such that
A11: s in dom f & s in L and
A12: r = f.s by PARTFUN2:59;
s in dom f /\ L by A11,XBOOLE_0:def 4;
then
A13: s in dom (f|L) by RELAT_1:61;
then r = (f|L).s by A12,FUNCT_1:47;
then r in rng (f|L) by A13,FUNCT_1:def 3;
hence r in dom ((f|L)") by FUNCT_1:33;
end;
A14: ((f|L)").:(f.:L) = ((f|L)").:(rng (f|L)) by RELAT_1:115
.= ((f|L)").:(dom ((f|L)")) by FUNCT_1:33
.= rng ((f|L)") by RELAT_1:113
.= dom (f|L) by FUNCT_1:33
.= dom f /\ L by RELAT_1:61
.= L by A2,XBOOLE_1:28;
(f|L)"|(f.:L) is decreasing by A9,Th10;
hence thesis by A10,A14,Th13,SUBSET_1:2;
end;
end;
hence thesis;
end;
theorem
for f be one-to-one PartFunc of REAL,REAL st (f|right_closed_halfline
p is increasing or f|right_closed_halfline p is decreasing) &
right_closed_halfline(p) c= dom f holds (f|right_closed_halfline(p))"|(f.:
right_closed_halfline(p)) is continuous
proof
let f be one-to-one PartFunc of REAL,REAL;
set L = right_closed_halfline(p);
assume that
A1: f|L is increasing or f|L is decreasing and
A2: L c= dom f;
now
per cases by A1;
suppose
A3: f|L is increasing;
A4: now
let r be Element of REAL;
assume r in f.:L;
then consider s being Element of REAL such that
A5: s in dom f & s in L and
A6: r = f.s by PARTFUN2:59;
s in dom f /\ L by A5,XBOOLE_0:def 4;
then
A7: s in dom (f|L) by RELAT_1:61;
then r = (f|L).s by A6,FUNCT_1:47;
then r in rng (f|L) by A7,FUNCT_1:def 3;
hence r in dom ((f|L)") by FUNCT_1:33;
end;
A8: ((f|L)").:(f.:L) = ((f|L)").:(rng (f|L)) by RELAT_1:115
.= ((f|L)").:(dom ((f|L)")) by FUNCT_1:33
.= rng ((f|L)") by RELAT_1:113
.= dom (f|L) by FUNCT_1:33
.= dom f /\ L by RELAT_1:61
.= L by A2,XBOOLE_1:28;
(f|L)"|(f.:L) is increasing by A3,Th9;
hence thesis by A4,A8,Th14,SUBSET_1:2;
end;
suppose
A9: f|L is decreasing;
A10: now
let r be Element of REAL;
assume r in f.:L;
then consider s being Element of REAL such that
A11: s in dom f & s in L and
A12: r = f.s by PARTFUN2:59;
s in dom f /\ L by A11,XBOOLE_0:def 4;
then
A13: s in dom (f|L) by RELAT_1:61;
then r = (f|L).s by A12,FUNCT_1:47;
then r in rng (f|L) by A13,FUNCT_1:def 3;
hence r in dom ((f|L)") by FUNCT_1:33;
end;
A14: ((f|L)").:(f.:L) = ((f|L)").:(rng (f|L)) by RELAT_1:115
.= ((f|L)").:(dom ((f|L)")) by FUNCT_1:33
.= rng ((f|L)") by RELAT_1:113
.= dom (f|L) by FUNCT_1:33
.= dom f /\ L by RELAT_1:61
.= L by A2,XBOOLE_1:28;
(f|L)"|(f.:L) is decreasing by A9,Th10;
hence thesis by A10,A14,Th14,SUBSET_1:2;
end;
end;
hence thesis;
end;
theorem
for f be one-to-one PartFunc of REAL,REAL st (f|[#]REAL is increasing
or f|[#]REAL is decreasing) & f is total holds f"|rng f is continuous
proof
set L = [#] REAL;
let f be one-to-one PartFunc of REAL,REAL;
assume that
A1: f|[#]REAL is increasing or f|[#]REAL is decreasing and
A2: f is total;
A3: dom f = [#] REAL by A2,PARTFUN1:def 2;
now
per cases by A1;
suppose
A4: f|L is increasing;
A5: now
let r be Element of REAL;
assume r in f.:L;
then consider s being Element of REAL such that
A6: s in dom f and
s in L and
A7: r = f.s by PARTFUN2:59;
s in dom f /\ L by A6,XBOOLE_0:def 4;
then
A8: s in dom (f|L) by RELAT_1:61;
r = (f|L).s by A7;
then r in rng (f|L) by A8,FUNCT_1:def 3;
hence r in dom ((f|L)") by FUNCT_1:33;
end;
A9: ((f|L)").:(f.:L) = ((f|L)").:(rng (f|L)) by RELAT_1:115
.= ((f|L)").:(dom ((f|L)")) by FUNCT_1:33
.= rng ((f|L)") by RELAT_1:113
.= dom (f|L) by FUNCT_1:33
.= dom f /\ L by RELAT_1:61
.= REAL by A3;
(f|L)"|(f.:L) is increasing by A4,Th9;
then (f|L)"|(f.:L) is continuous by A5,A9,Th16,SUBSET_1:2;
then (f|L)"|rng f is continuous by A3,RELAT_1:113;
hence thesis;
end;
suppose
A10: f|L is decreasing;
A11: now
let r be Element of REAL;
assume r in f.:L;
then consider s being Element of REAL such that
A12: s in dom f and
s in L and
A13: r = f.s by PARTFUN2:59;
s in dom f /\ L by A12,XBOOLE_0:def 4;
then
A14: s in dom (f|L) by RELAT_1:61;
r = (f|L).s by A13;
then r in rng (f|L) by A14,FUNCT_1:def 3;
hence r in dom ((f|L)") by FUNCT_1:33;
end;
A15: ((f|L)").:(f.:L) = ((f|L)").:(rng (f|L)) by RELAT_1:115
.= ((f|L)").:(dom ((f|L)")) by FUNCT_1:33
.= rng ((f|L)") by RELAT_1:113
.= dom (f|L) by FUNCT_1:33
.= dom f /\ L by RELAT_1:61
.= REAL by A3;
(f|L)"|(f.:L) is decreasing by A10,Th10;
then (f|L)"|(f.:L) is continuous by A11,A15,Th16,SUBSET_1:2;
then (f|L)"|rng f is continuous by A3,RELAT_1:113;
hence thesis;
end;
end;
hence thesis;
end;
theorem
].p,g.[ c= dom f & f|].p,g.[ is continuous & (f|].p,g.[ is increasing
or f|].p,g.[ is decreasing) implies rng (f|].p,g.[) is open
proof
assume that
A1: ].p,g.[ c= dom f and
A2: f|].p,g.[ is continuous and
A3: f|].p,g.[ is increasing or f|].p,g.[ is decreasing;
now
let r1 be Element of REAL;
set f1 = f|].p,g.[;
assume r1 in rng f1;
then consider x0 being Element of REAL such that
A4: x0 in dom f1 and
A5: f1.x0 = r1 by PARTFUN1:3;
A6: r1 = f.x0 by A4,A5,FUNCT_1:47;
A7: x0 in dom f /\ ].p,g.[ by A4,RELAT_1:61;
then x0 in ].p,g.[ by XBOOLE_0:def 4;
then consider N be Neighbourhood of x0 such that
A8: N c= ].p,g.[ by RCOMP_1:18;
consider r be Real such that
A9: 0 < r and
A10: N = ].x0 - r, x0 + r.[ by RCOMP_1:def 6;
reconsider r as Element of REAL by XREAL_0:def 1;
0 < r/2 by A9,XREAL_1:215;
then
A11: x0 - r/2 < x0 - 0 by XREAL_1:15;
A12: r/2 < r by A9,XREAL_1:216;
then
A13: x0 - r < x0 - r/2 by XREAL_1:15;
A14: N c= dom f by A1,A8;
set fp = f.(x0 + r/2);
set fm = f.(x0 - r/2);
A15: x0 + r/2 < x0 + r by A12,XREAL_1:8;
A16: x0 < x0 + r/2 by A9,XREAL_1:29,215;
then
A17: x0 - r/2 < x0 + r/2 by A11,XXREAL_0:2;
x0 < x0 + r by A9,XREAL_1:29;
then x0 - r/2 < x0 + r by A11,XXREAL_0:2;
then
A18: x0 - r/2 in ].x0 - r, x0 + r.[ by A13;
then
A19: x0 - r/2 in ].p,g.[ /\ dom f by A8,A10,A14,XBOOLE_0:def 4;
x0 - r < x0 by A9,XREAL_1:44;
then x0 - r < x0 + r/2 by A16,XXREAL_0:2;
then
A20: x0 + r/2 in ].x0 - r, x0 + r.[ by A15;
then
A21: x0 + r/2 in ].p,g.[ /\ dom f by A8,A10,A14,XBOOLE_0:def 4;
A22: [.x0 - r/2, x0 + r/2.] c= ].x0 - r, x0 + r.[ by A18,A20,XXREAL_2:def 12;
A23: [.x0 - r/2, x0 + r/2.] c= ].p,g.[ by A8,A10,A18,A20,XXREAL_2:def 12;
then
A24: f|[.x0 - r/2, x0 + r/2.] is continuous by A2,FCONT_1:16;
now
per cases by A3;
suppose
A25: f|].p,g.[ is increasing;
set R = min(f.x0 - fm,fp - f.x0);
f.x0 < fp by A7,A16,A21,A25,RFUNCT_2:20;
then
A26: 0 < fp - f.x0 by XREAL_1:50;
fm < f.x0 by A7,A11,A19,A25,RFUNCT_2:20;
then 0 < f.x0 - fm by XREAL_1:50;
then 0 < R by A26,XXREAL_0:15;
then reconsider N1 = ].r1 - R, r1 + R.[ as Neighbourhood of r1 by
RCOMP_1:def 6;
take N1;
fm < fp by A17,A21,A19,A25,RFUNCT_2:20;
then [.fp,fm.] = {} by XXREAL_1:29;
then
A27: [.fm,fp.] \/ [.fp,fm.] = [.fm,fp.];
thus N1 c= rng f1
proof
let x be object;
A28: ].fm,fp.[ c= [.fm,fp.] by XXREAL_1:25;
assume x in N1;
then consider r2 such that
A29: r2 = x and
A30: f.x0 - R < r2 and
A31: r2 < f.x0 + R by A6;
R <= fp - f.x0 by XXREAL_0:17;
then f.x0 + R <= f.x0 + (fp - f.x0) by XREAL_1:7;
then
A32: r2 < fp by A31,XXREAL_0:2;
R <= f.x0 - fm by XXREAL_0:17;
then f.x0 - (f.x0 - fm) <= f.x0 - R by XREAL_1:13;
then fm < r2 by A30,XXREAL_0:2;
then r2 in ].fm,fp.[ by A32;
then consider s such that
A33: s in [.x0 - r/2, x0 + r/2.] and
A34: x = f.s by A1,A23,A24,A17,A27,A29,A28,FCONT_2:15,XBOOLE_1:1;
s in N by A10,A22,A33;
then s in dom f /\ ].p,g.[ by A8,A14,XBOOLE_0:def 4;
then
A35: s in dom f1 by RELAT_1:61;
then x = f1.s by A34,FUNCT_1:47;
hence thesis by A35,FUNCT_1:def 3;
end;
end;
suppose
A36: f|].p,g.[ is decreasing;
set R = min(fm - f.x0,f.x0 - fp);
fp < f.x0 by A7,A16,A21,A36,RFUNCT_2:21;
then
A37: 0 < f.x0 - fp by XREAL_1:50;
f.x0 < fm by A7,A11,A19,A36,RFUNCT_2:21;
then 0 < fm - f.x0 by XREAL_1:50;
then 0 < R by A37,XXREAL_0:15;
then reconsider N1 = ].r1 - R, r1 + R.[ as Neighbourhood of r1 by
RCOMP_1:def 6;
take N1;
fp < fm by A17,A21,A19,A36,RFUNCT_2:21;
then [.fm,fp.] = {} by XXREAL_1:29;
then
A38: [.fm,fp.] \/ [.fp,fm.] = [.fp,fm.];
thus N1 c= rng f1
proof
let x be object;
A39: ].fp,fm.[ c= [.fp,fm.] by XXREAL_1:25;
assume x in N1;
then consider r2 such that
A40: r2 = x and
A41: f.x0 - R < r2 and
A42: r2 < f.x0 + R by A6;
R <= fm - f.x0 by XXREAL_0:17;
then f.x0 + R <= f.x0 + (fm - f.x0) by XREAL_1:7;
then
A43: r2 < fm by A42,XXREAL_0:2;
R <= f.x0 - fp by XXREAL_0:17;
then f.x0 - (f.x0 - fp) <= f.x0 - R by XREAL_1:13;
then fp < r2 by A41,XXREAL_0:2;
then r2 in ].fp,fm.[ by A43;
then consider s such that
A44: s in [.x0 - r/2, x0 + r/2.] and
A45: x = f.s by A1,A23,A24,A17,A38,A40,A39,FCONT_2:15,XBOOLE_1:1;
s in N by A10,A22,A44;
then s in dom f /\ ].p,g.[ by A8,A14,XBOOLE_0:def 4;
then
A46: s in dom f1 by RELAT_1:61;
then x = f1.s by A45,FUNCT_1:47;
hence thesis by A46,FUNCT_1:def 3;
end;
end;
end;
hence ex N be Neighbourhood of r1 st N c= rng f1;
end;
hence thesis by RCOMP_1:20;
end;
theorem
left_open_halfline(p) c= dom f & f|left_open_halfline p is continuous
& (f|left_open_halfline p is increasing or f|left_open_halfline p is decreasing
) implies rng (f|left_open_halfline(p)) is open
proof
set L = left_open_halfline(p);
assume that
A1: left_open_halfline(p) c= dom f and
A2: f|L is continuous and
A3: f|L is increasing or f|L is decreasing;
now
let r1 be Element of REAL;
set f1 = f|L;
assume r1 in rng f1;
then consider x0 being Element of REAL such that
A4: x0 in dom f1 and
A5: f1.x0 = r1 by PARTFUN1:3;
A6: r1 = f.x0 by A4,A5,FUNCT_1:47;
A7: x0 in dom f /\ L by A4,RELAT_1:61;
then x0 in L by XBOOLE_0:def 4;
then consider N be Neighbourhood of x0 such that
A8: N c= L by RCOMP_1:18;
consider r be Real such that
A9: 0 < r and
A10: N = ].x0 - r, x0 + r.[ by RCOMP_1:def 6;
reconsider r as Element of REAL by XREAL_0:def 1;
0 < r/2 by A9,XREAL_1:215;
then
A11: x0 - r/2 < x0 - 0 by XREAL_1:15;
A12: r/2 < r by A9,XREAL_1:216;
then
A13: x0 - r < x0 - r/2 by XREAL_1:15;
A14: N c= dom f by A1,A8;
set fp = f.(x0 + r/2);
set fm = f.(x0 - r/2);
A15: x0 + r/2 < x0 + r by A12,XREAL_1:8;
A16: x0 < x0 + r/2 by A9,XREAL_1:29,215;
then
A17: x0 - r/2 < x0 + r/2 by A11,XXREAL_0:2;
x0 < x0 + r by A9,XREAL_1:29;
then x0 - r/2 < x0 + r by A11,XXREAL_0:2;
then
A18: x0 - r/2 in ].x0 - r, x0 + r.[ by A13;
then
A19: x0 - r/2 in L /\ dom f by A8,A10,A14,XBOOLE_0:def 4;
x0 - r < x0 by A9,XREAL_1:44;
then x0 - r < x0 + r/2 by A16,XXREAL_0:2;
then
A20: x0 + r/2 in ].x0 - r, x0 + r.[ by A15;
then
A21: x0 + r/2 in L /\ dom f by A8,A10,A14,XBOOLE_0:def 4;
A22: [.x0 - r/2, x0 + r/2.] c= ].x0 - r, x0 + r.[ by A18,A20,XXREAL_2:def 12;
f|N is continuous by A2,A8,FCONT_1:16;
then
A23: f|[.x0 - r/2, x0 + r/2.] is continuous by A10,A22,FCONT_1:16;
A24: [.x0 - r/2, x0 + r/2.] c= L by A8,A10,A18,A20,XXREAL_2:def 12;
now
per cases by A3;
suppose
A25: f|L is increasing;
set R = min(f.x0 - fm,fp - f.x0);
f.x0 < fp by A7,A16,A21,A25,RFUNCT_2:20;
then
A26: 0 < fp - f.x0 by XREAL_1:50;
fm < f.x0 by A7,A11,A19,A25,RFUNCT_2:20;
then 0 < f.x0 - fm by XREAL_1:50;
then 0 < R by A26,XXREAL_0:15;
then reconsider N1 = ].r1 - R, r1 + R.[ as Neighbourhood of r1 by
RCOMP_1:def 6;
take N1;
fm < fp by A17,A21,A19,A25,RFUNCT_2:20;
then [.fp,fm.] = {} by XXREAL_1:29;
then
A27: [.fm,fp.] \/ [.fp,fm.] = [.fm,fp.];
thus N1 c= rng f1
proof
let x be object;
A28: ].fm,fp.[ c= [.fm,fp.] by XXREAL_1:25;
assume x in N1;
then consider r2 such that
A29: r2 = x and
A30: f.x0 - R < r2 and
A31: r2 < f.x0 + R by A6;
R <= fp - f.x0 by XXREAL_0:17;
then f.x0 + R <= f.x0 + (fp - f.x0) by XREAL_1:7;
then
A32: r2 < fp by A31,XXREAL_0:2;
R <= f.x0 - fm by XXREAL_0:17;
then f.x0 - (f.x0 - fm) <= f.x0 - R by XREAL_1:13;
then fm < r2 by A30,XXREAL_0:2;
then r2 in ].fm,fp.[ by A32;
then consider s such that
A33: s in [.x0 - r/2, x0 + r/2.] and
A34: x = f.s by A1,A24,A23,A17,A27,A29,A28,FCONT_2:15,XBOOLE_1:1;
s in N by A10,A22,A33;
then s in dom f /\ L by A8,A14,XBOOLE_0:def 4;
then
A35: s in dom f1 by RELAT_1:61;
then x = f1.s by A34,FUNCT_1:47;
hence thesis by A35,FUNCT_1:def 3;
end;
end;
suppose
A36: f|L is decreasing;
set R = min(fm - f.x0,f.x0 - fp);
fp < f.x0 by A7,A16,A21,A36,RFUNCT_2:21;
then
A37: 0 < f.x0 - fp by XREAL_1:50;
f.x0 < fm by A7,A11,A19,A36,RFUNCT_2:21;
then 0 < fm - f.x0 by XREAL_1:50;
then 0 < R by A37,XXREAL_0:15;
then reconsider N1 = ].r1 - R, r1 + R.[ as Neighbourhood of r1 by
RCOMP_1:def 6;
take N1;
fp < fm by A17,A21,A19,A36,RFUNCT_2:21;
then [.fm,fp.] = {} by XXREAL_1:29;
then
A38: [.fm,fp.] \/ [.fp,fm.] = [.fp,fm.];
thus N1 c= rng f1
proof
let x be object;
A39: ].fp,fm.[ c= [.fp,fm.] by XXREAL_1:25;
assume x in N1;
then consider r2 such that
A40: r2 = x and
A41: f.x0 - R < r2 and
A42: r2 < f.x0 + R by A6;
R <= fm - f.x0 by XXREAL_0:17;
then f.x0 + R <= f.x0 + (fm - f.x0) by XREAL_1:7;
then
A43: r2 < fm by A42,XXREAL_0:2;
R <= f.x0 - fp by XXREAL_0:17;
then f.x0 - (f.x0 - fp) <= f.x0 - R by XREAL_1:13;
then fp < r2 by A41,XXREAL_0:2;
then r2 in ].fp,fm.[ by A43;
then consider s such that
A44: s in [.x0 - r/2, x0 + r/2.] and
A45: x = f.s by A1,A24,A23,A17,A38,A40,A39,FCONT_2:15,XBOOLE_1:1;
s in N by A10,A22,A44;
then s in dom f /\ L by A8,A14,XBOOLE_0:def 4;
then
A46: s in dom f1 by RELAT_1:61;
then x = f1.s by A45,FUNCT_1:47;
hence thesis by A46,FUNCT_1:def 3;
end;
end;
end;
hence ex N be Neighbourhood of r1 st N c= rng f1;
end;
hence thesis by RCOMP_1:20;
end;
theorem
right_open_halfline(p) c= dom f & f|right_open_halfline p is
continuous & (f|right_open_halfline p is increasing or f|right_open_halfline p
is decreasing) implies rng (f|right_open_halfline(p)) is open
proof
set L = right_open_halfline(p);
assume that
A1: right_open_halfline(p) c= dom f and
A2: f|L is continuous and
A3: f|L is increasing or f|L is decreasing;
now
let r1 be Element of REAL;
set f1 = f|L;
assume r1 in rng f1;
then consider x0 being Element of REAL such that
A4: x0 in dom f1 and
A5: f1.x0 = r1 by PARTFUN1:3;
A6: r1 = f.x0 by A4,A5,FUNCT_1:47;
A7: x0 in dom f /\ L by A4,RELAT_1:61;
then x0 in L by XBOOLE_0:def 4;
then consider N be Neighbourhood of x0 such that
A8: N c= L by RCOMP_1:18;
consider r be Real such that
A9: 0 < r and
A10: N = ].x0 - r, x0 + r.[ by RCOMP_1:def 6;
reconsider r as Element of REAL by XREAL_0:def 1;
0 < r/2 by A9,XREAL_1:215;
then
A11: x0 - r/2 < x0 - 0 by XREAL_1:15;
A12: r/2 < r by A9,XREAL_1:216;
then
A13: x0 - r < x0 - r/2 by XREAL_1:15;
A14: N c= dom f by A1,A8;
set fp = f.(x0 + r/2);
set fm = f.(x0 - r/2);
A15: x0 + r/2 < x0 + r by A12,XREAL_1:8;
A16: x0 < x0 + r/2 by A9,XREAL_1:29,215;
then
A17: x0 - r/2 < x0 + r/2 by A11,XXREAL_0:2;
x0 < x0 + r by A9,XREAL_1:29;
then x0 - r/2 < x0 + r by A11,XXREAL_0:2;
then
A18: x0 - r/2 in ].x0 - r, x0 + r.[ by A13;
then
A19: x0 - r/2 in L /\ dom f by A8,A10,A14,XBOOLE_0:def 4;
x0 - r < x0 by A9,XREAL_1:44;
then x0 - r < x0 + r/2 by A16,XXREAL_0:2;
then
A20: x0 + r/2 in ].x0 - r, x0 + r.[ by A15;
then
A21: x0 + r/2 in L /\ dom f by A8,A10,A14,XBOOLE_0:def 4;
A22: [.x0 - r/2, x0 + r/2.] c= ].x0 - r, x0 + r.[ by A18,A20,XXREAL_2:def 12;
f|N is continuous by A2,A8,FCONT_1:16;
then
A23: f|([.x0 - r/2, x0 + r/2.]) is continuous by A10,A22,FCONT_1:16;
A24: [.x0 - r/2, x0 + r/2.] c= L by A8,A10,A18,A20,XXREAL_2:def 12;
now
per cases by A3;
suppose
A25: f|L is increasing;
set R = min(f.x0 - fm,fp - f.x0);
f.x0 < fp by A7,A16,A21,A25,RFUNCT_2:20;
then
A26: 0 < fp - f.x0 by XREAL_1:50;
fm < f.x0 by A7,A11,A19,A25,RFUNCT_2:20;
then 0 < f.x0 - fm by XREAL_1:50;
then 0 < R by A26,XXREAL_0:15;
then reconsider N1 = ].r1 - R, r1 + R.[ as Neighbourhood of r1 by
RCOMP_1:def 6;
take N1;
fm < fp by A17,A21,A19,A25,RFUNCT_2:20;
then [.fp,fm.] = {} by XXREAL_1:29;
then
A27: [.fm,fp.] \/ [.fp,fm.] = [.fm,fp.];
thus N1 c= rng f1
proof
let x be object;
A28: ].fm,fp.[ c= [.fm,fp.] by XXREAL_1:25;
assume x in N1;
then consider r2 such that
A29: r2 = x and
A30: f.x0 - R < r2 and
A31: r2 < f.x0 + R by A6;
R <= fp - f.x0 by XXREAL_0:17;
then f.x0 + R <= f.x0 + (fp - f.x0) by XREAL_1:7;
then
A32: r2 < fp by A31,XXREAL_0:2;
R <= f.x0 - fm by XXREAL_0:17;
then f.x0 - (f.x0 - fm) <= f.x0 - R by XREAL_1:13;
then fm < r2 by A30,XXREAL_0:2;
then r2 in ].fm,fp.[ by A32;
then consider s such that
A33: s in [.x0 - r/2, x0 + r/2.] and
A34: x = f.s by A1,A24,A23,A17,A27,A29,A28,FCONT_2:15,XBOOLE_1:1;
s in N by A10,A22,A33;
then s in dom f /\ L by A8,A14,XBOOLE_0:def 4;
then
A35: s in dom f1 by RELAT_1:61;
then x = f1.s by A34,FUNCT_1:47;
hence thesis by A35,FUNCT_1:def 3;
end;
end;
suppose
A36: f|L is decreasing;
set R = min(fm - f.x0,f.x0 - fp);
fp < f.x0 by A7,A16,A21,A36,RFUNCT_2:21;
then
A37: 0 < f.x0 - fp by XREAL_1:50;
f.x0 < fm by A7,A11,A19,A36,RFUNCT_2:21;
then 0 < fm - f.x0 by XREAL_1:50;
then 0 < R by A37,XXREAL_0:15;
then reconsider N1 = ].r1 - R, r1 + R.[ as Neighbourhood of r1 by
RCOMP_1:def 6;
take N1;
fp < fm by A17,A21,A19,A36,RFUNCT_2:21;
then [.fm,fp.] = {} by XXREAL_1:29;
then
A38: [.fm,fp.] \/ [.fp,fm.] = [.fp,fm.];
thus N1 c= rng f1
proof
let x be object;
A39: ].fp,fm.[ c= [.fp,fm.] by XXREAL_1:25;
assume x in N1;
then consider r2 such that
A40: r2 = x and
A41: f.x0 - R < r2 and
A42: r2 < f.x0 + R by A6;
R <= fm - f.x0 by XXREAL_0:17;
then f.x0 + R <= f.x0 + (fm - f.x0) by XREAL_1:7;
then
A43: r2 < fm by A42,XXREAL_0:2;
R <= f.x0 - fp by XXREAL_0:17;
then f.x0 - (f.x0 - fp) <= f.x0 - R by XREAL_1:13;
then fp < r2 by A41,XXREAL_0:2;
then r2 in ].fp,fm.[ by A43;
then consider s such that
A44: s in [.x0 - r/2, x0 + r/2.] and
A45: x = f.s by A1,A24,A23,A17,A38,A40,A39,FCONT_2:15,XBOOLE_1:1;
s in N by A10,A22,A44;
then s in dom f /\ L by A8,A14,XBOOLE_0:def 4;
then
A46: s in dom f1 by RELAT_1:61;
then x = f1.s by A45,FUNCT_1:47;
hence thesis by A46,FUNCT_1:def 3;
end;
end;
end;
hence ex N be Neighbourhood of r1 st N c= rng f1;
end;
hence thesis by RCOMP_1:20;
end;
theorem
[#](REAL) c= dom f & f|[#]REAL is continuous & (f|[#]REAL is
increasing or f|[#]REAL is decreasing) implies rng f is open
proof
set L = [#]REAL;
assume that
A1: [#](REAL) c= dom f and
A2: f|L is continuous and
A3: f|L is increasing or f|L is decreasing;
now
let r1 be Element of REAL;
assume r1 in rng f;
then consider x0 being Element of REAL such that
A4: x0 in dom f and
A5: f.x0 = r1 by PARTFUN1:3;
A6: x0 in L /\ dom f by A4,XBOOLE_0:def 4;
set N = the Neighbourhood of x0;
consider r be Real such that
A7: 0 < r and
A8: N = ].x0 - r, x0 + r.[ by RCOMP_1:def 6;
reconsider r as Element of REAL by XREAL_0:def 1;
0 < r/2 by A7,XREAL_1:215;
then
A9: x0 - r/2 < x0 - 0 by XREAL_1:15;
A10: r/2 < r by A7,XREAL_1:216;
then
A11: x0 - r < x0 - r/2 by XREAL_1:15;
A12: x0 + r/2 < x0 + r by A10,XREAL_1:8;
A13: N c= dom f by A1;
set fp = f.(x0 + r/2);
set fm = f.(x0 - r/2);
A14: f|([.x0 - r/2, x0 + r/2.]) is continuous by A2,FCONT_1:16;
A15: x0 < x0 + r/2 by A7,XREAL_1:29,215;
then
A16: x0 - r/2 < x0 + r/2 by A9,XXREAL_0:2;
x0 - r < x0 by A7,XREAL_1:44;
then x0 - r < x0 + r/2 by A15,XXREAL_0:2;
then
A17: x0 + r/2 in ].x0 - r, x0 + r.[ by A12;
then
A18: x0 + r/2 in L /\ dom f by A8,A13,XBOOLE_0:def 4;
x0 < x0 + r by A7,XREAL_1:29;
then x0 - r/2 < x0 + r by A9,XXREAL_0:2;
then
A19: x0 - r/2 in ].x0 - r, x0 + r.[ by A11;
then
A20: x0 - r/2 in L /\ dom f by A8,A13,XBOOLE_0:def 4;
A21: [.x0 - r/2, x0 + r/2.] c= ].x0 - r, x0 + r.[ by A19,A17,XXREAL_2:def 12;
now
per cases by A3;
suppose
A22: f|L is increasing;
set R = min(f.x0 - fm,fp - f.x0);
f.x0 < fp by A15,A18,A6,A22,RFUNCT_2:20;
then
A23: 0 < fp - f.x0 by XREAL_1:50;
fm < f.x0 by A9,A20,A6,A22,RFUNCT_2:20;
then 0 < f.x0 - fm by XREAL_1:50;
then 0 < R by A23,XXREAL_0:15;
then reconsider N1 = ].r1 - R, r1 + R.[ as Neighbourhood of r1 by
RCOMP_1:def 6;
take N1;
fm < fp by A16,A18,A20,A22,RFUNCT_2:20;
then [.fp,fm.] = {} by XXREAL_1:29;
then
A24: [.fm,fp.] \/ [.fp,fm.] = [.fm,fp.];
thus N1 c= rng f
proof
let x be object;
A25: [.x0 - r/2, x0 + r/2.] c= dom f & ].fm,fp.[ c= [.fm,fp.] by A1,
XXREAL_1:25;
assume x in N1;
then consider r2 such that
A26: r2 = x and
A27: f.x0 - R < r2 and
A28: r2 < f.x0 + R by A5;
R <= fp - f.x0 by XXREAL_0:17;
then f.x0 + R <= f.x0 + (fp - f.x0) by XREAL_1:7;
then
A29: r2 < fp by A28,XXREAL_0:2;
R <= f.x0 - fm by XXREAL_0:17;
then f.x0 - (f.x0 - fm) <= f.x0 - R by XREAL_1:13;
then fm < r2 by A27,XXREAL_0:2;
then r2 in ].fm,fp.[ by A29;
then consider s such that
A30: s in [.x0 - r/2, x0 + r/2.] and
A31: x = f.s by A9,A15,A14,A24,A26,A25,FCONT_2:15,XXREAL_0:2;
s in N by A8,A21,A30;
hence thesis by A13,A31,FUNCT_1:def 3;
end;
end;
suppose
A32: f|L is decreasing;
set R = min(fm - f.x0,f.x0 - fp);
fp < f.x0 by A15,A18,A6,A32,RFUNCT_2:21;
then
A33: 0 < f.x0 - fp by XREAL_1:50;
f.x0 < fm by A9,A20,A6,A32,RFUNCT_2:21;
then 0 < fm - f.x0 by XREAL_1:50;
then 0 < R by A33,XXREAL_0:15;
then reconsider N1 = ].r1 - R, r1 + R.[ as Neighbourhood of r1 by
RCOMP_1:def 6;
take N1;
fp < fm by A16,A18,A20,A32,RFUNCT_2:21;
then [.fm,fp.] = {} by XXREAL_1:29;
then
A34: [.fm,fp.] \/ [.fp,fm.] = [.fp,fm.];
thus N1 c= rng f
proof
let x be object;
A35: ].fp,fm.[ c= [.fp,fm.] by XXREAL_1:25;
assume x in N1;
then consider r2 such that
A36: r2 = x and
A37: f.x0 - R < r2 and
A38: r2 < f.x0 + R by A5;
R <= fm - f.x0 by XXREAL_0:17;
then f.x0 + R <= f.x0 + (fm - f.x0) by XREAL_1:7;
then
A39: r2 < fm by A38,XXREAL_0:2;
R <= f.x0 - fp by XXREAL_0:17;
then f.x0 - (f.x0 - fp) <= f.x0 - R by XREAL_1:13;
then fp < r2 by A37,XXREAL_0:2;
then r2 in ].fp,fm.[ by A39;
then consider s such that
A40: s in [.x0 - r/2, x0 + r/2.] and
A41: x = f.s by A1,A14,A16,A34,A36,A35,FCONT_2:15,XBOOLE_1:1;
s in N by A8,A21,A40;
hence thesis by A13,A41,FUNCT_1:def 3;
end;
end;
end;
hence ex N be Neighbourhood of r1 st N c= rng f;
end;
hence thesis by RCOMP_1:20;
end;