let f be PartFunc of REAL ,REAL ; :: thesis: ( [#] REAL c= dom f & f | ([#] REAL ) is continuous & ( f | ([#] REAL ) is increasing or f | ([#] REAL ) is decreasing ) implies rng f is open )
set L = [#] REAL ;
assume that
A0:
[#] REAL c= dom f
and
A1:
f | ([#] REAL ) is continuous
and
A2:
( f | ([#] REAL ) is increasing or f | ([#] REAL ) is decreasing )
; :: thesis: rng f is open
now let r1 be
real number ;
:: thesis: ( r1 in rng f implies ex N being Neighbourhood of r1 st N c= rng f )assume
r1 in rng f
;
:: thesis: ex N being Neighbourhood of r1 st N c= rng fthen consider x0 being
Real such that A3:
(
x0 in dom f &
f . x0 = r1 )
by PARTFUN1:26;
consider N being
Neighbourhood of
x0;
consider r being
real number such that A4:
(
0 < r &
N = ].(x0 - r),(x0 + r).[ )
by RCOMP_1:def 7;
reconsider r =
r as
Real by XREAL_0:def 1;
A6:
r / 2
< r
by A4, XREAL_1:218;
then A7:
x0 - r < x0 - (r / 2)
by XREAL_1:17;
A8:
0 < r / 2
by A4, XREAL_1:217;
then A9:
x0 - (r / 2) < x0 - 0
by XREAL_1:17;
x0 < x0 + r
by A4, XREAL_1:31;
then
x0 - (r / 2) < x0 + r
by A9, XXREAL_0:2;
then A10:
x0 - (r / 2) in ].(x0 - r),(x0 + r).[
by A7;
A11:
x0 + (r / 2) < x0 + r
by A6, XREAL_1:10;
A12:
x0 - r < x0
by A4, XREAL_1:46;
A13:
x0 < x0 + (r / 2)
by A8, XREAL_1:31;
then
x0 - r < x0 + (r / 2)
by A12, XXREAL_0:2;
then A14:
x0 + (r / 2) in ].(x0 - r),(x0 + r).[
by A11;
then A15:
[.(x0 - (r / 2)),(x0 + (r / 2)).] c= ].(x0 - r),(x0 + r).[
by A10, XXREAL_2:def 12;
A16:
f | [.(x0 - (r / 2)),(x0 + (r / 2)).] is
continuous
by A1, FCONT_1:17;
set fm =
f . (x0 - (r / 2));
set fp =
f . (x0 + (r / 2));
A17:
x0 - (r / 2) < x0 + (r / 2)
by A9, A13, XXREAL_0:2;
A18:
N c= dom f
by A0, XBOOLE_1:1;
then A19:
x0 + (r / 2) in ([#] REAL ) /\ (dom f)
by A4, A14, XBOOLE_0:def 4;
A20:
x0 - (r / 2) in ([#] REAL ) /\ (dom f)
by A4, A10, A18, XBOOLE_0:def 4;
A21:
x0 in ([#] REAL ) /\ (dom f)
by A3, XBOOLE_0:def 4;
now per cases
( f | ([#] REAL ) is increasing or f | ([#] REAL ) is decreasing )
by A2;
suppose A22:
f | ([#] REAL ) is
increasing
;
:: thesis: ex N1 being Neighbourhood of r1 st N1 c= rng fthen
f . (x0 - (r / 2)) < f . (x0 + (r / 2))
by A17, A19, A20, RFUNCT_2:43;
then
[.(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).] = {}
by XXREAL_1:29;
then A23:
[.(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 A9, A20, A21, A22, RFUNCT_2:43;
then A24:
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 A13, A19, A21, A22, 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 A24, 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 fthus
N1 c= rng f
:: thesis: verumproof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in N1 or x in rng f )
assume
x in N1
;
:: thesis: x in rng f
then consider r2 being
Real such that A25:
(
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 A3;
A26:
(
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 A27:
f . (x0 - (r / 2)) < r2
by A25, 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 A26, XREAL_1:9;
then
r2 < f . (x0 + (r / 2))
by A25, XXREAL_0:2;
then A28:
r2 in ].(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).[
by A27;
].(x0 - r),(x0 + r).[ c= dom f
by A0, XBOOLE_1:1;
then X:
[.(x0 - (r / 2)),(x0 + (r / 2)).] c= dom f
by A15, XBOOLE_1:1;
].(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 A29:
(
s in [.(x0 - (r / 2)),(x0 + (r / 2)).] &
x = f . s )
by A16, A17, A23, A25, A28, X, FCONT_2:16;
s in N
by A4, A15, A29;
hence
x in rng f
by A18, A29, FUNCT_1:def 5;
:: thesis: verum
end; end; suppose A30:
f | ([#] REAL ) is
decreasing
;
:: thesis: ex N1 being Neighbourhood of r1 st N1 c= rng fthen
f . (x0 + (r / 2)) < f . (x0 - (r / 2))
by A17, A19, A20, RFUNCT_2:44;
then
[.(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).] = {}
by XXREAL_1:29;
then A31:
[.(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 A9, A20, A21, A30, RFUNCT_2:44;
then A32:
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 A13, A19, A21, A30, 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 A32, 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 fthus
N1 c= rng f
:: thesis: verumproof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in N1 or x in rng f )
assume
x in N1
;
:: thesis: x in rng f
then consider r2 being
Real such that A33:
(
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 A3;
A34:
(
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 A35:
f . (x0 + (r / 2)) < r2
by A33, 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 A34, XREAL_1:9;
then
r2 < f . (x0 - (r / 2))
by A33, XXREAL_0:2;
then A36:
r2 in ].(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).[
by A35;
X:
[.(x0 - (r / 2)),(x0 + (r / 2)).] c= dom f
by A0, XBOOLE_1:1;
].(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 A37:
(
s in [.(x0 - (r / 2)),(x0 + (r / 2)).] &
x = f . s )
by A16, A17, A31, A33, A36, X, FCONT_2:16;
s in N
by A4, A15, A37;
hence
x in rng f
by A18, A37, FUNCT_1:def 5;
:: thesis: verum
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:41; :: thesis: verum