:: Sequences of Metric Spaces and an Abstract Intermediate Value Theorem
:: by Yatsuka Nakamura and Andrzej Trybulec
::
:: Received September 11, 2002
:: Copyright (c) 2002-2017 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, XBOOLE_0, SUBSET_1, XXREAL_0, SEQ_4, XXREAL_2, ARYTM_1,
CARD_1, ARYTM_3, METRIC_1, NAT_1, PCOMPS_1, SEQ_2, FUNCT_1, RCOMP_1,
ORDINAL2, TARSKI, REAL_1, STRUCT_0, PRE_TOPC, RELAT_1, SEQ_1, COMPLEX1,
XXREAL_1, TOPMETR, VALUED_0, BORSUK_1, EUCLID, TOPREAL1, TOPREAL2,
PSCOMP_1, JORDAN6, TOPS_2;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0,
XXREAL_2, XREAL_0, COMPLEX1, REAL_1, RELAT_1, FUNCT_1, RELSET_1,
PARTFUN1, FUNCT_2, BINOP_1, NAT_1, STRUCT_0, METRIC_1, PRE_TOPC, TOPS_2,
COMPTS_1, PCOMPS_1, RCOMP_1, EUCLID, PSCOMP_1, TOPMETR, SEQ_1, SEQ_2,
SEQM_3, SEQ_4, TBSP_1, JORDAN6, TOPREAL1, TOPREAL2;
constructors REAL_1, COMPLEX1, RCOMP_1, TOPS_2, COMPTS_1, TBSP_1, TOPMETR,
TOPREAL1, PSCOMP_1, JORDAN5C, JORDAN6, SEQ_4, BINOP_2, SEQ_2, PCOMPS_1,
COMSEQ_2, BINOP_1;
registrations XBOOLE_0, ORDINAL1, RELSET_1, NUMBERS, XREAL_0, NAT_1, MEMBERED,
STRUCT_0, PRE_TOPC, METRIC_1, PCOMPS_1, EUCLID, TOPMETR, COMPTS_1,
VALUED_0, SEQ_4;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
definitions TARSKI, XXREAL_2;
equalities STRUCT_0;
expansions TARSKI, XXREAL_2;
theorems PRE_TOPC, TOPMETR, XREAL_0, TBSP_1, XBOOLE_0, METRIC_1, FUNCT_1,
XBOOLE_1, FUNCT_2, JGRAPH_2, GOBOARD6, SEQ_2, TREAL_1, SEQ_4, NAT_1,
SEQM_3, UNIFORM1, BORSUK_1, JORDAN6, TOPREAL1, TOPS_2, TARSKI, RELAT_1,
TOPREAL3, JORDAN5B, PREPOWER, XCMPLX_1, XREAL_1, XXREAL_0, XXREAL_1,
EUCLID, ORDINAL1;
schemes FUNCT_2, RECDEF_1, NAT_1;
begin
theorem Th1:
for X being non empty MetrSpace, S being sequence of X, F being
Subset of TopSpaceMetr(X) st S is convergent & (for n being Nat
holds S.n in F) & F is closed holds lim S in F
proof
let X be non empty MetrSpace, S be sequence of X, F be Subset of
TopSpaceMetr(X);
assume that
A1: S is convergent and
A2: for n being Nat holds S.n in F and
A3: F is closed;
A4: for G being Subset of TopSpaceMetr(X) st G is open holds lim S in G
implies F meets G
proof
let G be Subset of TopSpaceMetr(X);
assume
A5: G is open;
now
assume lim S in G;
then consider r1 being Real such that
A6: r1>0 and
A7: Ball(lim S,r1) c= G by A5,TOPMETR:15;
reconsider r2=r1 as Real;
consider n being Nat such that
A8: for m being Nat st m>=n holds dist(S.m,lim S)0
ex n being Nat st for m being Nat st n<=m holds dist(T.m,x0)0;
then V is open & x0 in V by GOBOARD6:1,TOPMETR:14;
then consider W being Subset of TopSpaceMetr(X) such that
A5: p in W & W is open and
A6: f.:W c= V by A3,JGRAPH_2:10;
consider r0 being Real such that
A7: r0>0 and
A8: Ball(z0,r0) c= W by A5,TOPMETR:15;
reconsider r00=r0 as Real;
consider n0 being Nat such that
A9: for m being Nat st n0<=m holds dist(S.m,z0)0 ex n being Nat st for m being
Nat st n<=m holds dist(S.m,x0)0;
then consider n0 being Nat such that
A4: for m being Nat st n0<=m holds |.s.m-g.| < r by A3;
for m being Nat st n0<=m holds dist(S.m,x0)0 ex n being Nat st for m being
Nat st n<=m holds dist(S.m,x)0 ex n being Nat st for m being
Nat st n<=m holds dist(S.m,x0)0 ex n being Nat st for m being
Nat st n<=m holds dist(S1.m,x1)0;
then consider n0 being Nat such that
A10: for m being Nat st n0<=m holds dist(S.m,x0)0 ex n being Nat st for m being
Nat st n<=m holds dist(S1.m,x0)0 ex n being Nat st for m being
Nat st n<=m holds dist(S.m,x1)0;
then consider n0 being Nat such that
A13: for m being Nat st n0<=m holds dist(S1.m,x0)a-1
proof
let n be Nat;
a0;
then 1/(n+1)>0 by XCMPLX_1:215;
then consider r0 being Real such that
A3: r0 in R and
A4: (rs) -(1/(n+1) qua Real)=r2 implies
$3=$2)&(r1=r20;
then for r1,r2 being Real,n1 being Nat st r1=x & r2=s1.(
n1+1) & n1=n holds (r1>=r2 implies x=x)&(r1=r2 implies s1.(n+1)=x)& (r1=r2;
hence thesis by A10,A15;
end;
case
r1=r2;
hence thesis by A10;
end;
case
r1=r2;
hence thesis by A10;
end;
case
r1=r2;
hence s3.i<=s3.(i+1) by A10;
end;
case
r1=r2;
hence thesis by A10,A39;
end;
case
r10 holds upper_bound R -r0;
consider n2 being Nat such that
A46: 1/rrs-r by XREAL_1:10;
then
A48: rs-rlim s3;
then r>0 by XREAL_1:50;
then upper_bound R -rr00));
assume
A1: R is bounded_below;
A2: for n being Element of NAT ex r being Element of REAL st X[n,r]
proof
let n be Element of NAT;
(n+1)">0;
then 1/(n+1)>0 by XCMPLX_1:215;
then consider r0 being Real such that
A3: r0 in R and
A4: (rs) +(1/(n+1) qua Real)>r0 by A1,SEQ_4:def 2;
for r00 being Real st r00=r0 holds (rs)+(1/(n+1) qua Real)>r00 by A4;
hence thesis by A3;
end;
ex s1 being sequence of REAL st
for n being Element of NAT holds X[
n,s1.n] from FUNCT_2:sch 3(A2);
then consider s1 being sequence of REAL such that
A5: for n being Element of NAT holds s1.n in R & for r0 being Real
st r0=s1.n holds (rs)+(1/(n+1) qua Real)>r0;
defpred P[set,set,set] means ($2 is Real implies (for r1,r2 being
Real,n1 being Nat st r1=$2 & r2=s1.(n1+1) & n1=$1 holds (r1<=r2 implies
$3=$2)&(r1>r2 implies $3=s1.(n1+1)))) & (not $2 is Real implies $3=1);
A6: for n being Nat for x being set ex y being set st P[n,x,y]
proof
let n be Nat;
thus for x being set ex y being set st P[n,x,y]
proof
let x be set;
now
per cases;
case
not x is Real;
hence ex y being set st (x is Real implies for r1,r2 being
Real,n1 being Nat st r1=x & r2=s1.(n1+1) & n1=n holds (r1>=r2 implies y=
x)&(r1r2 implies x=s1.(n1+1));
hence thesis by A7;
end;
case
r10>r20;
then for r1,r2 being Real,n1 being Nat st r1=x & r2=s1.(
n1+1) & n1=n holds (r1<=r2 implies s1.(n+1)=x)& (r1>r2 implies s1.(n+1)=s1.(n1+
1));
hence thesis by A7;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
end;
ex f being Function st dom f = NAT & f.0 = s1.0 &
for n being Nat holds P[n,f.n,f.(n+1)] from RECDEF_1:sch 1(A6);
then consider s2 being Function such that
A8: dom s2 = NAT and
A9: s2.0 = s1.0 and
A10: for n being Nat holds P[n,s2.n,s2.(n+1)];
A11: rng s2 c= REAL
proof
defpred X[Nat] means s2.$1 in REAL;
let y be object;
assume y in rng s2;
then consider x being object such that
A12: x in dom s2 and
A13: y=s2.x by FUNCT_1:def 3;
reconsider n=x as Nat by A8,A12;
A14: for k being Nat st X[k] holds X[k+1]
proof
let k be Nat;
reconsider r2=s1.(k+1) as Real;
assume
A15: s2.k in REAL;
then reconsider r1=s2.k as Real;
now
per cases;
case
r1<=r2;
hence thesis by A10,A15;
end;
case
r1>r2;
then s2.(k+1)=s1.(k+1) by A10;
hence thesis;
end;
end;
hence thesis;
end;
A16: X[0] by A9;
for m being Nat holds X[m] from NAT_1:sch 2(A16,A14);
then s2.n in REAL;
hence thesis by A13;
end;
then reconsider s3=s2 as Real_Sequence by A8,FUNCT_2:2;
defpred X[Nat] means s1.$1>=s3.$1;
A17: for k being Nat st X[k] holds X[k+1]
proof
let k be Nat;
A18: k in NAT by ORDINAL1:def 12;
assume s1.k>=s3.k;
reconsider r2=s1.(k+1) as Real;
s2.k in rng s2 by A8,FUNCT_1:def 3,A18;
then reconsider r1=s2.k as Real by A11;
now
per cases;
case
r1<=r2;
hence thesis by A10;
end;
case
r1>r2;
hence thesis by A10;
end;
end;
hence thesis;
end;
A19: X[0] by A9;
A20: for n4 being Nat holds X[n4] from NAT_1:sch 2(A19,A17);
defpred X[Nat] means 0<=$1 implies s3.0>=s3.$1;
A21: for n4 being Nat holds s3.n4>=s3.(n4+1)
proof
let n4 be Nat;
reconsider r2=s1.(n4+1) as Real;
dom s3=NAT by FUNCT_2:def 1;
then reconsider r1=s2.n4 as Real;
now
per cases;
case
r1<=r2;
hence thesis by A10;
end;
case
r1>r2;
hence thesis by A10;
end;
end;
hence thesis;
end;
A22: for k being Nat st X[k] holds X[k+1]
proof
let k be Nat;
assume
A23: 0<=k implies s3.0>=s3.k;
now
assume 0<=k+1;
A24: s3.k>=s3.(k+1) by A21;
now
per cases;
case
0=s3.(k+1) by A23,A24,XXREAL_0:2;
end;
case
0=k+1;
hence s3.0>=s3.(k+1);
end;
end;
hence s3.0>=s3.(k+1);
end;
hence thesis;
end;
defpred Y[Nat] means for n4 being Nat st $1<=n4 holds s3.$1>=s3.
n4;
A25: for k being Nat st Y[k] holds Y[k+1]
proof
let k be Nat;
assume for n5 being Nat st k<=n5 holds s3.k>=s3.n5;
defpred X[Nat] means k+1<=$1 implies s3.(k+1)>=s3.$1;
A26: for i being Nat st X[i] holds X[i+1]
proof
let i be Nat;
A27: i in NAT by ORDINAL1:def 12;
reconsider r2=s1.(i+1) as Real;
s2.i in rng s2 by A8,FUNCT_1:def 3,A27;
then reconsider r1=s2.i as Real by A11;
A28: now
per cases;
case
r1<=r2;
hence s3.i>=s3.(i+1) by A10;
end;
case
r1>r2;
hence s3.i>=s3.(i+1) by A10;
end;
end;
assume
A29: k+1<=i implies s3.(k+1)>=s3.i;
now
assume
A30: k+1<=i+1;
now
per cases by A30,XXREAL_0:1;
case
k+1*=s3.(i+1) by A29,A28,NAT_1:13,XXREAL_0:2;
end;
case
k+1=i+1;
hence s3.(k+1)>=s3.(i+1);
end;
end;
hence s3.(k+1)>=s3.(i+1);
end;
hence thesis;
end;
A31: X[0];
thus for n4 being Nat holds X[n4] from NAT_1:sch 2(A31, A26);
end;
A32: X[0];
for n4 being Nat holds X[n4] from NAT_1:sch 2(A32,A22);
then
A33: Y[0];
for m4 being Nat holds Y[m4] from NAT_1:sch 2(A33,A25);
then for m4,n4 being Nat st m4 in dom s3 & n4 in dom s3 & m4 <=
n4 holds s3.m4 >= s3.n4;
then
A34: s3 is non-increasing by SEQM_3:def 4;
A35: rng s3 c= R
proof
defpred Z[Nat] means s3.$1 in R;
let y be object;
assume y in rng s3;
then
A36: ex x being object st x in dom s3 & y=s3.x by FUNCT_1:def 3;
A37: for k being Nat st Z[k] holds Z[k+1]
proof
let k be Nat;
A38: k in NAT by ORDINAL1:def 12;
reconsider r2=s1.(k+1) as Real;
s2.k in rng s2 by A8,FUNCT_1:def 3,A38;
then reconsider r1=s2.k as Real by A11;
assume
A39: s3.k in R;
now
per cases;
case
r1<=r2;
hence thesis by A10,A39;
end;
case
r1>r2;
then s2.(k+1)=s1.(k+1) by A10;
hence thesis by A5;
end;
end;
hence thesis;
end;
A40: Z[0] by A5,A9;
for nn being Nat holds Z[nn] from NAT_1:sch 2(A40,A37);
hence thesis by A36;
end;
for n being Nat holds s3.n > lower_bound R -1
proof
let n be Nat;
A41: n in NAT by ORDINAL1:def 12;
lower_bound R < lower_bound R +1 by XREAL_1:29;
then
A42: lower_bound R > lower_bound R -1 by XREAL_1:19;
s3.n in rng s3 by A8,FUNCT_1:def 3,A41;
then s3.n >=lower_bound R by A1,A35,SEQ_4:def 2;
hence thesis by A42,XXREAL_0:2;
end;
then
A43: s3 is bounded_below by SEQ_2:def 4;
A44: for r being Real st r>0 holds lower_bound R +r>lim s3
proof
let r be Real;
assume
A45: r>0;
consider n2 being Nat such that
A46: 1/rs1.n2 by A5,XXREAL_0:2,A47;
A49: s3.n2>=lim s3 by A34,A43,SEQ_4:38;
s1.n2>=s3.n2 by A20;
then rs+r>s3.n2 by A48,XXREAL_0:2;
hence thesis by A49,XXREAL_0:2;
end;
A50: now
reconsider r=(lim s3) -lower_bound R as Real;
assume lower_bound R0 by XREAL_1:50;
then lower_bound R +((lim s3)+-lower_bound R)>lim s3 by A44;
hence contradiction;
end;
A51: for n being Nat holds s3.n >=lower_bound R
proof
let n be Nat;
A52: n in NAT by ORDINAL1:def 12;
dom s3=NAT by FUNCT_2:def 1;
then s3.n in rng s3 by FUNCT_1:def 3,A52;
hence thesis by A1,A35,SEQ_4:def 2;
end;
for n being Nat holds s3.n > lower_bound R -1
proof
let n be Nat;
lower_bound Rlower_bound R -1 by XREAL_1:19;
s3.n>=lower_bound R by A51;
hence thesis by A53,XXREAL_0:2;
end;
then
A54: s3 is bounded_below by SEQ_2:def 4;
then lim s3>=lower_bound R by A34,A51,PREPOWER:1;
hence thesis by A34,A35,A54,A50,XXREAL_0:1;
end;
theorem Th13:
:: An Abstract Intermediate Value Theorem for Closed Sets
for X being non empty MetrSpace, f being Function of I[01],
TopSpaceMetr(X), F1,F2 being Subset of TopSpaceMetr(X),
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
ex r being Real st r1<=r & r<=r2 & f.r in F1 /\ F2
proof
let X be non empty MetrSpace, f be Function of I[01],TopSpaceMetr(X), F1,F2
be Subset of TopSpaceMetr(X),r1,r2 be Real;
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;
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
proof
let x be object;
assume x in {r3 where r3 is Real: r1<=r3 & r3<=r2 & f.r3 in F1};
then ex r3 being Real st r3=x & r1<=r3 & r3<=r2 & f.r3 in F1;
hence thesis by XREAL_0:def 1;
end;
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;
assume r in R;
then ex r3 being Real st r3=r & r1<=r3 & r3<=r2 & f.r3 in F1;
hence thesis;
end;
r2 is UpperBound of R
proof
let r be ExtReal;
assume r in R;
then ex r3 being Real st r3=r & r1<=r3 & r3<=r2 & f.r3 in F1;
hence thesis;
end;
then
A11: R is bounded_above;
then consider s1 being Real_Sequence such that
A12: s1 is non-decreasing 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.]
proof
let x be object;
assume x in {r3 where r3 is Real: r1<=r3 & r3<=r2 & f.r3 in F1};
then consider r3 being Real such that
A15: r3=x & r1<=r3 and
A16: r3<=r2 and
f.r3 in F1;
r3<=1 by A2,A16,XXREAL_0:2;
hence thesis by A1,A15,XXREAL_1:1;
end;
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,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 ex n being Nat st for m being
Nat st m>=n holds dist(S00.m,t1)0;
then consider r7 being Real such that
A22: r7>0 and
A23: for w being Point of Closed-Interval-MSpace(0,1), w1 being Point
of X st w1=f.w & dist(lim S1,w)=n0 holds dist(S1.m,lim S1)=n0 holds dist(S00.m,t1)=n0;
then dist(lim S1,S1.m)=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
proof
let x be object;
assume x in {r3 where r3 is Real:
upper_bound R<=r3 & r3<=r2 & f.r3 in F2};
then ex r3 being Real
st r3=x & upper_bound R<=r3 & r3<=r2 & f.r3 in F2;
hence thesis by XREAL_0:def 1;
end;
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
proof
let r be Real;
assume r in R2;
then ex r3 being Real
st r3=r & upper_bound R<=r3 & r3<=r2 & f.r3 in F2;
hence thesis;
end;
upper_bound R is LowerBound of R2
proof
let r be ExtReal;
assume r in R2;
then ex r3 being Real
st r3=r & upper_bound R<=r3 & r3<=r2 & f.r3 in F2;
hence thesis;
end;
then
A30: R2 is bounded_below;
then consider s2 being Real_Sequence such that
A31: s2 is non-increasing 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.]
proof
let x be object;
assume x in {r3 where r3 is Real:
upper_bound R<=r3 & r3<=r2 & f.r3 in F2};
then consider r3 being Real such that
A35: r3=x & upper_bound R<=r3 and
A36: r3<=r2 and
f.r3 in F2;
r3<=1 by A2,A36,XXREAL_0:2;
hence thesis by A34,A35,XXREAL_1:1;
end;
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
proof
let n4 be Nat;
A39: n4 in NAT by ORDINAL1:def 12;
dom s1=NAT by FUNCT_2:def 1;
then s1.n4 in rng s1 by FUNCT_1:def 3,A39;
then s1.n4 in R by A13;
then dom S00=NAT &
ex r3 being Real st r3=s1.n4 & r1<=r3 & r3<=r2 & f.r3
in F1 by TBSP_1:4;
hence thesis by FUNCT_1:12,A39;
end;
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,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 ex n being Nat st for m being
Nat st m>=n holds dist(S00.m,t1)0;
then consider r7 being Real such that
A43: r7>0 and
A44: for w being Point of Closed-Interval-MSpace(0,1), w1 being Point
of X st w1=f.w & dist(lim S1,w)=n0 holds dist(S1.m,lim S1)=n0 holds dist(S00.m,t1)=n0;
then dist(lim S1,S1.m)0;
set rs0=min(r2-upper_bound R,s);
set r0=upper_bound R + rs0/2;
A52: rs0>0 by A49,A51,XXREAL_0:21;
then
A53: upper_bound Rr2;
reconsider Q=P as non empty Subset of Euclid 2 by TOPREAL3:8;
A49: the carrier of (TOP-REAL 2)|P1=[#]((TOP-REAL 2)|P1)
.=P1 by PRE_TOPC:def 5;
the carrier of (TOP-REAL 2)|P=[#]((TOP-REAL 2)|P)
.=P by PRE_TOPC:def 5;
then rng f c= the carrier of (TOP-REAL 2)|P by A3,A49;
then reconsider g=f as Function of I[01],(TOP-REAL 2)|P by A17,
FUNCT_2:2;
P=P1 \/ P by A3,XBOOLE_1:12;
then
A50: (TOP-REAL 2)|P1 is SubSpace of (TOP-REAL 2)|P by TOPMETR:4;
U2 \/ U3 =the carrier of ((Euclid 2)|Q) & (TOP-REAL 2)|P=
TopSpaceMetr(( Euclid 2)|Q) by A8,EUCLID:63,TOPMETR:def 2;
then consider r0 being Real such that
A51: r2<=r0 and
A52: r0<=r1 and
A53: g.r0 in U2 /\ U3 by A19,A7,A9,A29,A34,A32,A37,A48,A50,Th13,
PRE_TOPC:26;
r0<1 by A34,A52,XXREAL_0:2;
then
A54: r0 in dom f by A17,A29,A51,BORSUK_1:40,XXREAL_1:1;
A55: 1 in dom f by A17,BORSUK_1:40,XXREAL_1:1;
A56: 0 in dom f by A17,BORSUK_1:40,XXREAL_1:1;
now
per cases by A10,A53,TARSKI:def 2;
case
g.r0=W-min(P);
hence contradiction by A14,A16,A29,A51,A54,A56,FUNCT_1:def 4;
end;
case
g.r0=E-max(P);
hence contradiction by A15,A16,A34,A52,A54,A55,FUNCT_1:def 4;
end;
end;
hence contradiction;
end;
end;
hence contradiction;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
*