let p be Real; 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; ( 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
A1:
left_open_halfline p c= dom f
and
A2:
f | (left_open_halfline p) is continuous
and
A3:
( f | (left_open_halfline p) is increasing or f | (left_open_halfline p) is decreasing )
; rng (f | (left_open_halfline p)) is open
now for r1 being Element of REAL st r1 in rng (f | (left_open_halfline p)) holds
ex N being Neighbourhood of r1 st N c= rng (f | (left_open_halfline p))let r1 be
Element of
REAL ;
( r1 in rng (f | (left_open_halfline p)) implies ex N being Neighbourhood of r1 st N c= rng (f | (left_open_halfline p)) )set f1 =
f | (left_open_halfline p);
assume
r1 in rng (f | (left_open_halfline p))
;
ex N being Neighbourhood of r1 st N c= rng (f | (left_open_halfline p))then consider x0 being
Element of
REAL such that A4:
x0 in dom (f | (left_open_halfline p))
and A5:
(f | (left_open_halfline p)) . x0 = r1
by PARTFUN1:3;
A6:
r1 = f . x0
by A4, A5, FUNCT_1:47;
A7:
x0 in (dom f) /\ (left_open_halfline p)
by A4, RELAT_1:61;
then
x0 in left_open_halfline p
by XBOOLE_0:def 4;
then consider N being
Neighbourhood of
x0 such that A8:
N c= left_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 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, XREAL_1: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 (left_open_halfline p) /\ (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 (left_open_halfline p) /\ (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= left_open_halfline p
by A8, A10, A18, A20, XXREAL_2:def 12;
now ex N1 being Neighbourhood of r1 st N1 c= rng (f | (left_open_halfline p))per cases
( f | (left_open_halfline p) is increasing or f | (left_open_halfline p) is decreasing )
by A3;
suppose A25:
f | (left_open_halfline p) is
increasing
;
ex N1 being Neighbourhood of r1 st N1 c= rng (f | (left_open_halfline p))set R =
min (
((f . x0) - (f . (x0 - (r / 2)))),
((f . (x0 + (r / 2))) - (f . x0)));
f . x0 < f . (x0 + (r / 2))
by A7, A16, A21, A25, RFUNCT_2:20;
then A26:
0 < (f . (x0 + (r / 2))) - (f . x0)
by XREAL_1:50;
f . (x0 - (r / 2)) < f . x0
by A7, A11, A19, A25, RFUNCT_2:20;
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 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 6;
take N1 =
N1;
N1 c= rng (f | (left_open_halfline p))
f . (x0 - (r / 2)) < f . (x0 + (r / 2))
by A17, A21, A19, A25, RFUNCT_2:20;
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 | (left_open_halfline p))
verumproof
let x be
object ;
TARSKI:def 3 ( not x in N1 or x in rng (f | (left_open_halfline p)) )
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
;
x in rng (f | (left_open_halfline p))
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 A31, XXREAL_0:2;
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 A30, XXREAL_0:2;
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 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) /\ (left_open_halfline p)
by A8, A14, XBOOLE_0:def 4;
then A35:
s in dom (f | (left_open_halfline p))
by RELAT_1:61;
then
x = (f | (left_open_halfline p)) . s
by A34, FUNCT_1:47;
hence
x in rng (f | (left_open_halfline p))
by A35, FUNCT_1:def 3;
verum
end; end; suppose A36:
f | (left_open_halfline p) is
decreasing
;
ex N1 being Neighbourhood of r1 st N1 c= rng (f | (left_open_halfline p))set R =
min (
((f . (x0 - (r / 2))) - (f . x0)),
((f . x0) - (f . (x0 + (r / 2)))));
f . (x0 + (r / 2)) < f . x0
by A7, A16, A21, A36, RFUNCT_2:21;
then A37:
0 < (f . x0) - (f . (x0 + (r / 2)))
by XREAL_1:50;
f . x0 < f . (x0 - (r / 2))
by A7, A11, A19, A36, RFUNCT_2:21;
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 A37, 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 6;
take N1 =
N1;
N1 c= rng (f | (left_open_halfline p))
f . (x0 + (r / 2)) < f . (x0 - (r / 2))
by A17, A21, A19, A36, RFUNCT_2:21;
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 | (left_open_halfline p))
verumproof
let x be
object ;
TARSKI:def 3 ( not x in N1 or x in rng (f | (left_open_halfline p)) )
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
;
x in rng (f | (left_open_halfline p))
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 A42, XXREAL_0:2;
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 A41, XXREAL_0:2;
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 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) /\ (left_open_halfline p)
by A8, A14, XBOOLE_0:def 4;
then A46:
s in dom (f | (left_open_halfline p))
by RELAT_1:61;
then
x = (f | (left_open_halfline p)) . s
by A45, FUNCT_1:47;
hence
x in rng (f | (left_open_halfline p))
by A46, FUNCT_1:def 3;
verum
end; end; hence
ex
N being
Neighbourhood of
r1 st
N c= rng (f | (left_open_halfline p))
;
verum end;
hence
rng (f | (left_open_halfline p)) is open
by RCOMP_1:20; verum