let X be non empty MetrSpace; 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); 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); 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; ( 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 & f . r1 in F1 )
and
A4:
f . r2 in F2
and
A5:
F1 is closed
and
A6:
F2 is closed
and
A7:
f is continuous
and
A8:
F1 \/ F2 = the carrier of X
; ex r being Real st
( r1 <= r & r <= r2 & f . r in F1 /\ F2 )
A9:
r1 in { r3 where r3 is Real : ( r1 <= r3 & r3 <= r2 & f . r3 in F1 ) }
by A3;
{ 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 A9;
A10:
for r being Real st r in R holds
r <= r2
proof
let r be
Real;
( r in R implies r <= r2 )
assume
r in R
;
r <= r2
then
ex
r3 being
Real st
(
r3 = r &
r1 <= r3 &
r3 <= r2 &
f . r3 in F1 )
;
hence
r <= r2
;
verum
end;
r2 is UpperBound of R
then A11:
R is bounded_above
;
then consider s1 being Real_Sequence such that
A12:
( s1 is non-decreasing & s1 is convergent )
and
A13:
rng s1 c= R
and
A14:
lim s1 = upper_bound R
by Th11;
{ r3 where r3 is Real : ( r1 <= r3 & r3 <= r2 & f . r3 in F1 ) } c= [.0,1.]
then reconsider S1 = s1 as sequence of (Closed-Interval-MSpace (0,1)) by A13, Th5, XBOOLE_1:1;
A17:
I[01] = TopSpaceMetr (Closed-Interval-MSpace (0,1))
by TOPMETR:20, TOPMETR:def 7;
then reconsider S00 = f * S1 as sequence of X by Th2;
A18:
S00 is convergent
by A7, A12, A17, Th3, Th8;
dom f =
the carrier of I[01]
by FUNCT_2:def 1
.=
the carrier of (Closed-Interval-MSpace (0,1))
by A17, TOPMETR:12
;
then
f . (lim S1) in rng f
by FUNCT_1:3;
then reconsider t1 = f . (lim S1) as Point of X by TOPMETR:12;
reconsider S2 = s1 as sequence of RealSpace by METRIC_1:def 13;
A19:
S1 is convergent
by A12, Th8;
then
S2 is convergent
by Th7;
then
lim S2 = lim S1
by Th7;
then A20:
lim s1 = lim S1
by A12, Th4;
A21:
for r being Real st r > 0 holds
ex n being Nat st
for m being Nat st m >= n holds
dist ((S00 . m),t1) < r
proof
let r be
Real;
( r > 0 implies ex n being Nat st
for m being Nat st m >= n holds
dist ((S00 . m),t1) < r )
assume
r > 0
;
ex n being Nat st
for m being Nat st m >= n holds
dist ((S00 . m),t1) < r
then consider r7 being
Real such that A22:
r7 > 0
and A23:
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 A7, A17, UNIFORM1:4;
consider n0 being
Nat such that A24:
for
m being
Nat st
m >= n0 holds
dist (
(S1 . m),
(lim S1))
< r7
by A19, A22, TBSP_1:def 3;
for
m being
Nat st
m >= n0 holds
dist (
(S00 . m),
t1)
< r
hence
ex
n being
Nat st
for
m being
Nat st
m >= n holds
dist (
(S00 . m),
t1)
< r
;
verum
end;
A27:
r2 >= upper_bound R
by A10, SEQ_4:144;
then A28:
r2 in { r3 where r3 is Real : ( upper_bound R <= r3 & r3 <= r2 & f . r3 in F2 ) }
by A4;
{ 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 A28;
A29:
for r being Real st r in R2 holds
r >= upper_bound R
upper_bound R is LowerBound of R2
then A30:
R2 is bounded_below
;
then consider s2 being Real_Sequence such that
A31:
( s2 is non-increasing & s2 is convergent )
and
A32:
rng s2 c= R2
and
A33:
lim s2 = lower_bound R2
by Th12;
A34:
0 <= upper_bound R
by A1, A9, A11, SEQ_4:def 1;
{ r3 where r3 is Real : ( upper_bound R <= r3 & r3 <= r2 & f . r3 in F2 ) } c= [.0,1.]
then reconsider S1 = s2 as sequence of (Closed-Interval-MSpace (0,1)) by A32, Th5, XBOOLE_1:1;
reconsider S2 = s2 as sequence of RealSpace by METRIC_1:def 13;
A37:
S1 is convergent
by A31, Th8;
then
S2 is convergent
by Th7;
then
lim S2 = lim S1
by Th7;
then A38:
lim s2 = lim S1
by A31, Th4;
for n4 being Nat holds S00 . n4 in F1
then
lim S00 in F1
by A5, A7, A19, A17, Th1, Th3;
then A40:
f . (lim s1) in F1
by A20, A18, A21, TBSP_1:def 3;
A41:
I[01] = TopSpaceMetr (Closed-Interval-MSpace (0,1))
by TOPMETR:20, TOPMETR:def 7;
then reconsider S00 = f * S1 as sequence of X by Th2;
dom f =
the carrier of I[01]
by FUNCT_2:def 1
.=
the carrier of (Closed-Interval-MSpace (0,1))
by A41, TOPMETR:12
;
then
f . (lim S1) in rng f
by FUNCT_1:3;
then reconsider t1 = f . (lim S1) as Point of X by TOPMETR:12;
A42:
for r being Real st r > 0 holds
ex n being Nat st
for m being Nat st m >= n holds
dist ((S00 . m),t1) < r
proof
let r be
Real;
( r > 0 implies ex n being Nat st
for m being Nat st m >= n holds
dist ((S00 . m),t1) < r )
assume
r > 0
;
ex n being Nat st
for m being Nat st m >= n holds
dist ((S00 . m),t1) < r
then consider r7 being
Real such that A43:
r7 > 0
and A44:
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 A7, A41, UNIFORM1:4;
consider n0 being
Nat such that A45:
for
m being
Nat st
m >= n0 holds
dist (
(S1 . m),
(lim S1))
< r7
by A37, A43, TBSP_1:def 3;
for
m being
Nat st
m >= n0 holds
dist (
(S00 . m),
t1)
< r
hence
ex
n being
Nat st
for
m being
Nat st
m >= n holds
dist (
(S00 . m),
t1)
< r
;
verum
end;
A48:
r1 <= upper_bound R
by A9, A11, SEQ_4:def 1;
for s being Real st 0 < s holds
ex r being Real st
( r in R2 & r < (upper_bound R) + s )
proof
let s be
Real;
( 0 < s implies ex r being Real st
( r in R2 & r < (upper_bound R) + s ) )
assume A49:
0 < s
;
ex r being Real st
( r in R2 & r < (upper_bound R) + s )
now ex r being Real st
( r < (upper_bound R) + s & r in R2 )assume A50:
for
r being
Real st
r < (upper_bound R) + s holds
not
r in R2
;
contradictionnow ( ( r2 - (upper_bound R) = 0 & contradiction ) or ( r2 - (upper_bound R) > 0 & contradiction ) )per cases
( r2 - (upper_bound R) = 0 or r2 - (upper_bound R) > 0 )
by A27, XREAL_1:48;
case A51:
r2 - (upper_bound R) > 0
;
contradictionset rs0 =
min (
(r2 - (upper_bound R)),
s);
set r0 =
(upper_bound R) + ((min ((r2 - (upper_bound R)),s)) / 2);
A52:
min (
(r2 - (upper_bound R)),
s)
> 0
by A49, A51, XXREAL_0:21;
then A53:
upper_bound R < (upper_bound R) + ((min ((r2 - (upper_bound R)),s)) / 2)
by XREAL_1:29, XREAL_1:215;
min (
(r2 - (upper_bound R)),
s)
<= r2 - (upper_bound R)
by XXREAL_0:17;
then A54:
(upper_bound R) + (min ((r2 - (upper_bound R)),s)) <= (upper_bound R) + (r2 - (upper_bound R))
by XREAL_1:7;
A55:
(min ((r2 - (upper_bound R)),s)) / 2
< min (
(r2 - (upper_bound R)),
s)
by A52, XREAL_1:216;
then
(upper_bound R) + ((min ((r2 - (upper_bound R)),s)) / 2) < (upper_bound R) + (min ((r2 - (upper_bound R)),s))
by XREAL_1:8;
then A56:
(upper_bound R) + ((min ((r2 - (upper_bound R)),s)) / 2) <= r2
by A54, 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, A48, A52, BORSUK_1:40, 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 3;
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:12;
then A57:
(
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 A8, XBOOLE_0:def 3;
upper_bound R <= (upper_bound R) + ((min ((r2 - (upper_bound R)),s)) / 2)
by A52, XREAL_1:29, XREAL_1:215;
then A58:
r1 <= (upper_bound R) + ((min ((r2 - (upper_bound R)),s)) / 2)
by A48, XXREAL_0:2;
min (
(r2 - (upper_bound R)),
s)
<= s
by XXREAL_0:17;
then
(min ((r2 - (upper_bound R)),s)) / 2
< s
by A55, XXREAL_0:2;
then
(upper_bound R) + ((min ((r2 - (upper_bound R)),s)) / 2) < (upper_bound R) + s
by XREAL_1:8;
then A59:
not
(upper_bound R) + ((min ((r2 - (upper_bound R)),s)) / 2) in R2
by A50;
upper_bound R < (upper_bound R) + ((min ((r2 - (upper_bound R)),s)) / 2)
by A52, XREAL_1:29, XREAL_1:215;
then
(upper_bound R) + ((min ((r2 - (upper_bound R)),s)) / 2) in R
by A59, A58, A56, A57;
hence
contradiction
by A11, A53, SEQ_4:def 1;
verum end; end; end; hence
contradiction
;
verum end;
hence
ex
r being
Real st
(
r in R2 &
r < (upper_bound R) + s )
;
verum
end;
then A60:
upper_bound R = lower_bound R2
by A29, A30, SEQ_4:def 2;
S00 is convergent
by A7, A31, A41, Th3, Th8;
then A61:
f . (lim S1) = lim S00
by A42, TBSP_1:def 3;
for n4 being Nat holds S00 . n4 in F2
then
lim S00 in F2
by A6, A7, A37, A41, Th1, Th3;
then
f . (lim s1) in F1 /\ F2
by A60, A14, A40, A33, A38, A61, XBOOLE_0:def 4;
hence
ex r being Real st
( r1 <= r & r <= r2 & f . r in F1 /\ F2 )
by A27, A48, A14; verum