let p be Real; :: thesis: for f being PartFunc of REAL,REAL st right_open_halfline p c= dom f & f | is continuous & ( f | is increasing or f | is decreasing ) holds
rng (f | ) is open

let f be PartFunc of REAL,REAL; :: thesis: ( right_open_halfline p c= dom f & f | is continuous & ( f | is increasing or f | is decreasing ) implies rng (f | ) is open )
set L = right_open_halfline p;
assume that
A1: right_open_halfline p c= dom f and
A2: f | is continuous and
A3: ( f | is increasing or f | is decreasing ) ; :: thesis: rng (f | ) is open
now :: thesis: for r1 being Element of REAL st r1 in rng (f | ) holds
ex N being Neighbourhood of r1 st N c= rng (f | )
let r1 be Element of REAL ; :: thesis: ( r1 in rng (f | ) implies ex N being Neighbourhood of r1 st N c= rng (f | ) )
set f1 = f | ;
assume r1 in rng (f | ) ; :: thesis: ex N being Neighbourhood of r1 st N c= 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: r1 = f . x0 by ;
A7: x0 in (dom f) /\ by ;
then x0 in right_open_halfline p by XBOOLE_0:def 4;
then consider N being Neighbourhood of x0 such that
A8: N c= right_open_halfline p by RCOMP_1:18;
consider r being Real such that
A9: 0 < r and
A10: N = ].(x0 - r),(x0 + r).[ by RCOMP_1:def 6;
reconsider r = r as Element of REAL by XREAL_0:def 1;
0 < r / 2 by ;
then A11: x0 - (r / 2) < x0 - 0 by XREAL_1:15;
A12: r / 2 < r by ;
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 ;
A16: x0 < x0 + (r / 2) by ;
then A17: x0 - (r / 2) < x0 + (r / 2) by ;
x0 < x0 + r by ;
then x0 - (r / 2) < x0 + r by ;
then A18: x0 - (r / 2) in ].(x0 - r),(x0 + r).[ by A13;
then A19: x0 - (r / 2) in /\ (dom f) by ;
x0 - r < x0 by ;
then x0 - r < x0 + (r / 2) by ;
then A20: x0 + (r / 2) in ].(x0 - r),(x0 + r).[ by A15;
then A21: x0 + (r / 2) in /\ (dom f) by ;
A22: [.(x0 - (r / 2)),(x0 + (r / 2)).] c= ].(x0 - r),(x0 + r).[ by ;
f | N is continuous by ;
then A23: f | [.(x0 - (r / 2)),(x0 + (r / 2)).] is continuous by ;
A24: [.(x0 - (r / 2)),(x0 + (r / 2)).] c= right_open_halfline p by ;
now :: thesis: ex N1 being Neighbourhood of r1 st N1 c= rng (f | )
per cases ( f | is increasing or f | is decreasing ) by A3;
suppose A25: f | is increasing ; :: thesis: ex N1 being Neighbourhood of r1 st N1 c= rng (f | )
set R = min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0)));
f . x0 < f . (x0 + (r / 2)) by ;
then A26: 0 < (f . (x0 + (r / 2))) - (f . x0) by XREAL_1:50;
f . (x0 - (r / 2)) < f . x0 by ;
then 0 < (f . x0) - (f . (x0 - (r / 2))) by XREAL_1:50;
then 0 < min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0))) by ;
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 6;
take N1 = N1; :: thesis: N1 c= rng (f | )
f . (x0 - (r / 2)) < f . (x0 + (r / 2)) by ;
then [.(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).] = {} by XXREAL_1:29;
then A27: [.(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).] \/ [.(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).] = [.(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).] ;
thus N1 c= rng (f | ) :: thesis: verum
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in N1 or x in rng (f | ) )
A28: ].(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).[ c= [.(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).] by XXREAL_1:25;
assume x in N1 ; :: thesis: x in rng (f | )
then consider r2 being Real such that
A29: r2 = x and
A30: (f . x0) - (min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0)))) < r2 and
A31: r2 < (f . x0) + (min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0)))) by A6;
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) + (min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0)))) <= (f . x0) + ((f . (x0 + (r / 2))) - (f . x0)) by XREAL_1:7;
then A32: r2 < f . (x0 + (r / 2)) by ;
min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0))) <= (f . x0) - (f . (x0 - (r / 2))) 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:13;
then f . (x0 - (r / 2)) < r2 by ;
then r2 in ].(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).[ by A32;
then consider s being Real such that
A33: s in [.(x0 - (r / 2)),(x0 + (r / 2)).] and
A34: x = f . s by ;
s in N by ;
then s in (dom f) /\ by ;
then A35: s in dom (f | ) by RELAT_1:61;
then x = (f | ) . s by ;
hence x in rng (f | ) by ; :: thesis: verum
end;
end;
suppose A36: f | is decreasing ; :: thesis: ex N1 being Neighbourhood of r1 st N1 c= rng (f | )
set R = min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2)))));
f . (x0 + (r / 2)) < f . x0 by ;
then A37: 0 < (f . x0) - (f . (x0 + (r / 2))) by XREAL_1:50;
f . x0 < f . (x0 - (r / 2)) by ;
then 0 < (f . (x0 - (r / 2))) - (f . x0) by XREAL_1:50;
then 0 < min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2))))) by ;
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 6;
take N1 = N1; :: thesis: N1 c= rng (f | )
f . (x0 + (r / 2)) < f . (x0 - (r / 2)) by ;
then [.(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).] = {} by XXREAL_1:29;
then A38: [.(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).] \/ [.(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).] = [.(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).] ;
thus N1 c= rng (f | ) :: thesis: verum
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in N1 or x in rng (f | ) )
A39: ].(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).[ c= [.(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).] by XXREAL_1:25;
assume x in N1 ; :: thesis: x in rng (f | )
then consider r2 being Real such that
A40: r2 = x and
A41: (f . x0) - (min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2)))))) < r2 and
A42: r2 < (f . x0) + (min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2)))))) by A6;
min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2))))) <= (f . (x0 - (r / 2))) - (f . x0) by XXREAL_0:17;
then (f . x0) + (min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2)))))) <= (f . x0) + ((f . (x0 - (r / 2))) - (f . x0)) by XREAL_1:7;
then A43: r2 < f . (x0 - (r / 2)) by ;
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:13;
then f . (x0 + (r / 2)) < r2 by ;
then r2 in ].(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).[ by A43;
then consider s being Real such that
A44: s in [.(x0 - (r / 2)),(x0 + (r / 2)).] and
A45: x = f . s by ;
s in N by ;
then s in (dom f) /\ by ;
then A46: s in dom (f | ) by RELAT_1:61;
then x = (f | ) . s by ;
hence x in rng (f | ) by ; :: thesis: verum
end;
end;
end;
end;
hence ex N being Neighbourhood of r1 st N c= rng (f | ) ; :: thesis: verum
end;
hence rng (f | ) is open by RCOMP_1:20; :: thesis: verum