let X be set ; :: thesis: for f being PartFunc of REAL ,REAL st X c= dom f & f | X is monotone & ex p being Real st f .: X = left_closed_halfline p holds
f | X is continuous
let f be PartFunc of REAL ,REAL ; :: thesis: ( X c= dom f & f | X is monotone & ex p being Real st f .: X = left_closed_halfline p implies f | X is continuous )
assume A1: ( X c= dom f & f | X is monotone ) ; :: thesis: ( for p being Real holds not f .: X = left_closed_halfline p or f | X is continuous )
given p being Real such that A2: f .: X = left_closed_halfline p ; :: thesis: f | X is continuous
set l = left_closed_halfline p;
set L = left_open_halfline p;
for x0 being real number st x0 in dom (f | X) holds
f | X is_continuous_in x0

proof

let x0 be real number ; :: thesis: ( x0 in dom (f | X) implies f | X is_continuous_in x0 )
assume x0 in dom (f | X) ; :: thesis: f | X is_continuous_in x0
then A3: x0 in X by RELAT_1:86;
then x0 in (dom f) /\ X by A1, XBOOLE_0:def 4;
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 RELAT_1:162;
then (f | X) . x0 in {p} \/ (left_open_halfline p) by A2, A5, XXREAL_1:423;
then A7: ( (f | X) . x0 in {p} or (f | X) . x0 in left_open_halfline p ) by XBOOLE_0:def 3;
A8: left_open_halfline p c= left_closed_halfline p by XXREAL_1:21;

now

let N1 be Neighbourhood of (f | X) . x0; :: thesis: ex N being Neighbourhood of x0 st
for r1 being real number st r1 in dom (f | X) & r1 in N holds
(f | X) . r1 in N1

now

per cases ( f | X is non-decreasing or f | X is non-increasing ) by A1, RFUNCT_2:def 6;

suppose f | X is non-decreasing ; :: thesis: ex N being Neighbourhood of x0 st
for r1 being real number st r1 in dom (f | X) & r1 in N holds
(f | X) . r1 in N1

then A9: (f | X) | X is non-decreasing ;

now

per cases ( (f | X) . x0 in left_open_halfline p or (f | X) . x0 = p ) by A7, TARSKI:def 1;

suppose (f | X) . x0 in left_open_halfline p ; :: thesis: ex N being Neighbourhood of x0 st
for x being real number st x in dom (f | X) & x in N holds
(f | X) . x in N1

then consider N2 being Neighbourhood of (f | X) . x0 such that
A10: N2 c= left_open_halfline p by 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 being real number such that
A12: ( r > 0 & N3 = ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ ) by RCOMP_1:def 7;
reconsider r = 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, XREAL_1:217;
then A14: ((f | X) . x0) - r < (((f | X) . x0) - r) + (r / 2) by XREAL_1:31;
A15: (f | X) . x0 < ((f | X) . x0) + (r / 2) by A13, XREAL_1:31;
then A16: ((f | X) . x0) - (r / 2) < (f | X) . x0 by XREAL_1:21;
A17: (f | X) . x0 < ((f | X) . x0) + r by A12, XREAL_1:31;
then ((f | X) . x0) - (r / 2) < ((f | X) . x0) + r by A16, XXREAL_0:2;
then A18: ((f | X) . x0) - (r / 2) in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A14;
A19: ((f | X) . x0) + (r / 2) < (((f | X) . x0) + (r / 2)) + (r / 2) by A13, XREAL_1:31;
((f | X) . x0) - r < (((f | X) . x0) + r) - r by A17, XREAL_1:11;
then ((f | X) . x0) - r < ((f | X) . x0) + (r / 2) by A15, XXREAL_0:2;
then A20: ((f | X) . x0) + (r / 2) in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A19;
then A21: [.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] c= ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A18, XXREAL_2:def 12;
((f | X) . x0) - (r / 2) in N2 by A11, A12, A18;
then ((f | X) . x0) - (r / 2) in left_open_halfline p by A10;
then consider r1 being Real such that
A22: ( r1 in dom (f | X) & r1 in X & ((f | X) . x0) - (r / 2) = (f | X) . r1 ) by A2, A6, A8, PARTFUN2:78;
((f | X) . x0) + (r / 2) in N2 by A11, A12, A20;
then ((f | X) . x0) + (r / 2) in left_open_halfline p by A10;
then consider r2 being Real such that
A23: ( r2 in dom (f | X) & r2 in X & ((f | X) . x0) + (r / 2) = (f | X) . r2 ) by A2, A6, A8, PARTFUN2:78;
set R = min (x0 - r1),(r2 - x0);
A24: (f | X) . x0 < ((f | X) . x0) + (r / 2) by A13, XREAL_1:31;
then A25: ((f | X) . x0) - (r / 2) < (f | X) . x0 by XREAL_1:21;
A26: r1 <> x0 by A22, A24, XREAL_1:21;

