:: Brouwer Fixed Point Theorem in the General Case
:: by Karol P\kak
::
:: Received December 21, 2010
:: Copyright (c) 2010-2026 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 ABIAN, ARYTM_1, ARYTM_3, BORSUK_1, BROUWER, CARD_1, COMPLEX1,
CONNSP_2, CONVEX1, EUCLID, FUNCOP_1, FUNCT_1, FUNCT_3, FUNCT_4, JGRAPH_4,
MEASURE5, MEMBERED, METRIC_1, NAT_1, NUMBERS, ORDINAL2, PCOMPS_1,
PRE_TOPC, PROB_1, RCOMP_1, REAL_1, RELAT_1, RLAFFIN1, RLTOPSP1, RLVECT_1,
RLVECT_5, RUSUB_4, RVSUM_1, STRUCT_0, SUBSET_1, SUPINF_2, TARSKI,
TOPMETR, TOPREALB, TOPS_1, TOPS_2, VALUED_1, VALUED_2, XBOOLE_0, XREAL_0,
XXREAL_0, XXREAL_2, FUNCT_2;
notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1,
FUNCT_2, ORDINAL1, NUMBERS, VALUED_1, CARD_1, XCMPLX_0, XREAL_0,
XXREAL_0, MEMBERED, COMPLEX1, FUNCOP_1, FINSEQ_2, VALUED_2, STRUCT_0,
PRE_TOPC, RLAFFIN2, TOPS_1, METRIC_1, PCOMPS_1, TOPMETR, BORSUK_1,
RLVECT_1, RLTOPSP1, EUCLID, TOPREAL9, TOPREALB, DOMAIN_1, TOPS_2,
COMPTS_1, TBSP_1, XXREAL_2, FUNCT_4, JGRAPH_4, TMAP_1, RUSUB_4, CONVEX1,
REAL_1, CONNSP_2, BROUWER, ABIAN, RLVECT_5, RLAFFIN1;
constructors BINOP_2, COMPLEX1, TBSP_1, MONOID_0, CONVEX1, GRCAT_1, TOPREAL9,
TOPS_1, COMPTS_1, PCOMPS_1, FUNCSDOM, JGRAPH_4, TMAP_1, TOPREALC,
BROUWER, ABIAN, RUSUB_4, RLAFFIN1, RLAFFIN2, RLVECT_5, SEQ_4, FUNCT_4,
REAL_1, XXREAL_3, SIMPLEX2, SIMPLEX1;
registrations BORSUK_1, BORSUK_3, BROUWER, CARD_1, COMPTS_1, CONVEX1, EUCLID,
FUNCOP_1, FUNCT_1, FUNCT_2, JGRAPH_4, JORDAN, JORDAN2C, MEMBERED, NAT_1,
PCOMPS_1, PRE_TOPC, RELAT_1, REVROT_1, RLAFFIN1, RLAFFIN3, RLTOPSP1,
RLVECT_1, SIMPLEX2, STRUCT_0, SUBSET_1, TMAP_1, TOPGRP_1, TOPMETR,
TOPREAL1, TOPREAL9, TOPREALC, TOPS_1, VALUED_0, VALUED_2, WAYBEL_2,
XBOOLE_0, XCMPLX_0, XREAL_0, XXREAL_0, RELSET_1, FINSET_1, ORDINAL1;
requirements ARITHM, BOOLE, NUMERALS, SUBSET, REAL;
definitions TARSKI, BORSUK_1;
equalities XCMPLX_0, STRUCT_0, ALGSTR_0, TOPREAL9, BROUWER, ORDINAL1;
expansions TARSKI, BORSUK_1;
theorems ABIAN, ABSVALUE, BOOLMARK, BORSUK_1, BROUWER, COMPLEX1, COMPTS_1,
CONNSP_2, CONVEX1, EUCLID, FUNCOP_1, FUNCT_1, FUNCT_2, FUNCT_4, GOBOARD6,
HAUSDORF, JGRAPH_4, JORDAN24, JORDAN2C, MEMBERED, METRIC_1, NECKLACE,
ORDINAL1, PRE_TOPC, RELAT_1, RLAFFIN1, RLAFFIN2, RLAFFIN3, RLTOPSP1,
RLVECT_1, RUSUB_4, SIMPLEX2, SPPOL_1, SUBSET_1, TARSKI, TBSP_1, TMAP_1,
TOPGEN_1, TOPMETR, TOPMETR2, TOPREAL9, TOPREALB, TOPREALC, TOPRNS_1,
TOPS_1, TOPS_2, TOPS_4, VALUED_2, XBOOLE_0, XBOOLE_1, XCMPLX_1, XREAL_0,
XREAL_1, XXREAL_0, XXREAL_2, ZFMISC_1, RLVECT_4;
begin :: Preliminaries
reserve n for Nat,
p,q,u,w for Point of TOP-REAL n,
S for Subset of TOP-REAL n,
A, B for convex Subset of TOP-REAL n,
r for Real;
Lm1: (1-r)*p+r*q-p = r*(q-p)
proof
thus (1-r)*p+r*q-p = r*q+((1-r)*p-p) by RLVECT_1:def 3
.= r*q+((1 *p-r*p)-p) by RLVECT_1:35
.= r*q+((p-r*p)-p) by RLVECT_1:def 8
.= r*q+((p+-r*p)+-p)
.= r*q+((p+-p)+-r*p) by RLVECT_1:def 3
.= r*q+((p-p)-r*p)
.= r*q+(0.(TOP-REAL n)-r*p) by RLVECT_1:15
.= r*q-r*p
.= r*(q-p) by RLVECT_1:34;
end;
Lm2: r>=0 implies r*p in halfline(0.TOP-REAL n,p)
proof
assume
A1: r>=0;
(1-r)*0.TOP-REAL n=0.TOP-REAL n & 0.TOP-REAL n+r*p=r*p;
hence thesis by A1;
end;
theorem Th1:
(1-r)*p + r*q = p + r*(q-p)
proof
thus p+r*(q-p) = ((1-r)*p+r*q-p)+p by Lm1
.= ((1-r)*p+r*q)-(p-p) by RLVECT_1:29
.= ((1-r)*p+r*q)-0.TOP-REAL n by RLVECT_1:15
.= (1-r)*p+r*q;
end;
theorem Th2:
u in halfline(p,q) & w in halfline(p,q) & |.u-p.| = |.w-p.| implies u = w
proof
set r1=u,r2=w;
assume that
A1: r1 in halfline(p,q) and
A2: r2 in halfline(p,q) and
A3: |.r1-p.|=|.r2-p.|;
per cases;
suppose p<>q;
then
A4: |.q-p.|<>0 by TOPRNS_1:28;
consider a1 be Real such that
A5: r1=(1-a1)*p+a1*q and
A6: a1>=0 by A1;
A7: |.a1.|=a1 by A6,ABSVALUE:def 1;
a1 in REAL & r1-p=a1*(q-p) by A5,Lm1,XREAL_0:def 1;
then
A8: |.r1-p.|=|.a1.|*|.q-p.| by TOPRNS_1:7;
consider a2 be Real such that
A9: r2=(1-a2)*p+a2*q and
A10: a2>=0 by A2;
a2 in REAL & r2-p=a2*(q-p) by A9,Lm1,XREAL_0:def 1;
then
A11: |.r2-p.|=|.a2.|*|.q-p.| by TOPRNS_1:7;
|.a2.|=a2 by A10,ABSVALUE:def 1;
then a1=a2 by A3,A4,A8,A11,A7,XCMPLX_1:5;
hence thesis by A5,A9;
end;
suppose
A12: p=q;
then r1 in {p} by A1,TOPREAL9:29;
then
A13: r1=p by TARSKI:def 1;
r2 in {p} by A2,A12,TOPREAL9:29;
hence thesis by A13,TARSKI:def 1;
end;
end;
Lm3: for A be Subset of TOP-REAL n st
p in A & p<>q & A/\halfline(p,q) is bounded
ex w be Point of Euclid n st w in (Fr A)/\halfline(p,q) &
(for u,P be Point of Euclid n st
P=p & u in A/\halfline(p,q) holds dist(P,u)<=dist(P,w)) &
for r st r>0 ex u be Point of Euclid n st u in A/\halfline(p,q) &
dist(w,u)<r
proof
set TRn=TOP-REAL n;
let A be Subset of TRn such that
A1: p in A and
A2: p<>q and
A3: A/\halfline(p,q) is bounded;
reconsider P=p,Q=q as Element of Euclid n by EUCLID:67;
A4: dist(P,Q)>0 by A2,METRIC_1:7;
set H=halfline(p,q);
reconsider AH=A/\H as bounded Subset of Euclid n by A3,JORDAN2C:11;
A5: dist(Q,P)=|.q-p.| by SPPOL_1:39;
p in H by TOPREAL9:27;
then
A6: p in AH by A1,XBOOLE_0:def 4;
set DAH=diameter AH;
set X={r where r is Real:(1-r)*p+r*q in AH & 0<=r};
set dAH=DAH+1;
A7: now let x be object;
assume x in X;
then ex r be Real st x=r & (1-r)*p+r*q in AH & 0<=r;
hence x is real;
end;
1 *p=p & 0 *q=0.TRn by RLVECT_1:10,def 8;
then p=(1-0)*p+0 *q;
then
A8: 0 in X by A6;
then reconsider X as non empty real-membered set by A7,MEMBERED:def 3;
A9: DAH+0<dAH by XREAL_1:8;
now let x be ExtReal;
assume x in X;
then consider r be Real such that
A10: x=r and
A11: (1-r)*p+r*q in AH and
A12: 0<=r;
reconsider PQ=(1-r)*p+r*q as Element of Euclid n by A11;
(1-r)*p+r*q-p=r*(q-p) by Lm1;
then dist(PQ,P) = |.r*(q-p).| by SPPOL_1:39
.= |.r.|*|.q-p.| by TOPRNS_1:7
.= r*dist(Q,P) by A5,A12,ABSVALUE:def 1;
then r*dist(Q,P)<=DAH by A6,A11,TBSP_1:def 8;
then
A13: r*dist(Q,P)<=dAH by A9,XXREAL_0:2;
r*dist(Q,P)/dist(Q,P)=r*(dist(Q,P)/dist(Q,P))
.=r*1 by A4,XCMPLX_1:60;
hence x<=dAH/dist(Q,P) by A10,A13,XREAL_1:72;
end;
then dAH/dist(P,Q) is UpperBound of X by XXREAL_2:def 1;
then X is bounded_above by XXREAL_2:def 10;
then reconsider S=sup X as Element of REAL by XXREAL_2:16;
A14: 0<=S by A8,XXREAL_2:4;
set Spq=(1-S)*p+S*q;
reconsider spq=Spq as Element of Euclid n by EUCLID:67;
A15: for r be Real st r>0
ex w be Point of Euclid n st w in AH & dist(spq,w)<r
proof
let r be Real such that
A16: r>0;
set r2=r/|.q-p.|;
assume
A17: for w be Point of Euclid n st w in AH holds dist(spq,w)>=r;
now let x be ExtReal;
assume
A18: x in X;
then consider w be Real such that
A19: x=w and
A20: (1-w)*p+w*q in AH and 0<=w;
S-w>=0 by A18,A19,XREAL_1:48,XXREAL_2:4;
then
A21: |.S-w.|=S-w by ABSVALUE:def 1;
reconsider PQ=(1-w)*p+w*q as Element of Euclid n by A20;
A22: PQ=p+w*(q-p) by Th1;
Spq-(p+w*(q-p)) = (Spq-p)-w*(q-p) by RLVECT_1:27
.= S*(q-p)-w*(q-p) by Lm1
.= (S-w)*(q-p) by RLVECT_1:35;
then dist(spq,PQ) = |.(S-w)*(q-p).| by A22,SPPOL_1:39
.= (S-w)*|.q-p.| by A21,TOPRNS_1:7;
then (S-w)*|.q-p.|>=r by A17,A20;
then S-w>=r2 by A2,A5,METRIC_1:7,XREAL_1:79;
hence S-r2>=x by A19,XREAL_1:11;
end;
then S-r2 is UpperBound of X by XXREAL_2:def 1;
then S-0<=S-r2 by XXREAL_2:def 3;
hence contradiction by A4,A5,A16,XREAL_1:8;
end;
A23: the TopStruct of TRn=TopSpaceMetr Euclid n by EUCLID:def 8;
now let U be Subset of TRn;
reconsider UE=U as Subset of TopSpaceMetr Euclid n by A23;
assume that
A24: U is open and
A25: Spq in U;
UE in the topology of TopSpaceMetr Euclid n by A23,A24,PRE_TOPC:def 2;
then UE is open by PRE_TOPC:def 2;
then consider r be Real such that
A26: r>0 and
A27: Ball(spq,r)c=UE by A25,TOPMETR:15;
set r2 = r/|.q-p.|;
set Sr = S+r2/2;
consider w be Element of Euclid n such that
A28: w in AH & dist(spq,w)<r by A15,A26;
w in Ball(spq,r) & w in A by A28,METRIC_1:11,XBOOLE_0:def 4;
hence A meets U by A27,XBOOLE_0:3;
A29: r2*|.q-p.| = r*(|.q-p.|/|.q-p.|)
.= r*1 by A4,A5,XCMPLX_1:60;
Sr>S+0 by A4,A5,A26,XREAL_1:6;
then S-Sr<0 by XREAL_1:49;
then
A30: |.S-Sr.| = -(S-Sr) by ABSVALUE:def 1
.= r2/2;
set Srpq=(1-Sr)*p+Sr*q;
reconsider srpq=Srpq as Element of Euclid n by EUCLID:67;
A31: srpq in H by A14,A26;
A32: not srpq in A
proof
assume srpq in A;
then srpq in AH by A31,XBOOLE_0:def 4;
then Sr in X by A14,A26;
then S+r2/2<=S+0 by XXREAL_2:4;
hence contradiction by A4,A5,A26,XREAL_1:8;
end;
Spq-Srpq = Spq-(p+Sr*(q-p)) by Th1
.= (Spq-p)-Sr*(q-p) by RLVECT_1:27
.= S*(q-p)-Sr*(q-p) by Lm1
.= (S-Sr)*(q-p) by RLVECT_1:35;
then dist(spq,srpq) = |.(S-Sr)*(q-p).| by SPPOL_1:39
.= r2/2*|.q-p.| by A30,TOPRNS_1:7
.= r/2 by A29;
then dist(spq,srpq)<r by A26,XREAL_1:216;
then srpq in Ball(spq,r) by METRIC_1:11;
hence U\A<>{} by A27,A32,XBOOLE_0:def 5;
end;
then
A33: Spq in Fr A by TOPGEN_1:9;
take spq;
A34: Spq-p=S*(q-p) by Lm1;
Spq in H by A14;
hence spq in (Fr A)/\H by A33,XBOOLE_0:def 4;
A35: |.S.|=S by A14,ABSVALUE:def 1;
hereby let u,P be Point of Euclid n such that
A36: P=p and
A37: u in A/\H;
A38: dist(P,spq) = |.S*(q-p).| by A34,A36,SPPOL_1:39
.= S*|.q-p.| by A35,TOPRNS_1:7;
u in H by A37,XBOOLE_0:def 4;
then consider Ur be Real such that
A39: u=(1-Ur)*p+Ur*q and
A40: 0<=Ur;
A41: |.Ur.|=Ur by A40,ABSVALUE:def 1;
Ur in X by A37,A39,A40;
then
A42: Ur<=S by XXREAL_2:4;
set du=dist(P,u),ds=dist(P,spq);
A43: (1-Ur)*p+Ur*q-p=Ur*(q-p) by Lm1;
dist(P,u) = |.Ur*(q-p).| by A36,A39,A43,SPPOL_1:39
.= Ur*|.q-p.| by A41,TOPRNS_1:7;
hence du<=ds by A38,A42,XREAL_1:64;
end;
thus thesis by A15;
end;
theorem
for S st p in S & p <> q & S/\halfline(p,q) is bounded
ex w st w in (Fr S)/\halfline(p,q) &
(for u st u in S/\halfline(p,q) holds |.p-u.| <= |.p-w.|) &
for r st r > 0 ex u st u in S/\halfline(p,q) & |.w-u.| < r
proof
set T=TOP-REAL n,E=Euclid n;
let A be Subset of T such that
A1: p in A & p<>q & A/\halfline(p,q) is bounded;
consider W be Point of E such that
A2: W in (Fr A)/\halfline(p,q) and
A3: for u,P be Point of E st P=p & u in A/\halfline(p,q)
holds dist(P,u)<= dist(P,W) and
A4: for r st r>0 ex u be Point of E st u in A/\halfline(p,q)
& dist(W,u)<r by A1,Lm3;
reconsider w=W as Point of T by EUCLID:67;
take w;
thus w in (Fr A)/\halfline(p,q) by A2;
reconsider P=p as Point of E by EUCLID:67;
hereby let u be Point of T such that
A5: u in A/\halfline(p,q);
reconsider U=u as Point of E by EUCLID:67;
A6: dist(P,U)=|.p-u.| by SPPOL_1:39;
dist(P,U)<=dist(P,W) by A3,A5;
hence |.p-u.|<=|.p-w.| by A6,SPPOL_1:39;
end;
let r be Real;
assume r>0;
then consider U be Point of E such that
A7: U in A/\halfline(p,q) & dist(W,U)<r by A4;
reconsider u=U as Point of T by EUCLID:67;
dist(W,U)=|.w-u.| by SPPOL_1:39;
hence thesis by A7;
end;
theorem Th4:
for A st A is closed & p in Int A & p <> q & A/\halfline(p,q) is bounded
ex u st(Fr A)/\halfline(p,q)={u}
proof
set TRn=TOP-REAL n;
set En=Euclid n;
let A be convex Subset of TOP-REAL n such that
A1: A is closed and
A2: p in Int A and
A3: p<>q and
A4: A/\halfline(p,q) is bounded;
reconsider P=p,Q=q as Point of En by EUCLID:67;
A5: the TopStruct of TRn=TopSpaceMetr Euclid n by EUCLID:def 8;
then reconsider I=Int A as Subset of TopSpaceMetr En;
Int A in the topology of TopSpaceMetr En by A5,PRE_TOPC:def 2;
then I is open by PRE_TOPC:def 2;
then consider r be Real such that
A6: r>0 and
A7: Ball(P,r)c=I by A2,TOPMETR:15;
dist(P,P)<r by A6,METRIC_1:1;
then
A8: P in Ball(P,r) by METRIC_1:11;
set H=halfline(p,q);
reconsider AH=A/\H as bounded Subset of En by A4,JORDAN2C:11;
A9: Int A c=A by TOPS_1:16;
then consider W be Point of En such that
A10: W in (Fr A)/\H and
A11: for u,P be Point of Euclid n st P=p & u in AH holds
dist(P,u)<=dist(P,W) and
for r be Real st r>0 ex u be Point of En st u in AH & dist(W,u)<r
by A2,A3,A4,Lm3;
reconsider w=W as Point of TRn by EUCLID:67;
A12: W in Fr A by A10,XBOOLE_0:def 4;
W in H by A10,XBOOLE_0:def 4;
then consider Wr be Real such that
A13: W=(1-Wr)*p+Wr*q and
A14: Wr>=0;
A15: Fr A c=A by A1,TOPS_1:35;
A16: Fr A misses Ball(P,r) by A7,TOPS_1:39,XBOOLE_1:63;
(Fr A)/\H={W}
proof
assume(Fr A)/\H<>{W};
then consider u be object such that
A17: u in (Fr A)/\H and
A18: u<>W by A10,ZFMISC_1:35;
reconsider u as Point of TRn by A17;
A19: u in H by A17,XBOOLE_0:def 4;
then consider Ur be Real such that
A20: u=(1-Ur)*p+Ur*q and
A21: Ur>=0;
A22: |.Ur.|=Ur by A21,ABSVALUE:def 1;
reconsider U=u as Element of En by EUCLID:67;
(1-Ur)*p+Ur*q-p=Ur*(q-p) by Lm1;
then
A23: dist(U,P) = |.Ur*(q-p).| by A20,SPPOL_1:39
.= Ur*|.q-p.| by A22,TOPRNS_1:7;
set R=r*(Wr-Ur)/Wr;
reconsider b=Ball(U,R) as Subset of TopSpaceMetr En by A5,EUCLID:67;
set x=(Wr-Ur)/Wr;
b is open by TOPMETR:14;
then b in the topology of TRn by A5,PRE_TOPC:def 2;
then reconsider B=b as open Subset of TRn by PRE_TOPC:def 2;
A24: |.Wr.|=Wr by A14,ABSVALUE:def 1;
(1-Wr)*p+Wr*q-p=Wr*(q-p) by Lm1;
then
A25: dist(W,P) = |.Wr*(q-p).| by A13,SPPOL_1:39
.= Wr*|.q-p.| by A24,TOPRNS_1:7;
A26: u in Fr A by A17,XBOOLE_0:def 4;
then
A27: u in AH by A15,A19,XBOOLE_0:def 4;
P<>W by A16,A8,A12,XBOOLE_0:3;
then
A28: Wr>0 by A25,METRIC_1:7;
then
A29: 1-x = Wr/Wr-x by XCMPLX_1:60
.= Ur/Wr;
P<>u by A16,A8,A26,XBOOLE_0:3;
then Ur>0 by A23,METRIC_1:7;
then 1-x>=x-x by A28,A29;
then
A30: x in REAL & x<=1 by XREAL_0:def 1,XREAL_1:6;
A31: (1-Wr)*p+Wr*q=Wr*(q-p)+p by Th1;
A32: (1-Ur)*p+Ur*q=p+Ur*(q-p) by Th1;
then (1-Wr)*p+Wr*q-((1-Ur)*p+Ur*q)
= (p+Wr*(q-p)-p)-Ur*(q-p) by A31,RLVECT_1:27
.= Wr*(q-p)+(p-p)-Ur*(q-p) by RLVECT_1:def 3
.= Wr*(q-p)+0.TRn-Ur*(q-p) by RLVECT_1:5
.= Wr*(q-p)-Ur*(q-p)
.= (Wr-Ur)*(q-p) by RLVECT_1:35;
then
A33: dist(U,W) = |.(Wr-Ur)*(q-p).| by A13,A20,SPPOL_1:39
.= |.Wr-Ur.|*|.q-p.| by TOPRNS_1:7;
dist(U,W)>0 by A18,METRIC_1:7;
then |.q-p.|>0 by A33,XREAL_1:134;
then Ur<=Wr by A11,A23,A25,A27,XREAL_1:68;
then Wr-Ur>=0 by XREAL_1:48;
then
A34: |.Wr-Ur.|=Wr-Ur by ABSVALUE:def 1;
then
A35: Wr-Ur>0 by A18,A33,METRIC_1:7;
dist(U,U)=0 by METRIC_1:1;
then U in B by A6,A28,A35,METRIC_1:11;
then B\A<>{} by A26,TOPGEN_1:9;
then consider t be object such that
A36: t in B\A by XBOOLE_0:def 1;
A37: t in B by A36,XBOOLE_0:def 5;
reconsider t as Point of TRn by A36;
set z=p+Wr/(Wr-Ur)*(t-u);
reconsider Z=z as Point of En by EUCLID:67;
reconsider T=t as Point of En by EUCLID:67;
A38: dist(U,T)=|.u-t.| by SPPOL_1:39;
A39: Wr/(Wr-Ur)*R = Wr/Wr*(Wr-Ur)/(Wr-Ur)*r
.= (Wr-Ur)/(Wr-Ur)*r by A28,XCMPLX_1:88
.= r by A35,XCMPLX_1:88;
|.-Wr.|=--Wr by A28,ABSVALUE:def 1;
then
A40: (-Wr)/(Wr-Ur) in REAL & |.(-Wr)/(Wr-Ur).|=Wr/(Wr-Ur)
by A34,COMPLEX1:67,XREAL_0:def 1;
A41: (Ur/Wr)*(Wr*(q-p)) = (Ur/Wr*Wr)*(q-p) by RLVECT_1:def 7
.= (Wr/Wr*Ur)*(q-p)
.= Ur*(q-p) by A28,XCMPLX_1:88;
p-z =(p-p)-Wr/(Wr-Ur)*(t-u) by RLVECT_1:27
.= 0.TRn-Wr/(Wr-Ur)*(t-u) by RLVECT_1:15
.= -Wr/(Wr-Ur)*(t-u)
.= (-1)*(Wr/(Wr-Ur)*(t-u)) by RLVECT_1:16
.= ((-1)*(Wr/(Wr-Ur)))*(t-u) by RLVECT_1:def 7
.= (-Wr)/(Wr-Ur)*(t-u);
then
A42: dist(P,Z) = |.((-Wr)/(Wr-Ur))*(t-u).| by SPPOL_1:39
.= Wr/(Wr-Ur)*|.t-u.| by A40,TOPRNS_1:7;
dist(U,T)<R by A37,METRIC_1:11;
then Wr/(Wr-Ur)*|.u-t.|<r by A28,A35,A38,A39,XREAL_1:68;
then dist(P,Z)<r by A38,A42,SPPOL_1:39;
then Z in Ball(P,r) by METRIC_1:11;
then
A43: Z in I by A7;
x*(Wr/(Wr-Ur)*(t-u)) = x*(Wr/(Wr-Ur))*(t-u) by RLVECT_1:def 7
.= (Wr-Ur)/(Wr-Ur)*Wr/Wr*(t-u)
.= Wr/Wr*(t-u) by A35,XCMPLX_1:88
.= 1 *(t-u) by A28,XCMPLX_1:60
.= t-u by RLVECT_1:def 8;
then x*z=x*p+(t-u) by RLVECT_1:def 5;
then x*z+(1-x)*w
= t-u+x*p+((1-x)*p+Ur*(q-p)) by A13,A29,A31,A41,RLVECT_1:def 5
.= t-u+x*p+(1-x)*p+Ur*(q-p) by RLVECT_1:def 3
.= t-u+(x*p+(1-x)*p)+Ur*(q-p) by RLVECT_1:def 3
.= t-u+(x+(1-x))*p+Ur*(q-p) by RLVECT_1:def 6
.= t-u+p+Ur*(q-p) by RLVECT_1:def 8
.= t-u+u by A20,A32,RLVECT_1:def 3
.= t-(u-u) by RLVECT_1:29
.= t-0.TRn by RLVECT_1:15
.= t;
then t in A by A15,A9,A12,A28,A30,A35,A43,RLTOPSP1:def 1;
hence contradiction by A36,XBOOLE_0:def 5;
end;
hence thesis by A10;
end;
Lm4: for n be Element of NAT st n>0
for A be convex Subset of TOP-REAL n st A is compact & 0*n in Int A
ex h be Function of(TOP-REAL n) |A,Tdisk(0.TOP-REAL n,1) st
h is being_homeomorphism & h.:Fr A=Sphere(0.TOP-REAL n,1)
proof
let n be Element of NAT;
set TRn=TOP-REAL n,En=Euclid n,cTRn=the carrier of TRn;
assume
A1: n>0;
cTRn\{0.TRn}={0.TRn}` by SUBSET_1:def 4;
then reconsider cTR0=cTRn\{0.TRn} as non empty open Subset of TRn by A1;
set CL=cl_Ball(0.TRn,1),S=Sphere(0.TRn,1);
set TRn0=TRn|cTR0;
set nN=n NormF;
set En=Euclid n;
set I0=0.TRn.-->0.TRn;
let A be convex Subset of TRn such that
A2: A is compact and
A3: 0*n in Int A;
A4: A is non empty by A3;
reconsider 0TRn=0.TRn as Point of En by EUCLID:67;
A5: 0*n=0.TRn by EUCLID:70;
then consider e be Real such that
A6: e>0 and
A7: Ball(0TRn,e)c=A by A3,GOBOARD6:5;
Fr A misses Int A by TOPS_1:39;
then
A8: not 0*n in Fr A by A3,XBOOLE_0:3;
then
A9: (Fr A)\{0.TRn}=Fr A by A5,ZFMISC_1:57;
set TM=TopSpaceMetr En;
A10: [#]TRn0=cTR0 by PRE_TOPC:def 5;
A11: the TopStruct of TRn=TM by EUCLID:def 8;
then reconsider a=A as Subset of TM;
reconsider aa=a as Subset of En by EUCLID:67;
TRn|A is compact by A2;
then TM|a is compact by A11,PRE_TOPC:36;
then
A12: a is compact by A4,COMPTS_1:3;
A13: for p be Point of TRn st p<>0.TRn ex x be Point of TRn st
(Fr A)/\halfline(0.TRn,p)={x}
proof
let p be Point of TRn such that
A14: p<>0.TRn;
A15: A/\halfline(0.TRn,p)c=aa by XBOOLE_1:17;
then reconsider F=A/\halfline(0.TRn,p) as Subset of En by XBOOLE_1:1;
A16: 0.TRn in Int A by A3,EUCLID:70;
F is bounded by A12,A15,HAUSDORF:18,TBSP_1:14;
then A/\halfline(0.TRn,p) is bounded by JORDAN2C:11;
hence thesis by A2,A14,A16,Th4;
end;
Fr A is non empty
proof
set q=the Element of cTR0;
q<>0.TRn by ZFMISC_1:56;
then ex x be Point of TRn st (Fr A)/\halfline(0.TRn,q)={x} by A13;
hence thesis;
end;
then reconsider FrA=Fr A as non empty Subset of TRn0 by A10,A9,XBOOLE_1:33;
A17: Fr A c=A by A2,TOPS_1:35;
set TS=TRn|S;
reconsider I=incl TRn0 as continuous Function of TRn0,TRn by TMAP_1:87;
A18: [#]TS=S by PRE_TOPC:def 5;
A19: nN|TRn0=nN|the carrier of TRn0 by TMAP_1:def 4;
not 0 in rng(nN|TRn0)
proof
assume 0 in rng(nN|TRn0);
then consider x be object such that
A20: x in dom(nN|TRn0) and
A21: (nN|TRn0).x=0 by FUNCT_1:def 3;
x in dom nN by A19,A20,RELAT_1:57;
then reconsider x as Element of TRn;
reconsider X=x as Element of REAL n by EUCLID:22;
0 = nN.x by A19,A20,A21,FUNCT_1:47
.= |.X.| by JGRAPH_4:def 1;
then x=0.TRn by A5,EUCLID:8;
then x in {0.TRn} by TARSKI:def 1;
hence contradiction by A10,A20,XBOOLE_0:def 5;
end;
then reconsider nN0=nN|TRn0 as non-empty continuous Function of TRn0,R^1
by RELAT_1:def 9;
reconsider b=I</>nN0 as Function of TRn0,TRn by TOPREALC:46;
A22: dom b = cTR0 by A10,FUNCT_2:def 1;
A23: for p be Point of TRn st p in cTR0 holds
b.p=1/|.p.|*p & |.(1/|.p.|)*p.|=1
proof
let p be Point of TRn;
assume
A24: p in cTR0;
then
A25: nN0.p=nN.p & I.p=p by A10,A19,FUNCT_1:49,TMAP_1:84;
thus b.p = I.p(/)nN0.p by A22,A24,VALUED_2:72
.= p(/)|.p.| by A25,JGRAPH_4:def 1
.= 1/|.p.|(#)p by VALUED_2:def 32
.= 1/|.p.|*p;
A26: |.1/|.p.|.|=1/|.p.| & p<>0.TRn by A24,ABSVALUE:def 1,ZFMISC_1:56;
thus|.(1/|.p.|)*p.| = |.1/|.p.|.|*|.p.| by TOPRNS_1:7
.= 1 by A26,TOPRNS_1:24,XCMPLX_1:87;
end;
A27: rng b c=S
proof
let y be object;
assume y in rng b;
then consider x be object such that
A28: x in dom b and
A29: b.x=y by FUNCT_1:def 3;
reconsider x as Point of TRn by A22,A28;
A30: (1/|.x.|)*x-0.TRn=(1/|.x.|)*x & |.(1/|.x.|)*x.|=1 by A10,A23,A28;
y = 1/|.x.|*x by A10,A23,A28,A29;
hence thesis by A30;
end;
then reconsider B=b as Function of TRn0,TS by A10,A18,A22,FUNCT_2:2;
A31: I0={0.TRn}-->0.TRn by FUNCOP_1:def 9;
then
A32: dom I0={0.TRn};
set FRA=TRn0|FrA,H=b|FRA;
A33: dom H=the carrier of FRA by FUNCT_2:def 1;
A34: H=b|the carrier of FRA by TMAP_1:def 4;
then
A35: rng H c=rng b by RELAT_1:70;
then
A36: rng H c=S by A27;
reconsider H as Function of FRA,TS by A18,A27,A33,A35,FUNCT_2:2,XBOOLE_1:1;
A37: [#]FRA=FrA by PRE_TOPC:def 5;
A38: (Fr A)\{0.TRn}c=cTR0 by XBOOLE_1:33;
S c=rng H
proof
let x be object;
assume x in S;
then consider p be Point of TRn such that
A39: x=p and
A40: |.p-0.TRn.|=1;
p <> 0.TRn by A5,A40;
then consider q be Point of TRn such that
A41: FrA/\halfline(0.TRn,p)={q} by A13;
A42: q in {q} by TARSKI:def 1;
then
A43: q in FrA by A41,XBOOLE_0:def 4;
then
A44: b.q=1/|.q.|*q & b.q=H.q by A9,A23,A34,A37,A38,FUNCT_1:49;
q in halfline(0.TRn,p) by A41,A42,XBOOLE_0:def 4;
then halfline(0.TRn,p)=halfline(0.TRn,q) by A5,A8,A43,TOPREAL9:31;
then
A45: 1/|.q.|*q in halfline(0.TRn,p) by Lm2;
A46: 1/|.q.|*q-0.TRn=1/|.q.|*q & p in halfline(0.TRn,p) by TOPREAL9:28;
H.q in rng H & |.1/|.q.|*q.|=1 by A9,A23,A33,A37,A38,A43,FUNCT_1:def 3;
hence thesis by A39,A40,A45,A46,A44,Th2;
end;
then
A47: S=rng H by A36,XBOOLE_0:def 10;
(Fr A) \ {0.TRn} c= cTR0 by XBOOLE_1:33;
then
A48: dom H=[#]FRA & TRn| (Fr A)=FRA by A9,FUNCT_2:def 1,PRE_TOPC:7;
for x1,x2 be object st x1 in dom H & x2 in dom H & H.x1=H.x2 holds x1=x2
proof
let x1,x2 be object such that
A49: x1 in dom H and
A50: x2 in dom H and
A51: H.x1=H.x2;
A52: x2 in dom b by A34,A50,RELAT_1:57;
A53: x1 in dom b by A34,A49,RELAT_1:57;
then reconsider p1=x1,p2=x2 as Point of TRn by A22,A52;
A54: b.p1=1/|.p1.|*p1 by A10,A23,A53;
x2<>0.TRn by A10,A52,ZFMISC_1:56;
then consider q be Point of TRn such that
A55: (Fr A)/\halfline(0.TRn,p2)={q} by A13;
p2 in halfline(0.TRn,p2) by TOPREAL9:28;
then p2 in {q} by A37,A50,A55,XBOOLE_0:def 4;
then
A56: p2=q by TARSKI:def 1;
|.(1/|.p2.|)*p2.|=1 by A10,A23,A52;
then
A57: 1/|.p2.|*p2<>0.TRn by TOPRNS_1:23;
A58: 0.TRn+1/|.p2.|*p2=1/|.p2.|*p2;
A59: b.p2=1/|.p2.|*p2 by A10,A23,A52;
A60: H.x1=b.x1 & H.x2=b.x2 by A34,A49,A50,FUNCT_1:47;
(1-1/|.p1.|)*0.TRn = 0.TRn;
then
A61: 1/|.p1.|*p1 in halfline(0.TRn,p1) by A51,A54,A58,A59,A60;
(1-1/|.p2.|)*0.TRn=0.TRn;
then 1/|.p2.|*p2 in halfline(0.TRn,p2) by A58;
then halfline(0.TRn,p2)
= halfline(0.TRn,1/|.p1.|*p1) by A51,A54,A57,A59,A60,TOPREAL9:31
.= halfline(0.TRn,p1) by A51,A54,A57,A59,A60,A61,TOPREAL9:31;
then p1 in halfline(0.TRn,p2) by TOPREAL9:28;
then p1 in {q} by A37,A49,A55,XBOOLE_0:def 4;
hence thesis by A56,TARSKI:def 1;
end;
then
A62: H is one-to-one by FUNCT_1:def 4;
then H is being_homeomorphism by A2,A18,A47,A48,COMPTS_1:17,PRE_TOPC:27;
then reconsider H1=H" as continuous Function of TS,FRA by TOPS_2:def 5;
reconsider HH=H as Function;
set nN0F=nN0|FRA;
reconsider H1B=H1*B as Function of TRn0,FRA by A47;
reconsider NH1B=nN0F*H1B as Function of TRn0,R^1;
A63: nN0F=nN0|the carrier of FRA by TMAP_1:def 4;
then rng NH1B c=rng nN0F & rng nN0F c=rng nN0 by RELAT_1:26,70;
then rng NH1B c=rng nN0;
then
A64: not 0 in rng NH1B;
(B is continuous) & S is non empty by A27,PRE_TOPC:27;
then reconsider NH1B as non-empty continuous Function of TRn0,R^1
by A64,RELAT_1:def 9;
reconsider G=I</>NH1B as Function of TRn0,TRn by TOPREALC:46;
A65: dom G=cTR0 by A10,FUNCT_2:def 1;
A66: dom nN0F=FrA by A37,FUNCT_2:def 1;
A67: for p be Point of TRn st p in cTR0 ex Hp be Point of TRn st Hp=H1B.p &
Hp in FrA & G.p=1/|.Hp.|*p & |.Hp.|>0
proof
let p be Point of TRn;
assume
A68: p in cTR0;
then
A69: p in dom NH1B by A10,FUNCT_2:def 1;
then
A70: H1B.p in dom nN0F by FUNCT_1:11;
then reconsider Hp=H1B.p as Point of TRn by A66;
A71: nN0F.Hp=nN0.Hp by A63,A70,FUNCT_1:49;
A72: nN.Hp=|.Hp.| & nN0.Hp=nN.Hp by A19,A66,A70,FUNCT_1:49,JGRAPH_4:def 1;
take Hp;
thus Hp=H1B.p & Hp in FrA by A37,A70;
A73: NH1B.p=nN0F.(H1B.p) by A69,FUNCT_1:12;
thus G.p = I.p(/)NH1B.p by A65,A68,VALUED_2:72
.= p(/)|.Hp.| by A10,A68,A73,A71,A72,TMAP_1:84
.= 1/|.Hp.|(#)p by VALUED_2:def 32
.= 1/|.Hp.|*p;
|.Hp.|<>0 by A63,A70,A73,A72,FUNCT_1:49;
hence thesis;
end;
A74: not 0.TRn in rng G
proof
assume 0.TRn in rng G;
then consider p be object such that
A75: p in dom G and
A76: G.p=0.TRn by FUNCT_1:def 3;
reconsider p as Point of TRn by A65,A75;
consider Hp be Point of TRn such that
Hp=H1B.p and
Hp in FrA and
A77: G.p=1/|.Hp.|*p & |.Hp.|>0 by A10,A67,A75;
p<>0.TRn by A10,A75,ZFMISC_1:56;
hence contradiction by A76,A77,RLVECT_1:11;
end;
A78: for x1,x2 be set st x1 in dom I0 & x2 in dom G\dom I0 holds I0.x1<>G.x2
proof
let x1,x2 be set such that
A79: x1 in dom I0 and
A80: x2 in dom G\dom I0;
x1=0.TRn by A79,TARSKI:def 1;
then
A81: I0.x1=0.TRn by FUNCOP_1:72;
x2 in dom G by A80,XBOOLE_0:def 5;
hence thesis by A74,A81,FUNCT_1:def 3;
end;
H is onto by A18,A47,FUNCT_2:def 3;
then
A82: H"=HH" by A62,TOPS_2:def 4;
A83: for p be Point of TRn st p in cTR0 holds
(Fr A)/\halfline(0.TRn,p)={H1B.p}
proof
let p be Point of TRn;
assume
A84: p in cTR0;
then
A85: p in dom H1B by A10,FUNCT_2:def 1;
then
A86: H1B.p=H1.(B.p) by FUNCT_1:12;
B.p in dom H1 by A85,FUNCT_1:11;
then consider x be object such that
A87: x in dom H and
A88: H.x=B.p by A18,A47,FUNCT_1:def 3;
reconsider x as Point of TRn by A33,A37,A87;
A89: H.x=b.x by A34,A87,FUNCT_1:47;
set xp=|.x.|/|.p.|;
A90: x in FrA by A37,A87;
then
A91: b.x=1/|.x.|*x by A9,A23,A38;
|.(1/|.x.|)*x.|=1 by A9,A23,A38,A90;
then (1/|.x.|)*x<>0.TRn by TOPRNS_1:23;
then 1/|.x.|<>0 by RLVECT_1:10;
then |.x.|>0;
then 1 = |.x.|/|.x.| by XCMPLX_1:60
.= |.x.|*(1/|.x.|);
then x = (|.x.|*(1/|.x.|))*x by RLVECT_1:def 8
.= |.x.|*(1/|.x.|*x) by RLVECT_1:def 7
.= |.x.|*(1/|.p.|*p) by A23,A84,A88,A89,A91
.= xp*p by RLVECT_1:def 7;
then x in halfline(0.TRn,p) by Lm2;
then
A92: x in (Fr A)/\halfline(0.TRn,p) by A37,A87,XBOOLE_0:def 4;
p<>0.TRn by A84,ZFMISC_1:56;
then consider y be Point of TRn such that
A93: (Fr A)/\halfline(0.TRn,p)={y} by A13;
H1.(B.p)=x by A62,A82,A87,A88,FUNCT_1:34;
hence thesis by A86,A92,A93,TARSKI:def 1;
end;
for x1,x2 be object st x1 in dom G & x2 in dom G & G.x1=G.x2 holds x1=x2
proof
let x1,x2 be object such that
A94: x1 in dom G and
A95: x2 in dom G and
A96: G.x1=G.x2;
reconsider p1=x1,p2=x2 as Point of TRn by A65,A94,A95;
consider Hp1 be Point of TRn such that
A97: Hp1=H1B.p1 and
Hp1 in FrA and
A98: G.p1=1/|.Hp1.|*p1 and
A99: |.Hp1.|>0 by A10,A67,A94;
A100: FrA/\halfline(0.TRn,p1)={Hp1} by A10,A83,A94,A97;
consider Hp2 be Point of TRn such that
A101: Hp2=H1B.p2 and
Hp2 in FrA and
A102: G.p2=1/|.Hp2.|*p2 and
|.Hp2.|>0 by A10,A67,A95;
p1<>0.TRn by A10,A94,ZFMISC_1:56;
then
A103: 1/|.Hp1.|*p1<>0.TRn by A99,RLVECT_1:11;
then halfline(0.TRn,p1) = halfline(0.TRn,1/|.Hp1.|*p1) by Lm2,TOPREAL9:31
.= halfline(0.TRn,p2)
by A96,A98,A102,A103,Lm2,TOPREAL9:31;
then Hp1 in {Hp1} & {Hp1}={Hp2} by A10,A83,A95,A100,A101,TARSKI:def 1;
then 1/|.Hp1.|=1/|.Hp2.| by TARSKI:def 1;
hence thesis by A96,A98,A99,A102,RLVECT_1:36;
end;
then
A104: G is one-to-one by FUNCT_1:def 4;
set G0=G+*I0;
A105: dom G0 = dom G\/dom I0 by FUNCT_4:def 1
.= cTR0\/{0.TRn} by A31,A65
.= cTRn by ZFMISC_1:116;
A106: for p,Hp be Point of TRn st p in cTR0 & Hp=H1B.p holds
p=G.(|.Hp.|*p) & (|.Hp.|*p) in dom G
proof
let p,Hp1 be Point of TRn such that
A107: p in cTR0 and
A108: Hp1=H1B.p;
reconsider p as Point of TRn;
consider Hp be Point of TRn such that
A109: Hp=H1B.p and
Hp in FrA and
G.p=1/|.Hp.|*p and
A110: |.Hp.|>0 by A67,A107;
set Hpp=|.Hp.|*p;
p<>0.TRn by A107,ZFMISC_1:56;
then
A111: Hpp<>0.TRn by A110,RLVECT_1:11;
then
A112: Hpp in cTR0 by ZFMISC_1:56;
then consider HP be Point of TRn such that
A113: HP=H1B.Hpp and
HP in FrA and
A114: G.Hpp=1/|.HP.|*Hpp and
|.HP.|>0 by A67;
A115: Hp in {Hp} by TARSKI:def 1;
{HP} = (Fr A)/\halfline(0.TRn,Hpp) by A83,A112,A113
.= (Fr A)/\halfline(0.TRn,p) by A111,Lm2,TOPREAL9:31
.= {Hp} by A83,A107,A109;
then G.Hpp = 1/|.Hp.|*(|.Hp.|*p) by A114,A115,TARSKI:def 1
.= (|.Hp.|/|.Hp.|)*p by RLVECT_1:def 7
.= 1 *p by A110,XCMPLX_1:60
.= p by RLVECT_1:def 8;
hence thesis by A65,A108,A109,A111,ZFMISC_1:56;
end;
A116: S c=G.:FrA
proof
let p be object;
assume
A117: p in S;
then reconsider p as Point of TRn;
|.p.|=1 by A117,TOPREAL9:12;
then p<>0.TRn by TOPRNS_1:23;
then
A118: p in cTR0 by ZFMISC_1:56;
then consider Hp be Point of TRn such that
A119: Hp=H1B.p and
A120: Hp in FrA and
G.p=1/|.Hp.|*p and
|.Hp.|>0 by A67;
set Hpp=|.Hp.|*p;
A121: p=G.Hpp & Hpp in dom G by A106,A118,A119;
Hp in {Hp} & (Fr A)/\halfline(0.TRn,p)={Hp}
by A83,A118,A119,TARSKI:def 1;
then
A122: Hp in halfline(0.TRn,p) by XBOOLE_0:def 4;
A123: Hp-0.TRn=Hp;
|.|.Hp.|.|=|.Hp.| by ABSVALUE:def 1;
then
A124: |.Hpp.| = |.Hp.|*|.p.| by TOPRNS_1:7
.= |.Hp.|*1 by A117,TOPREAL9:12;
Hpp-0.TRn=Hpp & Hpp in halfline(0.TRn,p) by Lm2;
then Hp=Hpp by A124,A122,A123,Th2;
hence thesis by A120,A121,FUNCT_1:def 6;
end;
A125: 0.TRn in {0.TRn} by TARSKI:def 1;
then
A126: I0.(0.TRn)=0.TRn by A31,FUNCOP_1:7;
rng I0={0.TRn} by A31,FUNCOP_1:8;
then rng G0=rng G\/{0.TRn} by A32,A65,NECKLACE:6,XBOOLE_1:79;
then reconsider G1=G0 as one-to-one Function of TRn,TRn
by A105,A78,A104,FUNCT_2:2,TOPMETR2:1;
A127: G1.0.TRn=I0.(0.TRn) by A32,A125,FUNCT_4:13;
A128: G.:FrA c=S
proof
let y be object;
assume y in G.:FrA;
then consider p be object such that
A129: p in dom G and
A130: p in FrA and
A131: G.p=y by FUNCT_1:def 6;
reconsider p as Point of TRn by A130;
consider Hp be Point of TRn such that
A132: Hp=H1B.p and
Hp in FrA and
A133: G.p=1/|.Hp.|*p and
A134: |.Hp.|>0 by A10,A67,A129;
p in halfline(0.TRn,p) by TOPREAL9:28;
then
A135: p in FrA/\halfline(0.TRn,p) by A130,XBOOLE_0:def 4;
FrA/\halfline(0.TRn,p)={Hp} by A10,A83,A129,A132;
then
A136: p=Hp by A135,TARSKI:def 1;
|.1/|.Hp.|.|=1/|.Hp.| by ABSVALUE:def 1;
then |.1/|.Hp.|*p.| = (1/|.Hp.|)*|.Hp.| by A136,TOPRNS_1:7
.= 1 by A134,XCMPLX_1:106;
then |.1/|.Hp.|*p-0.TRn.|=1;
hence thesis by A131,A133;
end;
set TRnCL=TRn|CL;
set TRnA=TRn|A;
A137: Int A c=A by TOPS_1:16;
set GA=G1|TRnA;
A138: G1|TRnA=G1|the carrier of TRnA by TMAP_1:def 4;
A139: [#]TRnA=A by PRE_TOPC:def 5;
then
A140: dom GA=A by FUNCT_2:def 1;
A141: dom GA=the carrier of TRnA by FUNCT_2:def 1;
A142: cl_Ball(0.TRn,1)c=rng GA
proof
let p be object;
assume
A143: p in cl_Ball(0.TRn,1);
then reconsider p as Point of TRn;
per cases;
suppose p=0.TRn;
then p=GA.0.TRn by A3,A137,A5,A126,A138,A139,A127,FUNCT_1:49;
hence thesis by A3,A137,A5,A139,A141,FUNCT_1:def 3;
end;
suppose
A144: p<>0.TRn;
set h=halfline(0.TRn,p);
A145: p in cTR0 by A144,ZFMISC_1:56;
then consider Hp be Point of TRn such that
A146: Hp=H1B.p and
A147: Hp in FrA and
G.p=1/|.Hp.|*p and
A148: |.Hp.|>0 by A67;
A149: |.|.Hp.|.|=|.Hp.| by ABSVALUE:def 1;
Fr A/\h={Hp} by A83,A145,A146;
then Hp in Fr A/\h by TARSKI:def 1;
then
A150: Hp in h by XBOOLE_0:def 4;
Hp<>0.TRn by A148,TOPRNS_1:23;
then h=halfline(0.TRn,Hp) by A150,TOPREAL9:31;
then
A151: |.p.|*Hp in h by Lm2;
|.p.|<=1 by A143,TOPREAL9:11;
then (1- |.p.|)*0.TRn=0.TRn & |.p.|*Hp+(1- |.p.|)*0.TRn in A
by A3,A137,A5,A17,A147,RLTOPSP1:def 1;
then |.p.|*Hp in dom GA by A140;
then
A152: GA.(|.p.|*Hp) in rng GA & GA.(|.p.|*Hp)=G1.(|.p.|*Hp)
by A138,FUNCT_1:47,def 3;
A153: |.Hp.|*p in h by Lm2;
(|.Hp.|*p) in dom G by A106,A145,A146;
then |.Hp.|*p<>0.TRn by A10,ZFMISC_1:56;
then not |.Hp.|*p in dom I0 by TARSKI:def 1;
then
A154: G.(|.Hp.|*p)=G1.(|.Hp.|*p) by FUNCT_4:11;
|.|.p.|.|=|.p.| by ABSVALUE:def 1;
then |.|.p.|*Hp.| = |.p.|*|.Hp.| by TOPRNS_1:7
.= |.|.Hp.|*p.| by A149,TOPRNS_1:7;
then
A155: |.|.p.|*Hp-0.TRn.| = |.|.Hp.|*p.|
.= |.|.Hp.|*p-0.TRn.|;
p=G.(|.Hp.|*p) by A106,A145,A146;
hence thesis by A151,A154,A155,A152,A153,Th2;
end;
end;
rng GA c=cl_Ball(0.TRn,1)
proof
let x be object;
assume x in rng GA;
then consider p be object such that
A156: p in dom GA and
A157: GA.p=x by FUNCT_1:def 3;
reconsider p as Point of TRn by A140,A156;
A158: GA.p=G1.p by A138,A156,FUNCT_1:47;
A159: G1.p-0.TRn=G1.p;
per cases;
suppose p=0.TRn;
then G1.p=0.TRn by A31,A125,A127,FUNCOP_1:7;
then |.G1.p-0.TRn.|=0 by TOPRNS_1:23;
hence thesis by A157,A158;
end;
suppose
A160: p<>0.TRn;
set h=halfline(0.TRn,p);
A161: A/\h c=aa by XBOOLE_1:17;
then reconsider F=A/\h as Subset of En by XBOOLE_1:1;
F is bounded by A12,A161,HAUSDORF:18,TBSP_1:14;
then A/\h is bounded by JORDAN2C:11;
then consider w be Point of En such that
A162: w in (Fr A)/\h and
A163: for u,P be Point of En st P=0.TRn & u in A/\h holds
dist(P,u)<=dist(P,w) and
for r st r>0 ex u be Point of En st u in A/\h & dist(w,u)<r
by A3,A137,A5,A160,Lm3;
reconsider P=p as Point of En by EUCLID:67;
p in h by TOPREAL9:28;
then
A164: p in A/\h by A139,A156,XBOOLE_0:def 4;
A165: not p in dom I0 by A160,TARSKI:def 1;
A166: p in cTR0 by A160,ZFMISC_1:56;
then consider Hp be Point of TRn such that
A167: Hp=H1B.p and
Hp in FrA and
A168: G.p=1/|.Hp.|*p and
|.Hp.|>0 by A67;
|.1/|.Hp.|.|=1/|.Hp.| by ABSVALUE:def 1;
then
A169: |.1/|.Hp.|*p.|=|.p.|/|.Hp.| by TOPRNS_1:7;
(Fr A)/\h={Hp} by A83,A166,A167;
then w=Hp by A162,TARSKI:def 1;
then
A170: dist(0TRn,w) = |.0.TRn-Hp.| by SPPOL_1:39
.= |.-Hp.|
.= |.Hp.| by TOPRNS_1:26;
dist(0TRn,P) = |.0.TRn-p.| by SPPOL_1:39
.= |.-p.|
.= |.p.| by TOPRNS_1:26;
then |.1/|.Hp.|*p.|<=1 by A163,A164,A169,A170,XREAL_1:183;
then |.G1.p.|<=1 by A165,A168,FUNCT_4:11;
hence thesis by A157,A158,A159;
end;
end;
then
A171: rng GA=CL by A142,XBOOLE_0:def 10;
A172: [#]TRnCL=CL by PRE_TOPC:def 5;
then reconsider GA as Function of TRnA,TRnCL by A139,A140,A171,FUNCT_2:1;
set e2=e/2;
A173: GA is one-to-one by A138,FUNCT_1:52;
A174: e2<e by A6,XREAL_1:216;
A175: G1 is continuous
proof
let x being Point of TRn,U being a_neighborhood of G1.x;
per cases;
suppose
A176: x<>0.TRn;
then
A177: x in dom G by A65,ZFMISC_1:56;
then reconsider X=x as Point of TRn0;
not x in dom I0 by A176,TARSKI:def 1;
then
A178: G.x=G1.x by FUNCT_4:11;
then
A179: G1.x<>0.TRn by A74,A177,FUNCT_1:def 3;
then reconsider G1x=G1.x as Point of TRn0 by A10,ZFMISC_1:56;
G1.x in cTR0 by A179,ZFMISC_1:56;
then cTR0 is a_neighborhood of G1.x by CONNSP_2:3;
then cTR0/\U is a_neighborhood of G1.x by CONNSP_2:2;
then consider H be a_neighborhood of X such that
A180: G.:H c=cTR0/\U by A178,BORSUK_1:def 1;
reconsider h=H as Subset of TRn by A10,XBOOLE_1:1;
reconsider h as a_neighborhood of x by CONNSP_2:9;
{0.TRn}misses H by A10,XBOOLE_1:63,79;
then cTR0/\U c=U & G.:H=G1.:h by A31,BOOLMARK:3,XBOOLE_1:17;
hence thesis by A180,XBOOLE_1:1;
reconsider U1=cTR0/\U as Subset of TRn0 by A10,XBOOLE_1:17;
end;
suppose
A181: x=0.TRn;
reconsider 0TRn=0.TRn as Point of Euclid n by EUCLID:67;
A182: 0.TRn in Int(U) by A126,A127,A181,CONNSP_2:def 1;
then consider r be Real such that
A183: r>0 and
A184: Ball(0TRn,r)c=U by GOBOARD6:5;
reconsider B=Ball(0TRn,r*e2) as Subset of TRn by EUCLID:67;
0TRn in Int B by A6,A183,GOBOARD6:5;
then reconsider Bx=B as a_neighborhood of x by A181,CONNSP_2:def 1;
take Bx;
let y be object;
assume
A185: y in G1.:Bx;
then reconsider p=y as Point of TRn;
A186: Int U c=U by TOPS_1:16;
per cases;
suppose y=0.TRn;
hence y in U by A182,A186;
end;
suppose
A187: p<>0.TRn;
set PP=e2/|.p.|*p;
|.e2/|.p.|.|=e2/|.p.| by A6,ABSVALUE:def 1;
then
A188: |.PP.| = (e2/|.p.|)*|.p.| by TOPRNS_1:7
.= e2*(|.p.|/|.p.|)
.= e2*1 by A187,TOPRNS_1:24,XCMPLX_1:60
.= e2;
then |.PP-0.TRn.|<e by A174;
then
A189: PP in Ball(0.TRn,e);
set h=halfline(0.TRn,p);
A190: A/\h c=aa by XBOOLE_1:17;
then reconsider F=A/\h as Subset of En by XBOOLE_1:1;
F is bounded by A12,A190,HAUSDORF:18,TBSP_1:14;
then A/\h is bounded by JORDAN2C:11;
then consider w be Point of En such that
A191: w in (Fr A)/\h and
A192: for u,P be Point of En st P=0.TRn & u in A/\h holds
dist(P,u)<=dist (P,w) and
for r st r>0 ex u be Point of En st u in A/\h & dist(w,u)<r
by A3,A137,A5,A187,Lm3;
A193: p in cTR0 by A187,ZFMISC_1:56;
then consider Hp be Point of TRn such that
A194: Hp=H1B.p and
Hp in FrA and
G.p=1/|.Hp.|*p and
A195: |.Hp.|>0 by A67;
Fr A/\h={Hp} by A83,A193,A194;
then w=Hp by A191,TARSKI:def 1;
then
A196: dist(0TRn,w) = |.0.TRn-Hp.| by SPPOL_1:39
.= |.-Hp.|
.= |.Hp.| by TOPRNS_1:26;
set Hpp=|.Hp.|*p;
Hpp in dom G by A106,A193,A194;
then Hpp<>0.TRn by A10,ZFMISC_1:56;
then not Hpp in dom I0 by TARSKI:def 1;
then
A197: G.Hpp=G1.Hpp by FUNCT_4:11;
|.Hp.|=|.|.Hp.|.| by ABSVALUE:def 1;
then
A198: Bx=Ball(0.TRn,r*e2) & |.Hpp.|=|.Hp.|*|.p.|
by TOPREAL9:13,TOPRNS_1:7;
reconsider pp=PP as Point of En by EUCLID:67;
consider x be object such that
A199: x in dom G1 and
A200: x in Bx and
A201: G1.x=p by A185,FUNCT_1:def 6;
PP in h & Ball(0.TRn,e)=Ball(0TRn,e) by A6,Lm2,TOPREAL9:13;
then
A202: pp in A/\h by A7,A189,XBOOLE_0:def 4;
dist(0TRn,pp) = |.0.TRn-PP.| by SPPOL_1:39
.= |.-PP.|
.= e2 by A188,TOPRNS_1:26;
then e2/|.Hp.|<=1 by A192,A196,A202,XREAL_1:183;
then
A203: r*(e2/|.Hp.|)<=r*1 by A183,XREAL_1:64;
p=G.Hpp by A106,A193,A194;
then Hpp=x by A105,A197,A199,A201,FUNCT_1:def 4;
then |.p.|<(r*e2)/|.Hp.| by A195,A198,A200,TOPREAL9:10,XREAL_1:81;
then |.p.|<r by A203,XXREAL_0:2;
then |.p-0.TRn.|<r;
then p in Ball(0.TRn,r);
then p in Ball(0TRn,r) by TOPREAL9:13;
hence y in U by A184;
end;
end;
end;
GA.:FrA=G1.:FrA by A2,A138,A139,RELAT_1:129,TOPS_1:35;
then GA.:FrA=G.:FrA by A5,A8,A31,BOOLMARK:3,ZFMISC_1:50;
then
A204: GA.:FrA=S by A116,A128,XBOOLE_0:def 10;
dom GA=[#]TRnA & rng GA=[#]TRnCL by A142,A172,FUNCT_2:def 1,XBOOLE_0:def 10;
then GA is being_homeomorphism
by A2,A3,A137,A173,A175,COMPTS_1:17,PRE_TOPC:27;
hence thesis by A204;
end;
theorem Th5:
r > 0 implies Fr cl_Ball(p,r) = Sphere(p,r)
proof
set TR=TOP-REAL n;
assume
A1: r>0;
set CB=cl_Ball(p,r),B=Ball(p,r),S=Sphere(p,r);
reconsider tr=TR as TopSpace;
reconsider cb=CB as Subset of tr;
A2: B misses S by TOPREAL9:19;
A3: B\/S=CB by TOPREAL9:18;
A4: Int cb c=B
proof
reconsider ONE=1 as Real;
let x be object;
assume x in Int cb;
then consider Q be Subset of TR such that
A5: Q is open and
A6: Q c=CB and
A7: x in Q by TOPS_1:22;
reconsider q=x as Point of TR by A7;
consider w be positive Real such that
A8: Ball(q,w)c=Q by A5,A7,TOPS_4:2;
assume not x in B;
then q in Sphere(p,r) by A3,A6,A7,XBOOLE_0:def 3;
then
A9: |.q-p.|=r by TOPREAL9:9;
set w2=w/2;
set wr=(w2/r)*(q-p);
A10: |.w2/r.|=w2/r by A1,ABSVALUE:def 1;
A11: wr+q-p = wr+(q-p) by RLVECT_1:28
.= wr+ONE*(q-p) by RLVECT_1:def 8
.= (w2/r+ONE)*(q-p) by RLVECT_1:def 6;
|.wr+q-q.| = |.wr+(q-q).| by RLVECT_1:def 3
.= |.wr+0.TR.| by RLVECT_1:15
.= |.wr.|
.= (w2/r)*r by A9,A10,TOPRNS_1:7
.= w2 by A1,XCMPLX_1:87;
then |.wr+q-q.|<w by XREAL_1:216;
then wr+q in Ball(q,w);
then
A12: wr+q in Q by A8;
A13: w2/r+ONE = w2/r+r/r by A1,XCMPLX_1:60
.= (w2+r)/r;
A14: w2+r>0+r by XREAL_1:6;
|.(w2+r)/r.|=(w2+r)/r by A1,ABSVALUE:def 1;
then |.wr+q-p.| = (w2+r)/r*r by A9,A13,A11,TOPRNS_1:7
.= w2+r by A1,XCMPLX_1:87;
hence contradiction by A6,A12,A14,TOPREAL9:8;
end;
B c=Int cb by TOPREAL9:16,TOPS_1:24;
then Int cb=B by A4,XBOOLE_0:def 10;
then Fr CB=CB\B by TOPS_1:43;
hence thesis by A3,A2,XBOOLE_1:88;
end;
registration
let n be Element of NAT;
let A be bounded Subset of TOP-REAL n;
let p be Point of TOP-REAL n;
cluster p+A -> bounded;
coherence
proof
set TR=TOP-REAL n;
set En=Euclid n;
reconsider a=A as bounded Subset of En by JORDAN2C:11;
reconsider pA=p+A as Subset of En by EUCLID:67;
consider r be Real such that
A1: 0<r and
A2: for x,y be Point of En st x in a & y in a holds dist(x,y)<=r
by TBSP_1:def 7;
A3: pA={p+u where u is Element of TR:u in A} by RUSUB_4:def 8;
now let x,y be Point of En;
assume x in pA;
then consider px be Element of TR such that
A4: x=p+px and
A5: px in A by A3;
assume y in pA;
then consider py be Element of TR such that
A6: y=p+py and
A7: py in A by A3;
reconsider pX=px,pY=py as Point of En by EUCLID:67;
p+px-(p+py) = p+px-p-py by RLVECT_1:27
.= px-py by RLVECT_4:1;
then dist(x,y) = |.px-py.| by A4,A6,SPPOL_1:39
.= dist(pX,pY) by SPPOL_1:39;
hence dist(x,y)<=r by A2,A5,A7;
end;
then pA is bounded by A1,TBSP_1:def 7;
hence thesis by JORDAN2C:11;
end;
end;
begin :: Main Theorems
theorem Th6:
for n be Element of NAT
for A be convex Subset of TOP-REAL n st A is compact non boundary
ex h be Function of(TOP-REAL n) |A,Tdisk(0.TOP-REAL n,1) st
h is being_homeomorphism & h.:Fr A = Sphere(0.TOP-REAL n,1)
proof
let n be Element of NAT;
set TRn=TOP-REAL n;
let A be convex Subset of TRn such that
A1: A is compact non boundary;
Int A<>{} by A1,TOPS_1:48;
then consider p be object such that
A2: p in Int A by XBOOLE_0:def 1;
set TRnA=TRn|A;
reconsider p as Point of TRn by A2;
A3: Int A c=A by TOPS_1:16;
A4: A is non empty by A2;
per cases;
suppose
A5: n=0;
set T=Tdisk(0.TRn,1);
A6: {0.TRn} = the carrier of TRn by A5,EUCLID:22,77;
then
A7: A={0.TRn} by A4,ZFMISC_1:33;
then reconsider I=id(TRn|A) as Function of TRn|A,T by A6,ZFMISC_1:33;
take I;
A8: Fr A=A\Int A by A5,TOPS_1:43;
A9: Sphere(0.TRn,1)={}
proof
assume Sphere(0.TRn,1)<>{};
then Sphere(0.TRn,1)=A by A6,A7,ZFMISC_1:33;
then |.0.TRn.|=1 by A6,A7,TOPREAL9:12;
hence contradiction by TOPRNS_1:23;
end;
Int A=A by A2,A3,A7,ZFMISC_1:33;
then
A10: Fr A={} by A8,XBOOLE_1:37;
T=TRn|A by A6,A7,ZFMISC_1:33;
hence thesis by A10,A9;
end;
suppose
A11: n>0;
set T=transl(-p,TRn);
set TA=T.:A;
A12: TA=-p+A by RLTOPSP1:33;
then
A13: 0.TRn=0*n & TA is convex by CONVEX1:7,EUCLID:70;
reconsider TT=T|A as Function of TRnA,TRn|TA by JORDAN24:12;
A14: TT.:Int A=T.:Int A by RELAT_1:129,TOPS_1:16;
0.TRn=-p+p by RLVECT_1:5;
then
A15: 0.TRn in {-p+q where q is Element of TRn:q in Int A} by A2;
Int TA=-p+Int A by A12,RLTOPSP1:37;
then 0.TRn in Int TA by A15,RUSUB_4:def 8;
then consider h be Function of TRn|TA,Tdisk(0.TRn,1) such that
A16: h is being_homeomorphism and
A17: h.:Fr TA=Sphere(0.TRn,1) by A1,A11,A12,A13,Lm4;
reconsider hTT=h*TT as Function of TRn|A,Tdisk(0.TRn,1) by A4;
take hTT;
A18: Int TA = -p+Int A by A12,RLTOPSP1:37
.= T.:Int A by RLTOPSP1:33;
A19: TT is being_homeomorphism by JORDAN24:14;
then dom TT=[#]TRnA by TOPS_2:def 5;
then
A20: dom TT=A by PRE_TOPC:def 5;
thus hTT is being_homeomorphism by A4,A16,A19,TOPS_2:57;
rng TT=[#](TRn|TA) by A19,TOPS_2:def 5;
then A21: rng TT=TA by PRE_TOPC:def 5;
Fr A=A\Int A by A1,TOPS_1:43;
then
A22: TT.:Fr A=(TT.:A)\TT.:(Int A) by A19,FUNCT_1:64;
Fr TA = TA\Int TA by A1,A12,TOPS_1:43
.= TT.:Fr A by A18,A22,A20,A21,A14,RELAT_1:113;
hence hTT.:Fr A= Sphere(0.TRn,1) by A17,RELAT_1:126;
end;
end;
theorem Th7:
for A,B st A is compact non boundary & B is compact non boundary
ex h be Function of(TOP-REAL n) |A,(TOP-REAL n) |B st
h is being_homeomorphism & h.:Fr A = Fr B
proof
set T=TOP-REAL n;
let A,B be convex Subset of T such that
A1: A is compact non boundary and
A2: B is compact non boundary;
A3: (A is non empty) & B is non empty by A1,A2;
reconsider N=n as Element of NAT by ORDINAL1:def 12;
set TN=TOP-REAL N;
consider hA be Function of T|A,Tdisk(0.TN,1) such that
A4: hA is being_homeomorphism and
A5: hA.:Fr A=Sphere(0.T,1) by A1,Th6;
consider hB be Function of T|B,Tdisk(0.TN,1) such that
A6: hB is being_homeomorphism and
A7: hB.:Fr B=Sphere(0.T,1) by A2,Th6;
reconsider h=(hB")*hA as Function of T|A,T|B;
take h;
hB" is being_homeomorphism by A6,TOPS_2:56;
hence h is being_homeomorphism by A3,A4,TOPS_2:57;
A8: rng hB=[#]Tdisk(0.TN,1) by A6,TOPS_2:def 5;
dom hB=[#](T|B) by A6,TOPS_2:def 5;
then
A9: dom hB=B by PRE_TOPC:def 5;
the carrier of Tdisk(0.TN,1)=cl_Ball(0.TN,1) by BROUWER:3;
then
A10: Sphere(0.T,1) is Subset of Tdisk(0.TN,1) by TOPREAL9:17;
thus h.:Fr A = (hB").:Sphere(0.T,1) by A5,RELAT_1:126
.= hB"Sphere(0.T,1) by A6,A8,A10,TOPS_2:55
.= Fr B by A2,A6,A7,A9,FUNCT_1:94,TOPS_1:35;
end;
::$N Brouwer fixed-point theorem
::$L https://en.wikipedia.org/wiki/Brouwer_fixed-point_theorem Brouwer fixed-point theorem
theorem Th8:
for A st A is compact non boundary
for h be continuous Function of(TOP-REAL n) |A,(TOP-REAL n) |A
holds h is with_fixpoint
proof
set T=TOP-REAL n;
consider I be affinely-independent Subset of T such that
{}T c=I and
I c=[#]T and
A1: Affin I=Affin[#]T by RLAFFIN1:60;
reconsider TT=T as non empty RLSStruct;
reconsider i=I as Subset of TT;
set II=Int i;
A2: I is non empty by A1;
then
A3: II is non empty by RLAFFIN2:20;
reconsider ii=II as Subset of T;
A4: Int ii c=Int conv I by RLAFFIN2:5,TOPS_1:19;
let A be convex Subset of T such that
A5: A is compact non boundary;
A6: A is non empty by A5;
let h be continuous Function of T|A,T|A;
[#]T is Affine by RUSUB_4:22;
then dim T=n & Affin[#]T=[#]T by RLAFFIN1:50,RLAFFIN3:4;
then
A7: card I=n+1 by A1,RLAFFIN3:6;
then ii is open by RLAFFIN3:33;
then conv I is non boundary by A3,A4,TOPS_1:23;
then consider f be Function of T|A,T|conv I such that
A8: f is being_homeomorphism and
f.:Fr A=Fr conv I by A5,Th7;
reconsider fhf=f*(h*(f")) as Function of T|conv I,T|conv I by A6;
f" is continuous by A8,TOPS_2:def 5;
then consider p be Point of T such that
A9: p in dom fhf and
A10: fhf.p=p by A7,A2,A8,A6,SIMPLEX2:23;
A11: p in dom(h*(f")) by A9,FUNCT_1:11;
reconsider F=f as Function;
A12: rng f=[#](T|conv I) by A8,TOPS_2:def 5;
A13: f"=F" by A8,TOPS_2:def 4;
consider x be object such that
A14: x in dom F and
A15: F.x=p by A12,A9,FUNCT_1:def 3;
(F").p=x by A8,A14,A15,FUNCT_1:34;
then (h*(f")).p=h.x by A11,A13,FUNCT_1:12;
then
A16: p=f.(h.x) by A9,A10,FUNCT_1:12;
A17: dom f=[#](T|A) by A8,TOPS_2:def 5;
then
A18: x in dom h by A14,FUNCT_2:52;
then h.x in rng h by FUNCT_1:def 3;
then h.x=x by A8,A17,A14,A15,A16,FUNCT_1:def 4;
then x is_a_fixpoint_of h by A18,ABIAN:def 3;
hence thesis by ABIAN:def 5;
end;
Lm5: cl_Ball(0.TOP-REAL n,1) is non boundary
proof
set TR=TOP-REAL n;
reconsider tr=TR as TopStruct;
reconsider cB=cl_Ball(0.TR,1) as Subset of tr;
Ball(0.TR,1)c=Int cB by TOPREAL9:16,TOPS_1:24;
hence thesis;
end;
reconsider jj=1 as Real;
Lm6: for n be Element of NAT for X be non empty SubSpace of Tdisk(0.TOP-REAL n,
1) st X=Tcircle(0.TOP-REAL n,1) holds not X is_a_retract_of Tdisk(0.TOP-REAL n,
1)
proof
let n be Element of NAT;
set TR=TOP-REAL n;
set Td=Tdisk(0.TR,1);
A1: Sphere(0.TR,1)c=cl_Ball(0.TR,1) by TOPREAL9:17;
set M=mlt(-jj,TR);
let X be non empty SubSpace of Tdisk(0.TR,1) such that
A2: X=Tcircle(0.TR,1);
A3: the carrier of X=Sphere(0.TR,1) by A2,TOPREALB:9;
assume X is_a_retract_of Td;
then consider F be continuous Function of Td,X such that
A4: F is being_a_retraction;
A5: the carrier of Td=cl_Ball(0.TR,1) by BROUWER:3;
then reconsider f=F as Function of Td,Td by A3,A1,FUNCT_2:7;
set Mf=(M|Td)*f;
A6: M|Td=M|the carrier of Td by TMAP_1:def 4;
A7: rng Mf c= Sphere(0.TR,1)
proof
let y be object;
assume y in rng Mf;
then consider x be object such that
A8: x in dom Mf and
A9: Mf.x=y by FUNCT_1:def 3;
A10: f.x in dom(M|Td) by A8,FUNCT_1:11;
then f.x in dom M by A6,RELAT_1:57;
then reconsider fx=f.x as Point of TR;
x in dom f by A8,FUNCT_1:11;
then f.x in rng F by FUNCT_1:def 3;
then
A11: 1 = |.fx.| by A3,TOPREAL9:12
.= |.-fx.| by EUCLID:10
.= |.-fx-0.TR.|;
y=(M|Td).(f.x) by A8,A9,FUNCT_1:12;
then y=M.(f.x) by A6,A10,FUNCT_1:47;
then y = (-1)*fx by RLTOPSP1:def 13
.= -fx by RLVECT_1:16;
hence thesis by A11;
end;
then rng Mf c=cl_Ball(0.TR,1) by A1;
then reconsider MF=Mf as Function of Td,Td by A5,FUNCT_2:6;
A12: cl_Ball(0.TR,1) is non boundary by Lm5;
f is continuous by PRE_TOPC:26;
then MF is continuous by PRE_TOPC:27;
then MF is with_fixpoint by A12,Th8;
then consider p be object such that
A13: p is_a_fixpoint_of MF by ABIAN:def 5;
A14: p in dom MF by A13,ABIAN:def 3;
A15: p=MF.p by A13,ABIAN:def 3;
then
A16: p in rng MF by A14,FUNCT_1:def 3;
then reconsider p as Point of TR by A7;
A17: f.p=p by A4,A3,A7,A16;
then
A18: p in dom(M|Td) by A14,FUNCT_1:11;
p=(M|Td).p by A14,A15,A17,FUNCT_1:12;
then p=M.p by A6,A18,FUNCT_1:47;
then p = (-1)*p by RLTOPSP1:def 13
.= -p by RLVECT_1:16;
then
A19: p=0.TR by RLVECT_1:19;
|.p.|=1 by A7,A16,TOPREAL9:12;
hence contradiction by A19,TOPRNS_1:23;
end;
theorem
for A be non empty convex Subset of TOP-REAL n st
A is compact non boundary
for FR be non empty SubSpace of (TOP-REAL n) |A st [#]FR = Fr A
holds not FR is_a_retract_of (TOP-REAL n) |A
proof
set T=TOP-REAL n;
set cB=cl_Ball(0.T,1),S=Sphere(0.T,1);
A1: [#](T|cB)=cB by PRE_TOPC:def 5;
then reconsider s=S as Subset of T|cB by TOPREAL9:17;
A2: T|S=T|cB|s by PRE_TOPC:7,TOPREAL9:17;
let A be non empty convex Subset of T such that
A3: A is compact non boundary;
A4: [#](T|A)=A & Fr A c=A by A3,PRE_TOPC:def 5,TOPS_1:35;
let FR be non empty SubSpace of T|A such that
A5: [#]FR=Fr A;
n>0
proof
assume n<=0;
then n=0;
then {0.T} =the carrier of T by EUCLID:22,77;
then
A6: A=[#]T by ZFMISC_1:33;
then Fr A=Cl A\A by TOPS_1:42;
hence contradiction by A5,A6,XBOOLE_1:37;
end;
then reconsider Ts=T|cB|s as non empty SubSpace of T|cB;
assume FR is_a_retract_of T|A;
then consider F be continuous Function of T|A,FR such that
A7: F is being_a_retraction;
reconsider f=F as Function of T|A,T|A by A5,A4,FUNCT_2:7;
A8: f is continuous by PRE_TOPC:26;
A9: rng F c=Fr A by A5;
reconsider N=n as Element of NAT by ORDINAL1:def 12;
set TN=TOP-REAL N;
A10: [#](T|S)=S by PRE_TOPC:def 5;
T|cB=Tdisk(0.TN,1) & T|S=Tcircle(0.TN,1) by TOPREALB:def 6;
then
A11: not Ts is_a_retract_of T|cB by A2,Lm6;
cB is non boundary by Lm5;
then consider h be Function of T|cB,T|A such that
A12: h is being_homeomorphism and
A13: h.:Fr cB=Fr A by A3,Th7;
A14: dom h=[#](T|cB) by A12,TOPS_2:def 5;
rng((h")*f)=((h")*f).:dom((h")*f) by RELAT_1:113;
then
A15: rng((h")*f)c=((h")*f).:dom f by RELAT_1:25,123;
reconsider H=h as Function;
A16: Fr cB=S by Th5;
rng h=[#](T|A) by A12,TOPS_2:def 5;
then
A17: h".:(Fr A) = h"(Fr A) by A12,A4,TOPS_2:55
.= Fr cB by A12,A13,A1,A14,FUNCT_1:94,TOPS_1:35;
((h")*f).:dom f = (h").:(f.:dom f) by RELAT_1:126
.= h".:rng f by RELAT_1:113;
then ((h")*f).:dom f c=Fr cB by A17,A9,RELAT_1:123;
then rng((h")*f*h)c=rng((h")*f) & rng((h")*f)c=Fr cB
by A15,RELAT_1:26;
then rng((h")*f*h)c=Fr cB;
then reconsider hfh=(h")*f*h as Function of T|cB,Ts by A2,A16,A10,FUNCT_2:6;
h" is continuous by A12,TOPS_2:def 5;
then hfh is continuous by A12,A8,PRE_TOPC:27;
then not hfh is being_a_retraction by A11;
then consider x be Point of T|cB such that
A18: x in S and
A19: hfh.x<>x by A2,A10;
set hx=h.x;
A20: dom hfh=the carrier of(T|cB) by FUNCT_2:def 1;
then
A21: hfh.x=((h")*f).hx by FUNCT_1:12;
x in dom h by A20,FUNCT_1:11;
then
A22: hx in the carrier of FR by A5,A13,A16,A18,FUNCT_1:def 6;
hx in dom((h")*f) by A20,FUNCT_1:11;
then
A23: ((h")*f).hx=(h").(f.hx) by FUNCT_1:12;
A24: H"=h" by A12,TOPS_2:def 4;
H".hx=x by A12,A14,FUNCT_1:34;
hence contradiction by A7,A24,A19,A21,A23,A22;
end;