let X be non empty MetrSpace; :: thesis: for f being Function of I[01] ,(TopSpaceMetr X)
for F1, F2 being Subset of (TopSpaceMetr X)
for r1, r2 being Real st 0 <= r1 & r2 <= 1 & r1 <= r2 & f . r1 in F1 & f . r2 in F2 & F1 is closed & F2 is closed & f is continuous & F1 \/ F2 = the carrier of X holds
ex r being Real st
( r1 <= r & r <= r2 & f . r in F1 /\ F2 )
let f be Function of I[01] ,(TopSpaceMetr X); :: thesis: for F1, F2 being Subset of (TopSpaceMetr X)
for r1, r2 being Real st 0 <= r1 & r2 <= 1 & r1 <= r2 & f . r1 in F1 & f . r2 in F2 & F1 is closed & F2 is closed & f is continuous & F1 \/ F2 = the carrier of X holds
ex r being Real st
( r1 <= r & r <= r2 & f . r in F1 /\ F2 )
let F1, F2 be Subset of (TopSpaceMetr X); :: thesis: for r1, r2 being Real st 0 <= r1 & r2 <= 1 & r1 <= r2 & f . r1 in F1 & f . r2 in F2 & F1 is closed & F2 is closed & f is continuous & F1 \/ F2 = the carrier of X holds
ex r being Real st
( r1 <= r & r <= r2 & f . r in F1 /\ F2 )
let r1, r2 be Real; :: thesis: ( 0 <= r1 & r2 <= 1 & r1 <= r2 & f . r1 in F1 & f . r2 in F2 & F1 is closed & F2 is closed & f is continuous & F1 \/ F2 = the carrier of X implies ex r being Real st
( r1 <= r & r <= r2 & f . r in F1 /\ F2 ) )
assume that
A1:
0 <= r1
and
A2:
r2 <= 1
and
A3:
r1 <= r2
and
A4:
f . r1 in F1
and
A5:
f . r2 in F2
and
A6:
F1 is closed
and
A7:
F2 is closed
and
A8:
f is continuous
and
A9:
F1 \/ F2 = the carrier of X
; :: thesis: ex r being Real st
( r1 <= r & r <= r2 & f . r in F1 /\ F2 )
A10:
r1 in { r3 where r3 is Real : ( r1 <= r3 & r3 <= r2 & f . r3 in F1 ) }
by A3, A4;
{ r3 where r3 is Real : ( r1 <= r3 & r3 <= r2 & f . r3 in F1 ) } c= REAL
then reconsider R = { r3 where r3 is Real : ( r1 <= r3 & r3 <= r2 & f . r3 in F1 ) } as non empty Subset of REAL by A10;
A12:
{ r3 where r3 is Real : ( r1 <= r3 & r3 <= r2 & f . r3 in F1 ) } c= [.0 ,1.]
A14:
for r being real number st r in R holds
r <= r2
then A16:
R is bounded_above
by SEQ_4:def 1;
A17:
r2 >= upper_bound R
by A14, Th1;
A18:
r1 <= upper_bound R
by A10, A16, SEQ_4:def 4;
A19:
0 <= upper_bound R
by A1, A10, A16, SEQ_4:def 4;
A20:
r2 in { r3 where r3 is Real : ( upper_bound R <= r3 & r3 <= r2 & f . r3 in F2 ) }
by A5, A17;
{ r3 where r3 is Real : ( upper_bound R <= r3 & r3 <= r2 & f . r3 in F2 ) } c= REAL
then reconsider R2 = { r3 where r3 is Real : ( upper_bound R <= r3 & r3 <= r2 & f . r3 in F2 ) } as non empty Subset of REAL by A20;
A22:
{ r3 where r3 is Real : ( upper_bound R <= r3 & r3 <= r2 & f . r3 in F2 ) } c= [.0 ,1.]
A24:
for r being real number st r in R2 holds
r >= upper_bound R
then A26:
R2 is bounded_below
by SEQ_4:def 2;
for s being real number st 0 < s holds
ex r being real number st
( r in R2 & r < (upper_bound R) + s )
proof
let s be
real number ;
:: thesis: ( 0 < s implies ex r being real number st
( r in R2 & r < (upper_bound R) + s ) )
assume A27:
0 < s
;
:: thesis: ex r being real number st
( r in R2 & r < (upper_bound R) + s )
now assume A28:
for
r being
real number st
r < (upper_bound R) + s holds
not
r in R2
;
:: thesis: contradictionnow per cases
( r2 - (upper_bound R) = 0 or r2 - (upper_bound R) > 0 )
by A17, XREAL_1:50;
case A29:
r2 - (upper_bound R) > 0
;
:: thesis: contradictionset rs0 =
min (r2 - (upper_bound R)),
s;
A30:
min (r2 - (upper_bound R)),
s > 0
by A27, A29, XXREAL_0:21;
then A31:
(min (r2 - (upper_bound R)),s) / 2
> 0
by XREAL_1:217;
set r0 =
(upper_bound R) + ((min (r2 - (upper_bound R)),s) / 2);
A32:
upper_bound R < (upper_bound R) + ((min (r2 - (upper_bound R)),s) / 2)
by A31, XREAL_1:31;
A33:
min (r2 - (upper_bound R)),
s <= s
by XXREAL_0:17;
A34:
(min (r2 - (upper_bound R)),s) / 2
< min (r2 - (upper_bound R)),
s
by A30, XREAL_1:218;
then
(min (r2 - (upper_bound R)),s) / 2
< s
by A33, XXREAL_0:2;
then
(upper_bound R) + ((min (r2 - (upper_bound R)),s) / 2) < (upper_bound R) + s
by XREAL_1:10;
then A35:
not
(upper_bound R) + ((min (r2 - (upper_bound R)),s) / 2) in R2
by A28;
A36:
upper_bound R <= (upper_bound R) + ((min (r2 - (upper_bound R)),s) / 2)
by A31, XREAL_1:31;
A37:
(upper_bound R) + ((min (r2 - (upper_bound R)),s) / 2) < (upper_bound R) + (min (r2 - (upper_bound R)),s)
by A34, XREAL_1:10;
min (r2 - (upper_bound R)),
s <= r2 - (upper_bound R)
by XXREAL_0:17;
then
(upper_bound R) + (min (r2 - (upper_bound R)),s) <= (upper_bound R) + (r2 - (upper_bound R))
by XREAL_1:9;
then A38:
(
r1 <= (upper_bound R) + ((min (r2 - (upper_bound R)),s) / 2) &
(upper_bound R) + ((min (r2 - (upper_bound R)),s) / 2) <= r2 )
by A18, A36, A37, XXREAL_0:2;
then
(upper_bound R) + ((min (r2 - (upper_bound R)),s) / 2) <= 1
by A2, XXREAL_0:2;
then
(upper_bound R) + ((min (r2 - (upper_bound R)),s) / 2) in the
carrier of
I[01]
by A1, A18, A36, BORSUK_1:83, XXREAL_1:1;
then
(upper_bound R) + ((min (r2 - (upper_bound R)),s) / 2) in dom f
by FUNCT_2:def 1;
then
f . ((upper_bound R) + ((min (r2 - (upper_bound R)),s) / 2)) in rng f
by FUNCT_1:def 5;
then
f . ((upper_bound R) + ((min (r2 - (upper_bound R)),s) / 2)) in the
carrier of
(TopSpaceMetr X)
;
then
f . ((upper_bound R) + ((min (r2 - (upper_bound R)),s) / 2)) in the
carrier of
X
by TOPMETR:16;
then
(
f . ((upper_bound R) + ((min (r2 - (upper_bound R)),s) / 2)) in F1 or
f . ((upper_bound R) + ((min (r2 - (upper_bound R)),s) / 2)) in F2 )
by A9, XBOOLE_0:def 3;
then A39:
(upper_bound R) + ((min (r2 - (upper_bound R)),s) / 2) in R
by A32, A35, A38;
upper_bound R < (upper_bound R) + ((min (r2 - (upper_bound R)),s) / 2)
by A31, XREAL_1:31;
hence
contradiction
by A16, A39, SEQ_4:def 4;
:: thesis: verum end; hence
contradiction
;
:: thesis: verum end;
hence
ex
r being
real number st
(
r in R2 &
r < (upper_bound R) + s )
;
:: thesis: verum
end;
then A40:
upper_bound R = lower_bound R2
by A24, A26, SEQ_4:def 5;
consider s1 being Real_Sequence such that
A41:
( s1 is non-decreasing & s1 is convergent & rng s1 c= R & lim s1 = upper_bound R )
by A16, Th15;
reconsider S2 = s1 as sequence of RealSpace by METRIC_1:def 14;
reconsider S1 = s1 as sequence of (Closed-Interval-MSpace 0 ,1) by A12, A41, Th7, XBOOLE_1:1;
A42:
S1 is convergent
by A41, Th10;
then
S2 is convergent
by Th9;
then
lim S2 = lim S1
by Th9;
then A43:
lim s1 = lim S1
by A41, Th6;
A44:
I[01] = TopSpaceMetr (Closed-Interval-MSpace 0 ,1)
by TOPMETR:27, TOPMETR:def 8;
then reconsider S00 = f * S1 as sequence of X by Th3;
A45:
S00 is convergent
by A8, A42, A44, Th4;
for n4 being Element of NAT holds S00 . n4 in F1
then A48:
lim S00 in F1
by A6, A45, Th2;
dom f =
the carrier of I[01]
by FUNCT_2:def 1
.=
the carrier of (Closed-Interval-MSpace 0 ,1)
by A44, TOPMETR:16
;
then
f . (lim S1) in rng f
by FUNCT_1:12;
then reconsider t1 = f . (lim S1) as Point of X by TOPMETR:16;
for r being Real st r > 0 holds
ex n being Element of NAT st
for m being Element of NAT st m >= n holds
dist (S00 . m),t1 < r
proof
let r be
Real;
:: thesis: ( r > 0 implies ex n being Element of NAT st
for m being Element of NAT st m >= n holds
dist (S00 . m),t1 < r )
assume
r > 0
;
:: thesis: ex n being Element of NAT st
for m being Element of NAT st m >= n holds
dist (S00 . m),t1 < r
then consider r7 being
Real such that A49:
(
r7 > 0 & ( for
w being
Point of
(Closed-Interval-MSpace 0 ,1) for
w1 being
Point of
X st
w1 = f . w &
dist (lim S1),
w < r7 holds
dist t1,
w1 < r ) )
by A8, A44, UNIFORM1:5;
consider n0 being
Element of
NAT such that A50:
for
m being
Element of
NAT st
m >= n0 holds
dist (S1 . m),
(lim S1) < r7
by A42, A49, TBSP_1:def 4;
for
m being
Element of
NAT st
m >= n0 holds
dist (S00 . m),
t1 < r
hence
ex
n being
Element of
NAT st
for
m being
Element of
NAT st
m >= n holds
dist (S00 . m),
t1 < r
;
:: thesis: verum
end;
then A52:
f . (lim s1) in F1
by A43, A45, A48, TBSP_1:def 4;
consider s2 being Real_Sequence such that
A53:
( s2 is non-increasing & s2 is convergent & rng s2 c= R2 & lim s2 = lower_bound R2 )
by A26, Th16;
reconsider S2 = s2 as sequence of RealSpace by METRIC_1:def 14;
reconsider S1 = s2 as sequence of (Closed-Interval-MSpace 0 ,1) by A22, A53, Th7, XBOOLE_1:1;
A54:
S1 is convergent
by A53, Th10;
then
S2 is convergent
by Th9;
then
lim S2 = lim S1
by Th9;
then A55:
lim s2 = lim S1
by A53, Th6;
A56:
I[01] = TopSpaceMetr (Closed-Interval-MSpace 0 ,1)
by TOPMETR:27, TOPMETR:def 8;
then reconsider S00 = f * S1 as sequence of X by Th3;
A57:
S00 is convergent
by A8, A54, A56, Th4;
for n4 being Element of NAT holds S00 . n4 in F2
then A60:
lim S00 in F2
by A7, A57, Th2;
dom f =
the carrier of I[01]
by FUNCT_2:def 1
.=
the carrier of (Closed-Interval-MSpace 0 ,1)
by A56, TOPMETR:16
;
then
f . (lim S1) in rng f
by FUNCT_1:12;
then reconsider t1 = f . (lim S1) as Point of X by TOPMETR:16;
for r being Real st r > 0 holds
ex n being Element of NAT st
for m being Element of NAT st m >= n holds
dist (S00 . m),t1 < r
proof
let r be
Real;
:: thesis: ( r > 0 implies ex n being Element of NAT st
for m being Element of NAT st m >= n holds
dist (S00 . m),t1 < r )
assume
r > 0
;
:: thesis: ex n being Element of NAT st
for m being Element of NAT st m >= n holds
dist (S00 . m),t1 < r
then consider r7 being
Real such that A61:
(
r7 > 0 & ( for
w being
Point of
(Closed-Interval-MSpace 0 ,1) for
w1 being
Point of
X st
w1 = f . w &
dist (lim S1),
w < r7 holds
dist t1,
w1 < r ) )
by A8, A56, UNIFORM1:5;
consider n0 being
Element of
NAT such that A62:
for
m being
Element of
NAT st
m >= n0 holds
dist (S1 . m),
(lim S1) < r7
by A54, A61, TBSP_1:def 4;
for
m being
Element of
NAT st
m >= n0 holds
dist (S00 . m),
t1 < r
hence
ex
n being
Element of
NAT st
for
m being
Element of
NAT st
m >= n holds
dist (S00 . m),
t1 < r
;
:: thesis: verum
end;
then
f . (lim S1) = lim S00
by A57, TBSP_1:def 4;
then
f . (lim s1) in F1 /\ F2
by A40, A41, A52, A53, A55, A60, XBOOLE_0:def 4;
hence
ex r being Real st
( r1 <= r & r <= r2 & f . r in F1 /\ F2 )
by A17, A18, A41; :: thesis: verum