now

assume A27: x0 < r1 ; :: thesis: contradiction
A28: x0 in X /\ (dom (f | X)) by A3, A4, XBOOLE_0:def 4;
r1 in X /\ (dom (f | X)) by A22, XBOOLE_0:def 4;
hence contradiction by A9, A22, A25, A27, A28, RFUNCT_2:45; :: thesis: verum

end;

then r1 < x0 by A26, XXREAL_0:1;
then A29: x0 - r1 > 0 by XREAL_1:52;
A30: ((f | X) . x0) + (r / 2) > (f | X) . x0 by A13, XREAL_1:31;
A31: x0 <> r2 by A13, A23, XREAL_1:31;

now

assume A32: r2 < x0 ; :: thesis: contradiction
A33: x0 in X /\ (dom (f | X)) by A3, A4, XBOOLE_0:def 4;
r2 in X /\ (dom (f | X)) by A23, XBOOLE_0:def 4;
hence contradiction by A9, A23, A30, A32, A33, RFUNCT_2:45; :: thesis: verum

end;

then x0 < r2 by A31, XXREAL_0:1;
then r2 - x0 > 0 by XREAL_1:52;
then min (x0 - r1),(r2 - x0) > 0 by A29, XXREAL_0:15;
then reconsider N = ].(x0 - (min (x0 - r1),(r2 - x0))),(x0 + (min (x0 - r1),(r2 - x0))).[ as Neighbourhood of x0 by RCOMP_1:def 7;
take N = N; :: thesis: for x being real number st x in dom (f | X) & x in N holds
(f | X) . x in N1
let x be real number ; :: thesis: ( x in dom (f | X) & x in N implies (f | X) . x in N1 )
assume A34: ( x in dom (f | X) & x in N ) ; :: thesis: (f | X) . x in N1
then A35: ex s being Real st
( s = x & x0 - (min (x0 - r1),(r2 - x0)) < s & s < x0 + (min (x0 - r1),(r2 - x0)) ) ;
then x0 < (min (x0 - r1),(r2 - x0)) + x by XREAL_1:21;
then A36: x0 - x < ((min (x0 - r1),(r2 - x0)) + x) - x by XREAL_1:11;
min (x0 - r1),(r2 - x0) <= x0 - r1 by XXREAL_0:17;
then x0 - x < x0 - r1 by A36, XXREAL_0:2;
then - (x0 - x) > - (x0 - r1) by XREAL_1:26;
then A37: (x - x0) + x0 > (r1 - x0) + x0 by XREAL_1:8;
A38: x - x0 < min (x0 - r1),(r2 - x0) by A35, XREAL_1:21;
min (x0 - r1),(r2 - x0) <= r2 - x0 by XXREAL_0:17;
then x - x0 < r2 - x0 by A38, XXREAL_0:2;
then A39: (x - x0) + x0 < (r2 - x0) + x0 by XREAL_1:8;
A40: x in X /\ (dom (f | X)) by A34, RELAT_1:87, XBOOLE_1:28;
r2 in X /\ (dom (f | X)) by A23, XBOOLE_0:def 4;
then A41: (f | X) . x <= (f | X) . r2 by A9, A39, A40, RFUNCT_2:45;
r1 in X /\ (dom (f | X)) by A22, XBOOLE_0:def 4;
then (f | X) . r1 <= (f | X) . x by A9, A37, A40, RFUNCT_2:45;
then (f | X) . x in [.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] by A22, A23, A41;
then (f | X) . x in N3 by A12, A21;
hence (f | X) . x in N1 by A11; :: thesis: verum

end;

suppose A42: (f | X) . x0 = p ; :: thesis: ex N being Neighbourhood of x0 st
for x being real number st x in dom (f | X) & x in N holds
(f | X) . x in N1

then consider r being real number such that
A43: ( r > 0 & N1 = ].(p - r),(p + r).[ ) by RCOMP_1:def 7;
reconsider r = r as Real by XREAL_0:def 1;
set R = r / 2;
A44: 0 < r / 2 by A43, XREAL_1:217;
A45: r / 2 < r by A43, XREAL_1:218;
then A46: p + (r / 2) < p + r by XREAL_1:8;
A47: p - r < p by A43, XREAL_1:46;
A48: p < p + (r / 2) by A44, XREAL_1:31;
then p - r < p + (r / 2) by A47, XXREAL_0:2;
then A49: p + (r / 2) in ].(p - r),(p + r).[ by A46;
A50: p - (r / 2) < p by A44, XREAL_1:46;
p < p + r by A43, XREAL_1:31;
then A51: p - (r / 2) < p + r by A50, XXREAL_0:2;
p - r < p - (r / 2) by A45, XREAL_1:17;
then p - (r / 2) in ].(p - r),(p + r).[ by A51;
then A52: [.(p - (r / 2)),(p + (r / 2)).] c= N1 by A43, A49, XXREAL_2:def 12;
p - (r / 2) in { s where s is Real : s < p } by A50;
then p - (r / 2) in left_open_halfline p by XXREAL_1:229;
then consider r1 being Real such that
A53: ( r1 in dom (f | X) & r1 in X & p - (r / 2) = (f | X) . r1 ) by A2, A6, A8, PARTFUN2:78;
A54: r1 <> x0 by A42, A44, A53, XREAL_1:46;

now

assume A55: x0 < r1 ; :: thesis: contradiction
A56: x0 in X /\ (dom (f | X)) by A3, A4, XBOOLE_0:def 4;
r1 in X /\ (dom (f | X)) by A53, XBOOLE_0:def 4;
hence contradiction by A9, A42, A50, A53, A55, A56, RFUNCT_2:45; :: thesis: verum

end;

then r1 < x0 by A54, XXREAL_0:1;
then x0 - r1 > 0 by XREAL_1:52;
then reconsider N = ].(x0 - (x0 - r1)),(x0 + (x0 - r1)).[ as Neighbourhood of x0 by RCOMP_1:def 7;
take N = N; :: thesis: for x being real number st x in dom (f | X) & x in N holds
(f | X) . x in N1
let x be real number ; :: thesis: ( x in dom (f | X) & x in N implies (f | X) . x in N1 )
assume A57: ( x in dom (f | X) & x in N ) ; :: thesis: (f | X) . x in N1
A58: dom (f | X) c= X by RELAT_1:87;
then (f | X) . x in left_closed_halfline p by A2, A6, A57, FUNCT_1:def 12;
then (f | X) . x in { s where s is Real : s <= p } by XXREAL_1:231;
then ex s being Real st
( s = (f | X) . x & s <= p ) ;
then A59: (f | X) . x <= p + (r / 2) by A48, XXREAL_0:2;
A60: x in X /\ (dom (f | X)) by A57, A58, XBOOLE_0:def 4;
A61: r1 in X /\ (dom (f | X)) by A53, XBOOLE_0:def 4;
ex s being Real st
( s = x & x0 - (x0 - r1) < s & s < x0 + (x0 - r1) ) by A57;
then p - (r / 2) <= (f | X) . x by A9, A53, A60, A61, RFUNCT_2:45;
then (f | X) . x in [.(p - (r / 2)),(p + (r / 2)).] by A59;
hence (f | X) . x in N1 by A52; :: thesis: verum

end;

end;

end;

hence ex N being Neighbourhood of x0 st
for r1 being real number st r1 in dom (f | X) & r1 in N holds
(f | X) . r1 in N1 ; :: thesis: verum

end;

suppose f | X is non-increasing ; :: thesis: ex N being Neighbourhood of x0 st
for r1 being real number st r1 in dom (f | X) & r1 in N holds
(f | X) . r1 in N1

then A62: (f | X) | X is non-increasing by RELAT_1:101;

now

per cases ( (f | X) . x0 in left_open_halfline p or (f | X) . x0 = p ) by A7, TARSKI:def 1;

suppose (f | X) . x0 in left_open_halfline p ; :: thesis: ex N being Neighbourhood of x0 st
for x being real number st x in dom (f | X) & x in N holds
(f | X) . x in N1

then consider N2 being Neighbourhood of (f | X) . x0 such that
A63: N2 c= left_open_halfline p by RCOMP_1:39;
consider N3 being Neighbourhood of (f | X) . x0 such that
A64: ( N3 c= N1 & N3 c= N2 ) by RCOMP_1:38;
consider r being real number such that
A65: ( r > 0 & N3 = ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ ) by RCOMP_1:def 7;
reconsider r = r as Real by XREAL_0:def 1;
set M1 = ((f | X) . x0) - (r / 2);
set M2 = ((f | X) . x0) + (r / 2);
A66: r / 2 > 0 by A65, XREAL_1:217;
then A67: ((f | X) . x0) - r < (((f | X) . x0) - r) + (r / 2) by XREAL_1:31;
A68: (f | X) . x0 < ((f | X) . x0) + (r / 2) by A66, XREAL_1:31;
then A69: ((f | X) . x0) - (r / 2) < (f | X) . x0 by XREAL_1:21;
A70: (f | X) . x0 < ((f | X) . x0) + r by A65, XREAL_1:31;
then ((f | X) . x0) - (r / 2) < ((f | X) . x0) + r by A69, XXREAL_0:2;
then A71: ((f | X) . x0) - (r / 2) in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A67;
A72: ((f | X) . x0) + (r / 2) < (((f | X) . x0) + (r / 2)) + (r / 2) by A66, XREAL_1:31;
((f | X) . x0) - r < (((f | X) . x0) + r) - r by A70, XREAL_1:11;
then ((f | X) . x0) - r < ((f | X) . x0) + (r / 2) by A68, XXREAL_0:2;
then A73: ((f | X) . x0) + (r / 2) in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A72;
then A74: [.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] c= ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A71, XXREAL_2:def 12;
((f | X) . x0) - (r / 2) in N2 by A64, A65, A71;
then ((f | X) . x0) - (r / 2) in left_open_halfline p by A63;
then consider r1 being Real such that
A75: ( r1 in dom (f | X) & r1 in X & ((f | X) . x0) - (r / 2) = (f | X) . r1 ) by A2, A6, A8, PARTFUN2:78;
((f | X) . x0) + (r / 2) in N2 by A64, A65, A73;
then ((f | X) . x0) + (r / 2) in left_open_halfline p by A63;
then consider r2 being Real such that
A76: ( r2 in dom (f | X) & r2 in X & ((f | X) . x0) + (r / 2) = (f | X) . r2 ) by A2, A6, A8, PARTFUN2:78;
set R = min (r1 - x0),(x0 - r2);
A77: (f | X) . x0 < ((f | X) . x0) + (r / 2) by A66, XREAL_1:31;
then A78: ((f | X) . x0) - (r / 2) < (f | X) . x0 by XREAL_1:21;
A79: r1 <> x0 by A75, A77, XREAL_1:21;

now

assume A80: x0 > r1 ; :: thesis: contradiction
A81: x0 in X /\ (dom (f | X)) by A3, A4, XBOOLE_0:def 4;
r1 in X /\ (dom (f | X)) by A75, XBOOLE_0:def 4;
hence contradiction by A62, A75, A78, A80, A81, RFUNCT_2:46; :: thesis: verum

end;

then r1 > x0 by A79, XXREAL_0:1;
then A82: r1 - x0 > 0 by XREAL_1:52;
A83: ((f | X) . x0) + (r / 2) > (f | X) . x0 by A66, XREAL_1:31;
A84: x0 <> r2 by A66, A76, XREAL_1:31;

now

assume A85: r2 > x0 ; :: thesis: contradiction
A86: x0 in X /\ (dom (f | X)) by A3, A4, XBOOLE_0:def 4;
r2 in X /\ (dom (f | X)) by A76, XBOOLE_0:def 4;
hence contradiction by A62, A76, A83, A85, A86, RFUNCT_2:46; :: thesis: verum

end;

then x0 > r2 by A84, XXREAL_0:1;
then x0 - r2 > 0 by XREAL_1:52;
then min (r1 - x0),(x0 - r2) > 0 by A82, XXREAL_0:15;
then reconsider N = ].(x0 - (min (r1 - x0),(x0 - r2))),(x0 + (min (r1 - x0),(x0 - r2))).[ as Neighbourhood of x0 by RCOMP_1:def 7;
take N = N; :: thesis: for x being real number st x in dom (f | X) & x in N holds
(f | X) . x in N1
let x be real number ; :: thesis: ( x in dom (f | X) & x in N implies (f | X) . x in N1 )
assume A87: ( x in dom (f | X) & x in N ) ; :: thesis: (f | X) . x in N1
then A88: ex s being Real st
( s = x & x0 - (min (r1 - x0),(x0 - r2)) < s & s < x0 + (min (r1 - x0),(x0 - r2)) ) ;
then x0 < (min (r1 - x0),(x0 - r2)) + x by XREAL_1:21;
then A89: x0 - x < ((min (r1 - x0),(x0 - r2)) + x) - x by XREAL_1:11;
min (r1 - x0),(x0 - r2) <= x0 - r2 by XXREAL_0:17;
then x0 - x < x0 - r2 by A89, XXREAL_0:2;
then - (x0 - x) > - (x0 - r2) by XREAL_1:26;
then A90: (x - x0) + x0 > (r2 - x0) + x0 by XREAL_1:8;
A91: x - x0 < min (r1 - x0),(x0 - r2) by A88, XREAL_1:21;
min (r1 - x0),(x0 - r2) <= r1 - x0 by XXREAL_0:17;
then x - x0 < r1 - x0 by A91, XXREAL_0:2;
then A92: (x - x0) + x0 < (r1 - x0) + x0 by XREAL_1:8;
A93: x in X /\ (dom (f | X)) by A87, RELAT_1:87, XBOOLE_1:28;
r2 in X /\ (dom (f | X)) by A76, XBOOLE_0:def 4;
then A94: (f | X) . x <= (f | X) . r2 by A62, A90, A93, RFUNCT_2:46;
r1 in X /\ (dom (f | X)) by A75, XBOOLE_0:def 4;
then (f | X) . r1 <= (f | X) . x by A62, A92, A93, RFUNCT_2:46;
then (f | X) . x in [.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] by A75, A76, A94;
then (f | X) . x in N3 by A65, A74;
hence (f | X) . x in N1 by A64; :: thesis: verum

end;

suppose A95: (f | X) . x0 = p ; :: thesis: ex N being Neighbourhood of x0 st
for x being real number st x in dom (f | X) & x in N holds
(f | X) . x in N1

then consider r being real number such that
A96: ( r > 0 & N1 = ].(p - r),(p + r).[ ) by RCOMP_1:def 7;
reconsider r = r as Real by XREAL_0:def 1;
set R = r / 2;
A97: 0 < r / 2 by A96, XREAL_1:217;
A98: r / 2 < r by A96, XREAL_1:218;
then A99: p + (r / 2) < p + r by XREAL_1:8;
A100: p - r < p by A96, XREAL_1:46;
A101: p < p + (r / 2) by A97, XREAL_1:31;
then p - r < p + (r / 2) by A100, XXREAL_0:2;
then A102: p + (r / 2) in ].(p - r),(p + r).[ by A99;
A103: p - (r / 2) < p by A97, XREAL_1:46;
p < p + r by A96, XREAL_1:31;
then A104: p - (r / 2) < p + r by A103, XXREAL_0:2;
p - r < p - (r / 2) by A98, XREAL_1:17;
then p - (r / 2) in ].(p - r),(p + r).[ by A104;
then A105: [.(p - (r / 2)),(p + (r / 2)).] c= N1 by A96, A102, XXREAL_2:def 12;
p - (r / 2) in { s where s is Real : s < p } by A103;
then p - (r / 2) in left_open_halfline p by XXREAL_1:229;
then consider r1 being Real such that
A106: ( r1 in dom (f | X) & r1 in X & p - (r / 2) = (f | X) . r1 ) by A2, A6, A8, PARTFUN2:78;
A107: r1 <> x0 by A95, A97, A106, XREAL_1:46;

now

assume A108: x0 > r1 ; :: thesis: contradiction
A109: x0 in X /\ (dom (f | X)) by A3, A4, XBOOLE_0:def 4;
r1 in X /\ (dom (f | X)) by A106, XBOOLE_0:def 4;
hence contradiction by A62, A95, A103, A106, A108, A109, RFUNCT_2:46; :: thesis: verum

end;

then r1 > x0 by A107, XXREAL_0:1;
then r1 - x0 > 0 by XREAL_1:52;
then reconsider N = ].(x0 - (r1 - x0)),(x0 + (r1 - x0)).[ as Neighbourhood of x0 by RCOMP_1:def 7;
take N = N; :: thesis: for x being real number st x in dom (f | X) & x in N holds
(f | X) . x in N1
let x be real number ; :: thesis: ( x in dom (f | X) & x in N implies (f | X) . x in N1 )
assume A110: ( x in dom (f | X) & x in N ) ; :: thesis: (f | X) . x in N1
A111: dom (f | X) c= X by RELAT_1:87;
then (f | X) . x in left_closed_halfline p by A2, A6, A110, FUNCT_1:def 12;
then (f | X) . x in { s where s is Real : s <= p } by XXREAL_1:231;
then ex s being Real st
( s = (f | X) . x & s <= p ) ;
then A112: (f | X) . x <= p + (r / 2) by A101, XXREAL_0:2;
A113: x in X /\ (dom (f | X)) by A110, A111, XBOOLE_0:def 4;
A114: r1 in X /\ (dom (f | X)) by A106, XBOOLE_0:def 4;
ex s being Real st
( s = x & x0 - (r1 - x0) < s & s < x0 + (r1 - x0) ) by A110;
then p - (r / 2) <= (f | X) . x by A62, A106, A113, A114, RFUNCT_2:46;
then (f | X) . x in [.(p - (r / 2)),(p + (r / 2)).] by A112;
hence (f | X) . x in N1 by A105; :: thesis: verum

end;

end;

end;

hence ex N being Neighbourhood of x0 st
for r1 being real number st r1 in dom (f | X) & r1 in N holds
(f | X) . r1 in N1 ; :: thesis: verum

end;

end;

end;

hence ex N being Neighbourhood of x0 st
for r1 being real number st r1 in dom (f | X) & r1 in N holds
(f | X) . r1 in N1 ; :: thesis: verum

end;

hence f | X is_continuous_in x0 by FCONT_1:4; :: thesis: verum

end;

hence f | X is continuous by FCONT_1:def 2; :: thesis: verum