let X be set ; :: thesis: for f being PartFunc of REAL,REAL st X c= dom f & f | X is monotone & ex p, g being Real st f .: X = ].p,g.[ holds
f | X is continuous
let f be PartFunc of REAL,REAL; :: thesis: ( X c= dom f & f | X is monotone & ex p, g being Real st f .: X = ].p,g.[ implies f | X is continuous )
assume that
A1: X c= dom f and
A2: f | X is monotone ; :: thesis: ( for p, g being Real holds not f .: X = ].p,g.[ or f | X is continuous )
given p, g being Real such that A3: f .: X = ].p,g.[ ; :: thesis: f | X is continuous
set L = ].p,g.[;
now :: thesis: f | X is continuous
per cases ( f | X is non-decreasing or f | X is non-increasing ) by A2, RFUNCT_2:def 5;
suppose f | X is non-decreasing ; :: thesis: f | X is continuous
then A4: (f | X) | X is non-decreasing ;
for x0 being Real st x0 in dom (f | X) holds
f | X is_continuous_in x0
proof
let x0 be Real; :: thesis: ( x0 in dom (f | X) implies f | X is_continuous_in x0 )
A5: (f | X) .: X = f .: X by RELAT_1:129;
assume x0 in dom (f | X) ; :: thesis: f | X is_continuous_in x0
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 ].p,g.[ by A3, RELAT_1:129;
now :: thesis: for N1 being Neighbourhood of (f | X) . x0 ex N being Neighbourhood of x0 st
for x being Real st x in dom (f | X) & x in N holds
(f | X) . x in N1
let N1 be Neighbourhood of (f | X) . x0; :: thesis: ex N being Neighbourhood of x0 st
for x being Real st x in dom (f | X) & x in N holds
(f | X) . x in N1
consider N2 being Neighbourhood of (f | X) . x0 such that
A8: N2 c= ].p,g.[ 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 being Real such that
A11: r > 0 and
A12: N3 = ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by RCOMP_1:def 6;
reconsider r = r as Real ;
A13: ((f | X) . x0) + (r / 2) < (((f | X) . x0) + (r / 2)) + (r / 2) by A11, XREAL_1:29, XREAL_1:215;
set M2 = ((f | X) . x0) + (r / 2);
A14: (f | X) . x0 < ((f | X) . x0) + (r / 2) by A11, XREAL_1:29, XREAL_1: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: ((f | X) . x0) + (r / 2) in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A13;
then ((f | X) . x0) + (r / 2) 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: ((f | X) . x0) + (r / 2) = (f | X) . r2 by A3, A5, A8, PARTFUN2:59;
A19: ((f | X) . x0) + (r / 2) > (f | X) . x0 by A11, XREAL_1:29, XREAL_1:215;
A20: now :: thesis: not r2 < x0
assume A21: r2 < x0 ; :: thesis: contradiction
( 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; :: thesis: verum
end;
set M1 = ((f | X) . x0) - (r / 2);
A22: ((f | X) . x0) - r < (((f | X) . x0) - r) + (r / 2) by A11, XREAL_1:29, XREAL_1: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: ((f | X) . x0) - (r / 2) in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A22;
then ((f | X) . x0) - (r / 2) 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: ((f | X) . x0) - (r / 2) = (f | X) . r1 by A3, A5, A8, PARTFUN2:59;
A26: (f | X) . x0 < ((f | X) . x0) + (r / 2) by A11, XREAL_1:29, XREAL_1:215;
then A27: ((f | X) . x0) - (r / 2) < (f | X) . x0 by XREAL_1:19;
A28: now :: thesis: not x0 < r1
assume A29: x0 < r1 ; :: thesis: contradiction
( 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; :: thesis: verum
end;
x0 <> r2 by A11, A18, XREAL_1:29, XREAL_1: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: min ((x0 - r1),(r2 - x0)) <= 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 min ((x0 - r1),(r2 - x0)) > 0 by A30, 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 6;
take N = N; :: thesis: for x being Real st x in dom (f | X) & x in N holds
(f | X) . x in N1
let x be Real; :: thesis: ( x in dom (f | X) & x in N implies (f | X) . x in N1 )
assume that
A32: x in dom (f | X) and
A33: x in N ; :: thesis: (f | X) . x in N1
A34: x in X /\ (dom (f | X)) by A32, XBOOLE_1:28;
A35: ex s being Real st
( s = x & x0 - (min ((x0 - r1),(r2 - x0))) < s & s < x0 + (min ((x0 - r1),(r2 - x0))) ) by A33;
then x0 < (min ((x0 - r1),(r2 - x0))) + x by XREAL_1:19;
then A36: x0 - x < ((min ((x0 - r1),(r2 - x0))) + x) - x by XREAL_1:9;
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: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 < min ((x0 - r1),(r2 - x0)) 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 [.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] by A25, A18, A38;
[.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] 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; :: 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
end;
suppose f | X is non-increasing ; :: thesis: f | X is continuous
then A41: (f | X) | X is non-increasing ;
for x0 being Real st x0 in dom (f | X) holds
f | X is_continuous_in x0
proof
let x0 be Real; :: thesis: ( x0 in dom (f | X) implies f | X is_continuous_in x0 )
A42: (f | X) .: X = f .: X by RELAT_1:129;
assume x0 in dom (f | X) ; :: thesis: f | X is_continuous_in x0
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 ].p,g.[ by A3, RELAT_1:129;
now :: thesis: for N1 being Neighbourhood of (f | X) . x0 ex N being Neighbourhood of x0 st
for x being Real st x in dom (f | X) & x in N holds
(f | X) . x in N1
let N1 be Neighbourhood of (f | X) . x0; :: thesis: ex N being Neighbourhood of x0 st
for x being Real st x in dom (f | X) & x in N holds
(f | X) . x in N1
consider N2 being Neighbourhood of (f | X) . x0 such that
A45: N2 c= ].p,g.[ 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 being Real such that
A48: r > 0 and
A49: N3 = ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by RCOMP_1:def 6;
reconsider r = r as Real ;
A50: ((f | X) . x0) + (r / 2) < (((f | X) . x0) + (r / 2)) + (r / 2) by A48, XREAL_1:29, XREAL_1:215;
set M2 = ((f | X) . x0) + (r / 2);
A51: (f | X) . x0 < ((f | X) . x0) + (r / 2) by A48, XREAL_1:29, XREAL_1: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: ((f | X) . x0) + (r / 2) in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A50;
then ((f | X) . x0) + (r / 2) 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: ((f | X) . x0) + (r / 2) = (f | X) . r2 by A3, A42, A45, PARTFUN2:59;
A56: ((f | X) . x0) + (r / 2) > (f | X) . x0 by A48, XREAL_1:29, XREAL_1:215;
A57: now :: thesis: not r2 > x0
assume A58: r2 > x0 ; :: thesis: contradiction
( 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; :: thesis: verum
end;
set M1 = ((f | X) . x0) - (r / 2);
A59: ((f | X) . x0) - r < (((f | X) . x0) - r) + (r / 2) by A48, XREAL_1:29, XREAL_1: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: ((f | X) . x0) - (r / 2) in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A59;
then ((f | X) . x0) - (r / 2) 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: ((f | X) . x0) - (r / 2) = (f | X) . r1 by A3, A42, A45, PARTFUN2:59;
A63: (f | X) . x0 < ((f | X) . x0) + (r / 2) by A48, XREAL_1:29, XREAL_1:215;
then A64: ((f | X) . x0) - (r / 2) < (f | X) . x0 by XREAL_1:19;
A65: now :: thesis: not x0 > r1
assume A66: x0 > r1 ; :: thesis: contradiction
( 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; :: thesis: verum
end;
x0 <> r2 by A48, A55, XREAL_1:29, XREAL_1: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: min ((r1 - x0),(x0 - r2)) <= 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 min ((r1 - x0),(x0 - r2)) > 0 by A67, 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 6;
take N = N; :: thesis: for x being Real st x in dom (f | X) & x in N holds
(f | X) . x in N1
let x be Real; :: thesis: ( x in dom (f | X) & x in N implies (f | X) . x in N1 )
assume that
A69: x in dom (f | X) and
A70: x in N ; :: thesis: (f | X) . x in N1
A71: x in X /\ (dom (f | X)) by A69, XBOOLE_1:28;
A72: ex s being Real st
( s = x & x0 - (min ((r1 - x0),(x0 - r2))) < s & s < x0 + (min ((r1 - x0),(x0 - r2))) ) by A70;
then x0 < (min ((r1 - x0),(x0 - r2))) + x by XREAL_1:19;
then A73: x0 - x < ((min ((r1 - x0),(x0 - r2))) + x) - x by XREAL_1:9;
x - x0 < min ((r1 - x0),(x0 - r2)) 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;
min ((r1 - x0),(x0 - r2)) <= 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 [.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] by A62, A55, A75;
[.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] 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; :: 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
end;
end;
end;
hence f | X is continuous ; :: thesis: verum