let p be Real; :: thesis: for f being PartFunc of REAL ,REAL st 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 ) holds
rng (f | (left_open_halfline p)) is open
let f be PartFunc of REAL ,REAL ; :: thesis: ( 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 )
set L = left_open_halfline p;
assume that
A0: left_open_halfline p c= dom f and
A1: f | (left_open_halfline p) is continuous and
A2: ( f | (left_open_halfline p) is increasing or f | (left_open_halfline p) is decreasing ) ; :: thesis: rng (f | (left_open_halfline p)) is open

now

set f1 = f | (left_open_halfline p);
let r1 be real number ; :: thesis: ( r1 in rng (f | (left_open_halfline p)) implies ex N being Neighbourhood of r1 st N c= rng (f | (left_open_halfline p)) )
assume r1 in rng (f | (left_open_halfline p)) ; :: thesis: ex N being Neighbourhood of r1 st N c= rng (f | (left_open_halfline p))
then consider x0 being Real such that
A3: ( x0 in dom (f | (left_open_halfline p)) & (f | (left_open_halfline p)) . x0 = r1 ) by PARTFUN1:26;
A4: x0 in (dom f) /\ (left_open_halfline p) by A3, RELAT_1:90;
then ( x0 in dom f & x0 in left_open_halfline p ) by XBOOLE_0:def 4;
then consider N being Neighbourhood of x0 such that
A5: N c= left_open_halfline p by RCOMP_1:39;
consider r being real number such that
A6: ( 0 < r & N = ].(x0 - r),(x0 + r).[ ) by RCOMP_1:def 7;
reconsider r = r as Real by XREAL_0:def 1;
A7: f | N is continuous by A1, A5, FCONT_1:17;
A8: r / 2 < r by A6, XREAL_1:218;
then A9: x0 - r < x0 - (r / 2) by XREAL_1:17;
A10: 0 < r / 2 by A6, XREAL_1:217;
then A11: x0 - (r / 2) < x0 - 0 by XREAL_1:17;
x0 < x0 + r by A6, XREAL_1:31;
then x0 - (r / 2) < x0 + r by A11, XXREAL_0:2;
then A12: x0 - (r / 2) in ].(x0 - r),(x0 + r).[ by A9;
A13: x0 + (r / 2) < x0 + r by A8, XREAL_1:10;
A14: x0 - r < x0 by A6, XREAL_1:46;
A15: x0 < x0 + (r / 2) by A10, XREAL_1:31;
then x0 - r < x0 + (r / 2) by A14, XXREAL_0:2;
then A16: x0 + (r / 2) in ].(x0 - r),(x0 + r).[ by A13;
then A17: [.(x0 - (r / 2)),(x0 + (r / 2)).] c= ].(x0 - r),(x0 + r).[ by A12, XXREAL_2:def 12;
then [.(x0 - (r / 2)),(x0 + (r / 2)).] c= left_open_halfline p by A5, A6, XBOOLE_1:1;
then X: [.(x0 - (r / 2)),(x0 + (r / 2)).] c= dom f by A0, XBOOLE_1:1;
A18: f | [.(x0 - (r / 2)),(x0 + (r / 2)).] is continuous by A6, A7, A17, FCONT_1:17;
set fm = f . (x0 - (r / 2));
set fp = f . (x0 + (r / 2));
A19: x0 - (r / 2) < x0 + (r / 2) by A11, A15, XXREAL_0:2;
A20: N c= dom f by A0, A5, XBOOLE_1:1;
then A21: x0 + (r / 2) in (left_open_halfline p) /\ (dom f) by A5, A6, A16, XBOOLE_0:def 4;
A22: x0 - (r / 2) in (left_open_halfline p) /\ (dom f) by A5, A6, A12, A20, XBOOLE_0:def 4;
A23: r1 = f . x0 by A3, FUNCT_1:70;

now

per cases ( f | (left_open_halfline p) is increasing or f | (left_open_halfline p) is decreasing ) by A2;

suppose A24: f | (left_open_halfline p) is increasing ; :: thesis: ex N1 being Neighbourhood of r1 st N1 c= rng (f | (left_open_halfline p))

then f . (x0 - (r / 2)) < f . (x0 + (r / 2)) by A19, A21, A22, RFUNCT_2:43;
then [.(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).] = {} by XXREAL_1:29;
then A25: [.(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).] \/ [.(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).] = [.(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).] ;
f . (x0 - (r / 2)) < f . x0 by A4, A11, A22, A24, RFUNCT_2:43;
then A26: 0 < (f . x0) - (f . (x0 - (r / 2))) by XREAL_1:52;
set R = min ((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0));
f . x0 < f . (x0 + (r / 2)) by A4, A15, A21, A24, RFUNCT_2:43;
then 0 < (f . (x0 + (r / 2))) - (f . x0) by XREAL_1:52;
then 0 < min ((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0)) by A26, XXREAL_0:15;
then reconsider N1 = ].(r1 - (min ((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0)))),(r1 + (min ((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0)))).[ as Neighbourhood of r1 by RCOMP_1:def 7;
take N1 = N1; :: thesis: N1 c= rng (f | (left_open_halfline p))
thus N1 c= rng (f | (left_open_halfline p)) :: thesis: verum

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in N1 or x in rng (f | (left_open_halfline p)) )
assume x in N1 ; :: thesis: x in rng (f | (left_open_halfline p))
then consider r2 being Real such that
A27: ( r2 = x & (f . x0) - (min ((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0))) < r2 & r2 < (f . x0) + (min ((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0))) ) by A23;
A28: ( min ((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0)) <= (f . x0) - (f . (x0 - (r / 2))) & min ((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0)) <= (f . (x0 + (r / 2))) - (f . x0) ) by XXREAL_0:17;
then (f . x0) - ((f . x0) - (f . (x0 - (r / 2)))) <= (f . x0) - (min ((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0))) by XREAL_1:15;
then A29: f . (x0 - (r / 2)) < r2 by A27, XXREAL_0:2;
(f . x0) + (min ((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0))) <= (f . x0) + ((f . (x0 + (r / 2))) - (f . x0)) by A28, XREAL_1:9;
then r2 < f . (x0 + (r / 2)) by A27, XXREAL_0:2;
then A30: r2 in ].(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).[ by A29;
].(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).[ c= [.(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).] by XXREAL_1:25;
then consider s being Real such that
A31: ( s in [.(x0 - (r / 2)),(x0 + (r / 2)).] & x = f . s ) by A18, A19, A25, A27, A30, X, FCONT_2:16;
s in N by A6, A17, A31;
then s in (dom f) /\ (left_open_halfline p) by A5, A20, XBOOLE_0:def 4;
then A32: s in dom (f | (left_open_halfline p)) by RELAT_1:90;
then x = (f | (left_open_halfline p)) . s by A31, FUNCT_1:70;
hence x in rng (f | (left_open_halfline p)) by A32, FUNCT_1:def 5; :: thesis: verum

end;

end;

suppose A33: f | (left_open_halfline p) is decreasing ; :: thesis: ex N1 being Neighbourhood of r1 st N1 c= rng (f | (left_open_halfline p))

then f . (x0 + (r / 2)) < f . (x0 - (r / 2)) by A19, A21, A22, RFUNCT_2:44;
then [.(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).] = {} by XXREAL_1:29;
then A34: [.(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).] \/ [.(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).] = [.(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).] ;
f . x0 < f . (x0 - (r / 2)) by A4, A11, A22, A33, RFUNCT_2:44;
then A35: 0 < (f . (x0 - (r / 2))) - (f . x0) by XREAL_1:52;
set R = min ((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2))));
f . (x0 + (r / 2)) < f . x0 by A4, A15, A21, A33, RFUNCT_2:44;
then 0 < (f . x0) - (f . (x0 + (r / 2))) by XREAL_1:52;
then 0 < min ((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2)))) by A35, XXREAL_0:15;
then reconsider N1 = ].(r1 - (min ((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2)))))),(r1 + (min ((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2)))))).[ as Neighbourhood of r1 by RCOMP_1:def 7;
take N1 = N1; :: thesis: N1 c= rng (f | (left_open_halfline p))
thus N1 c= rng (f | (left_open_halfline p)) :: thesis: verum

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in N1 or x in rng (f | (left_open_halfline p)) )
assume x in N1 ; :: thesis: x in rng (f | (left_open_halfline p))
then consider r2 being Real such that
A36: ( r2 = x & (f . x0) - (min ((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2))))) < r2 & r2 < (f . x0) + (min ((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2))))) ) by A23;
A37: ( min ((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2)))) <= (f . (x0 - (r / 2))) - (f . x0) & min ((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2)))) <= (f . x0) - (f . (x0 + (r / 2))) ) by XXREAL_0:17;
then (f . x0) - ((f . x0) - (f . (x0 + (r / 2)))) <= (f . x0) - (min ((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2))))) by XREAL_1:15;
then A38: f . (x0 + (r / 2)) < r2 by A36, XXREAL_0:2;
(f . x0) + (min ((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2))))) <= (f . x0) + ((f . (x0 - (r / 2))) - (f . x0)) by A37, XREAL_1:9;
then r2 < f . (x0 - (r / 2)) by A36, XXREAL_0:2;
then A39: r2 in ].(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).[ by A38;
].(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).[ c= [.(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).] by XXREAL_1:25;
then consider s being Real such that
A40: ( s in [.(x0 - (r / 2)),(x0 + (r / 2)).] & x = f . s ) by A18, A19, A34, A36, A39, X, FCONT_2:16;
s in N by A6, A17, A40;
then s in (dom f) /\ (left_open_halfline p) by A5, A20, XBOOLE_0:def 4;
then A41: s in dom (f | (left_open_halfline p)) by RELAT_1:90;
then x = (f | (left_open_halfline p)) . s by A40, FUNCT_1:70;
hence x in rng (f | (left_open_halfline p)) by A41, FUNCT_1:def 5; :: thesis: verum

end;

end;

end;

end;

hence ex N being Neighbourhood of r1 st N c= rng (f | (left_open_halfline p)) ; :: thesis: verum

end;

hence rng (f | (left_open_halfline p)) is open by RCOMP_1:41; :: thesis: verum