:: Brouwer Fixed Point Theorem in the General Case :: by Karol P\kak :: :: Received December 21, 2010 :: Copyright (c) 2010-2012 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, ORDINAL1, 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; 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, REALSET1, 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; requirements ARITHM, BOOLE, NUMERALS, SUBSET, REAL; definitions TARSKI, XCMPLX_0, STRUCT_0, ALGSTR_0, TOPREAL9, BORSUK_1, BROUWER; 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; 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 number; 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 EUCLID:45 .= r*q+((1 *p-r*p)-p) by EUCLID:50 .= r*q+((p-r*p)-p) by RLVECT_1:def 8 .= r*q+((p+-r*p)+-p) .= r*q+((p+-p)+-r*p) by EUCLID:26 .= r*q+((p-p)-r*p) .= r*q+(0.(TOP-REAL n)-r*p) by RLVECT_1:15 .= r*q-r*p by RLVECT_1:14 .= r*(q-p) by EUCLID:49; end; Lm2: r>=0 implies r*p in halfline(0.TOP-REAL n,p) proof A1: n in NAT by ORDINAL1:def 12; assume A2: r>=0; (1-r)*0.TOP-REAL n=0.TOP-REAL n & 0.TOP-REAL n+r*p=r*p by RLVECT_1:4,10; hence thesis by A1,A2,TOPREAL9:26; 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 EUCLID:47 .= ((1-r)*p+r*q)-0.TOP-REAL n by RLVECT_1:15 .= (1-r)*p+r*q by RLVECT_1:13; 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.|; A4: n in NAT by ORDINAL1:def 12; per cases; suppose p<>q; then A5: |.q-p.|<>0 by A4,TOPRNS_1:28; consider a1 be real number such that A6: r1=(1-a1)*p+a1*q and A7: a1>=0 by A1,A4,TOPREAL9:26; A8: abs a1=a1 by A7,ABSVALUE:def 1; a1 in REAL & r1-p=a1*(q-p) by A6,Lm1,XREAL_0:def 1; then A9: |.r1-p.|=abs(a1)*|.q-p.| by A4,TOPRNS_1:7; consider a2 be real number such that A10: r2=(1-a2)*p+a2*q and A11: a2>=0 by A2,A4,TOPREAL9:26; a2 in REAL & r2-p=a2*(q-p) by A10,Lm1,XREAL_0:def 1; then A12: |.r2-p.|=abs(a2)*|.q-p.| by A4,TOPRNS_1:7; abs a2=a2 by A11,ABSVALUE:def 1; then a1=a2 by A3,A5,A9,A12,A8,XCMPLX_1:5; hence thesis by A6,A10; end; suppose A13: p=q; then r1 in {p} by A1,A4,TOPREAL9:29; then A14: r1=p by TARSKI:def 1; r2 in {p} by A2,A4,A13,TOPREAL9:29; hence thesis by A14,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)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: n in NAT by ORDINAL1:def 12; then A6: dist(Q,P)=|.q-p.| by SPPOL_1:39; p in H by A5,TOPREAL9:27; then A7: 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; A8: now let x be set; 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 by RLVECT_1:def 4; then A9: 0 in X by A7; then reconsider X as non empty real-membered set by A8,MEMBERED:def 3; A10: DAH+00 ex w be Point of Euclid n st w in AH & dist(spq,w)0; set r2=r/|.q-p.|; assume A18: for w be Point of Euclid n st w in AH holds dist(spq,w)>=r; now let x be ext-real number; assume A19: x in X; then consider w be Real such that A20: x=w and A21: (1-w)*p+w*q in AH and 0<=w; S-w>=0 by A19,A20,XREAL_1:48,XXREAL_2:4; then A22: abs(S-w)=S-w by ABSVALUE:def 1; reconsider PQ=(1-w)*p+w*q as Element of Euclid n by A21; A23: 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 A5,A23,SPPOL_1:39 .= (S-w)*|.q-p.| by A5,A22,TOPRNS_1:7; then (S-w)*|.q-p.|>=r by A18,A21; then S-w>=r2 by A2,A6,METRIC_1:7,XREAL_1:79; hence S-r2>=x by A20,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,A6,A17,XREAL_1:8; end; A24: 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 A24; assume that A25: U is open and A26: Spq in U; UE in the topology of TopSpaceMetr Euclid n by A24,A25,PRE_TOPC:def 2; then UE is open by PRE_TOPC:def 2; then consider r be real number such that A27: r>0 and A28: Ball(spq,r)c=UE by A26,TOPMETR:15; set r2 = r/|.q-p.|; set Sr = S+r2/2; consider w be Element of Euclid n such that A29: w in AH & dist(spq,w)S+0 by A4,A6,A27,XREAL_1:6; then S-Sr<0 by XREAL_1:49; then A31: abs(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; A32: srpq in H by A15,A27; A33: not srpq in A proof assume srpq in A; then srpq in AH by A32,XBOOLE_0:def 4; then Sr in X by A15,A27; then S+r2/2<=S+0 by XXREAL_2:4; hence contradiction by A4,A6,A27,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 A5,SPPOL_1:39 .= r2/2*|.q-p.| by A5,A31,TOPRNS_1:7 .= r/2 by A30; then dist(spq,srpq){} by A28,A33,XBOOLE_0:def 5; end; then A34: Spq in Fr A by TOPGEN_1:9; take spq; A35: Spq-p=S*(q-p) by Lm1; Spq in H by A15; hence spq in (Fr A)/\H by A34,XBOOLE_0:def 4; A36: abs S=S by A15,ABSVALUE:def 1; hereby let u,P be Point of Euclid n such that A37: P=p and A38: u in A/\H; A39: dist(P,spq) = |.S*(q-p).| by A5,A35,A37,SPPOL_1:39 .= S*|.q-p.| by A5,A36,TOPRNS_1:7; u in H by A38,XBOOLE_0:def 4; then consider Ur be real number such that A40: u=(1-Ur)*p+Ur*q and A41: 0<=Ur by A5,TOPREAL9:26; A42: abs Ur=Ur by A41,ABSVALUE:def 1; Ur in REAL by XREAL_0:def 1; then Ur in X by A38,A40,A41; then A43: Ur<=S by XXREAL_2:4; set du=dist(P,u),ds=dist(P,spq); A44: (1-Ur)*p+Ur*q-p=Ur*(q-p) by Lm1; dist(P,u) = |.Ur*(q-p).| by A5,A37,A40,A44,SPPOL_1:39 .= Ur*|.q-p.| by A5,A42,TOPRNS_1:7; hence du<=ds by A39,A43,XREAL_1:64; end; thus thesis by A16; 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)0; then consider U be Point of E such that A8: U in A/\halfline(p,q) & dist(W,U) 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; A5: n in NAT by ORDINAL1:def 12; reconsider P=p,Q=q as Point of En by EUCLID:67; A6: 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 A6,PRE_TOPC:def 2; then I is open by PRE_TOPC:def 2; then consider r be real number such that A7: r>0 and A8: Ball(P,r)c=I by A2,TOPMETR:15; dist(P,P)0 ex u be Point of En st u in AH & dist(W,u)=0 by A5,TOPREAL9:26; A16: Fr A c=A by A1,TOPS_1:35; A17: Fr A misses Ball(P,r) by A8,TOPS_1:39,XBOOLE_1:63; (Fr A)/\H={W} proof assume(Fr A)/\H<>{W}; then consider u be set such that A18: u in (Fr A)/\H and A19: u<>W by A11,ZFMISC_1:35; reconsider u as Point of TRn by A18; A20: u in H by A18,XBOOLE_0:def 4; then consider Ur be real number such that A21: u=(1-Ur)*p+Ur*q and A22: Ur>=0 by A5,TOPREAL9:26; A23: abs Ur=Ur by A22,ABSVALUE:def 1; reconsider U=u as Element of En by EUCLID:67; A24: Wr-Ur in REAL by XREAL_0:def 1; (1-Ur)*p+Ur*q-p=Ur*(q-p) by Lm1; then A25: dist(U,P) = |.Ur*(q-p).| by A5,A21,SPPOL_1:39 .= Ur*|.q-p.| by A5,A23,TOPRNS_1:7; set R=r*(Wr-Ur)/Wr; reconsider b=Ball(U,R) as Subset of TopSpaceMetr En by A6,EUCLID:67; set x=(Wr-Ur)/Wr; b is open by TOPMETR:14; then b in the topology of TRn by A6,PRE_TOPC:def 2; then reconsider B=b as open Subset of TRn by PRE_TOPC:def 2; A26: abs Wr=Wr by A15,ABSVALUE:def 1; (1-Wr)*p+Wr*q-p=Wr*(q-p) by Lm1; then A27: dist(W,P) = |.Wr*(q-p).| by A5,A14,SPPOL_1:39 .= Wr*|.q-p.| by A5,A26,TOPRNS_1:7; A28: u in Fr A by A18,XBOOLE_0:def 4; then A29: u in AH by A16,A20,XBOOLE_0:def 4; P<>W by A17,A9,A13,XBOOLE_0:3; then A30: Wr>0 by A27,METRIC_1:7; then A31: 1-x = Wr/Wr-x by XCMPLX_1:60 .= Ur/Wr; P<>u by A17,A9,A28,XBOOLE_0:3; then Ur>0 by A25,METRIC_1:7; then 1-x>=x-x by A30,A31; then A32: x in REAL & x<=1 by XREAL_0:def 1,XREAL_1:6; A33: (1-Wr)*p+Wr*q=Wr*(q-p)+p by Th1; A34: (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 A33,RLVECT_1:27 .= Wr*(q-p)+(p-p)-Ur*(q-p) by EUCLID:45 .= Wr*(q-p)+0.TRn-Ur*(q-p) by EUCLID:42 .= Wr*(q-p)-Ur*(q-p) by RLVECT_1:def 4 .= (Wr-Ur)*(q-p) by EUCLID:50; then A35: dist(U,W) = |.(Wr-Ur)*(q-p).| by A5,A14,A21,SPPOL_1:39 .= abs(Wr-Ur)*|.q-p.| by A5,A24,TOPRNS_1:7; dist(U,W)>0 by A19,METRIC_1:7; then |.q-p.|>0 by A35,XREAL_1:134; then Ur<=Wr by A12,A25,A27,A29,XREAL_1:68; then Wr-Ur>=0 by XREAL_1:48; then A36: abs(Wr-Ur)=Wr-Ur by ABSVALUE:def 1; then A37: Wr-Ur>0 by A19,A35,METRIC_1:7; dist(U,U)=0 by METRIC_1:1; then U in B by A7,A30,A37,METRIC_1:11; then B\A<>{} by A28,TOPGEN_1:9; then consider t be set such that A38: t in B\A by XBOOLE_0:def 1; A39: t in B by A38,XBOOLE_0:def 5; reconsider t as Point of TRn by A38; 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; A40: dist(U,T)=|.u-t.| by A5,SPPOL_1:39; A41: Wr/(Wr-Ur)*R = Wr/Wr*(Wr-Ur)/(Wr-Ur)*r .= (Wr-Ur)/(Wr-Ur)*r by A30,XCMPLX_1:88 .= r by A37,XCMPLX_1:88; abs(-Wr)=--Wr by A30,ABSVALUE:def 1; then A42: (-Wr)/(Wr-Ur) in REAL & abs((-Wr)/(Wr-Ur))=Wr/(Wr-Ur) by A36,COMPLEX1:67,XREAL_0:def 1; A43: (Ur/Wr)*(Wr*(q-p)) = (Ur/Wr*Wr)*(q-p) by RLVECT_1:def 7 .= (Wr/Wr*Ur)*(q-p) .= Ur*(q-p) by A30,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) by RLVECT_1:14 .= (-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 A44: dist(P,Z) = |.((-Wr)/(Wr-Ur))*(t-u).| by A5,SPPOL_1:39 .= Wr/(Wr-Ur)*|.t-u.| by A5,A42,TOPRNS_1:7; dist(U,T)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 number 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; A20: not 0 in rng(nN|TRn0) proof assume 0 in rng(nN|TRn0); then consider x be set such that A21: x in dom(nN|TRn0) and A22: (nN|TRn0).x=0 by FUNCT_1:def 3; x in dom nN by A19,A21,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,A21,A22,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,A21,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=InN0 as Function of TRn0,TRn by TOPREALC:46; A23: dom b = cTR0 by A10,FUNCT_2:def 1; A24: 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 A25: p in cTR0; then A26: nN0.p=nN.p & I.p=p by A10,A19,FUNCT_1:49,TMAP_1:84; thus b.p = I.p(/)nN0.p by A23,A25,VALUED_2:72 .= p(/)|.p.| by A26,JGRAPH_4:def 1 .= 1/|.p.|(#)p by VALUED_2:def 32 .= 1/|.p.|*p; A27: abs(1/|.p.|)=1/|.p.| & p<>0.TRn by A25,ABSVALUE:def 1,ZFMISC_1:56; thus|.(1/|.p.|)*p.| = abs(1/|.p.|)*|.p.| by TOPRNS_1:7 .= 1 by A27,TOPRNS_1:24,XCMPLX_1:87; end; A28: rng b c=S proof let y be set; assume y in rng b; then consider x be set such that A29: x in dom b and A30: b.x=y by FUNCT_1:def 3; reconsider x as Point of TRn by A23,A29; A31: (1/|.x.|)*x-0.TRn=(1/|.x.|)*x & |.(1/|.x.|)*x.|=1 by A10,A24,A29,RLVECT_1:13; y = 1/|.x.|*x by A10,A24,A29,A30; hence thesis by A31; end; then reconsider B=b as Function of TRn0,TS by A10,A18,A23,FUNCT_2:2; A32: I0={0.TRn}-->0.TRn by FUNCOP_1:def 9; then A33: dom I0={0.TRn} by FUNCOP_1:13; set FRA=TRn0|FrA,H=b|FRA; A34: dom H=the carrier of FRA by FUNCT_2:def 1; A35: H=b|the carrier of FRA by TMAP_1:def 4; then A36: rng H c=rng b by RELAT_1:70; then A37: rng H c=S by A28,XBOOLE_1:1; reconsider H as Function of FRA,TS by A18,A28,A34,A36,FUNCT_2:2,XBOOLE_1:1; A38: [#]FRA=FrA by PRE_TOPC:def 5; A39: (Fr A)\{0.TRn}c=cTR0 by XBOOLE_1:33; S c=rng H proof let x be set; assume x in S; then consider p be Point of TRn such that A40: x=p and A41: |.p-0.TRn.|=1; p <> 0.TRn by A5,A41; then consider q be Point of TRn such that A42: FrA/\halfline(0.TRn,p)={q} by A13; A43: q in {q} by TARSKI:def 1; then A44: q in FrA by A42,XBOOLE_0:def 4; then A45: b.q=1/|.q.|*q & b.q=H.q by A9,A24,A35,A38,A39,FUNCT_1:49; q in halfline(0.TRn,p) by A42,A43,XBOOLE_0:def 4; then halfline(0.TRn,p)=halfline(0.TRn,q) by A5,A8,A44,TOPREAL9:31; then A46: 1/|.q.|*q in halfline(0.TRn,p) by Lm2; A47: 1/|.q.|*q-0.TRn=1/|.q.|*q & p in halfline(0.TRn,p) by RLVECT_1:13 ,TOPREAL9:28; H.q in rng H & |.1/|.q.|*q.|=1 by A9,A24,A34,A38,A39,A44,FUNCT_1:def 3; hence thesis by A40,A41,A46,A47,A45,Th2; end; then A48: S=rng H by A37,XBOOLE_0:def 10; (Fr A) \ {0.TRn} c= cTR0 by XBOOLE_1:33; then A49: dom H=[#]FRA & TRn| (Fr A)=FRA by A9,FUNCT_2:def 1,PRE_TOPC:7; for x1,x2 be set st x1 in dom H & x2 in dom H & H.x1=H.x2 holds x1=x2 proof let x1,x2 be set such that A50: x1 in dom H and A51: x2 in dom H and A52: H.x1=H.x2; A53: x2 in dom b by A35,A51,RELAT_1:57; A54: x1 in dom b by A35,A50,RELAT_1:57; then reconsider p1=x1,p2=x2 as Point of TRn by A23,A53; A55: b.p1=1/|.p1.|*p1 by A10,A24,A54; x2<>0.TRn by A10,A53,ZFMISC_1:56; then consider q be Point of TRn such that A56: (Fr A)/\halfline(0.TRn,p2)={q} by A13; p2 in halfline(0.TRn,p2) by TOPREAL9:28; then p2 in {q} by A38,A51,A56,XBOOLE_0:def 4; then A57: p2=q by TARSKI:def 1; |.(1/|.p2.|)*p2.|=1 by A10,A24,A53; then A58: 1/|.p2.|*p2<>0.TRn by TOPRNS_1:23; A59: 0.TRn+1/|.p2.|*p2=1/|.p2.|*p2 by RLVECT_1:4; A60: b.p2=1/|.p2.|*p2 by A10,A24,A53; A61: H.x1=b.x1 & H.x2=b.x2 by A35,A50,A51,FUNCT_1:47; (1-1/|.p1.|)*0.TRn = 0.TRn by RLVECT_1:10; then A62: 1/|.p1.|*p1 in halfline(0.TRn,p1) by A52,A55,A59,A60,A61; (1-1/|.p2.|)*0.TRn=0.TRn by RLVECT_1:10; then 1/|.p2.|*p2 in halfline(0.TRn,p2) by A59; then halfline(0.TRn,p2) = halfline(0.TRn,1/|.p1.|*p1) by A52,A55,A58,A60,A61,TOPREAL9:31 .= halfline(0.TRn,p1) by A52,A55,A58,A60,A61,A62,TOPREAL9:31; then p1 in halfline(0.TRn,p2) by TOPREAL9:28; then p1 in {q} by A38,A50,A56,XBOOLE_0:def 4; hence thesis by A57,TARSKI:def 1; end; then A63: H is one-to-one by FUNCT_1:def 4; then H is being_homeomorphism by A2,A18,A48,A49,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 A48; reconsider NH1B=nN0F*H1B as Function of TRn0,R^1; A64: 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 by XBOOLE_1:1; then A65: not 0 in rng NH1B by A20; (B is continuous) & S is non empty by A28,PRE_TOPC:27; then reconsider NH1B as non-empty continuous Function of TRn0,R^1 by A65,RELAT_1:def 9; reconsider G=INH1B as Function of TRn0,TRn by TOPREALC:46; A66: dom G=cTR0 by A10,FUNCT_2:def 1; A67: dom nN0F=FrA by A38,FUNCT_2:def 1; A68: 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 A69: p in cTR0; then A70: p in dom NH1B by A10,FUNCT_2:def 1; then A71: H1B.p in dom nN0F by FUNCT_1:11; then reconsider Hp=H1B.p as Point of TRn by A67; A72: nN0F.Hp=nN0.Hp by A64,A71,FUNCT_1:49; A73: nN.Hp=|.Hp.| & nN0.Hp=nN.Hp by A19,A67,A71,FUNCT_1:49,JGRAPH_4:def 1; take Hp; A74: NH1B.p=nN0F.(H1B.p) by A70,FUNCT_1:12; G.p = I.p(/)NH1B.p by A66,A69,VALUED_2:72 .= p(/)|.Hp.| by A10,A69,A74,A72,A73,TMAP_1:84 .= 1/|.Hp.|(#)p by VALUED_2:def 32 .= 1/|.Hp.|*p; hence thesis by A38,A64,A70,A71,A74,A73,FUNCT_1:49; end; A75: not 0.TRn in rng G proof assume 0.TRn in rng G; then consider p be set such that A76: p in dom G and A77: G.p=0.TRn by FUNCT_1:def 3; reconsider p as Point of TRn by A66,A76; consider Hp be Point of TRn such that Hp=H1B.p and Hp in FrA and A78: G.p=1/|.Hp.|*p & |.Hp.|>0 by A10,A68,A76; p<>0.TRn by A10,A76,ZFMISC_1:56; hence contradiction by A77,A78,RLVECT_1:11; end; A79: 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 A80: x1 in dom I0 and A81: x2 in dom G\dom I0; x1=0.TRn by A80,TARSKI:def 1; then A82: I0.x1=0.TRn by FUNCOP_1:72; x2 in dom G by A81,XBOOLE_0:def 5; hence thesis by A75,A82,FUNCT_1:def 3; end; H is onto by A18,A48,FUNCT_2:def 3; then A83: H"=HH" by A63,TOPS_2:def 4; A84: 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 A85: p in cTR0; then A86: p in dom H1B by A10,FUNCT_2:def 1; then A87: H1B.p=H1.(B.p) by FUNCT_1:12; B.p in dom H1 by A86,FUNCT_1:11; then consider x be set such that A88: x in dom H and A89: H.x=B.p by A18,A48,FUNCT_1:def 3; reconsider x as Point of TRn by A34,A38,A88; A90: H.x=b.x by A35,A88,FUNCT_1:47; set xp=|.x.|/|.p.|; A91: x in FrA by A38,A88; then A92: b.x=1/|.x.|*x by A9,A24,A39; |.(1/|.x.|)*x.|=1 by A9,A24,A39,A91; 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 A24,A85,A89,A90,A92 .= xp*p by RLVECT_1:def 7; then x in halfline(0.TRn,p) by Lm2; then A93: x in (Fr A)/\halfline(0.TRn,p) by A38,A88,XBOOLE_0:def 4; p<>0.TRn by A85,ZFMISC_1:56; then consider y be Point of TRn such that A94: (Fr A)/\halfline(0.TRn,p)={y} by A13; H1.(B.p)=x by A63,A83,A88,A89,FUNCT_1:34; hence thesis by A87,A93,A94,TARSKI:def 1; end; for x1,x2 be set st x1 in dom G & x2 in dom G & G.x1=G.x2 holds x1=x2 proof let x1,x2 be set such that A95: x1 in dom G and A96: x2 in dom G and A97: G.x1=G.x2; reconsider p1=x1,p2=x2 as Point of TRn by A66,A95,A96; consider Hp1 be Point of TRn such that A98: Hp1=H1B.p1 and Hp1 in FrA and A99: G.p1=1/|.Hp1.|*p1 and A100: |.Hp1.|>0 by A10,A68,A95; A101: FrA/\halfline(0.TRn,p1)={Hp1} by A10,A84,A95,A98; consider Hp2 be Point of TRn such that A102: Hp2=H1B.p2 and Hp2 in FrA and A103: G.p2=1/|.Hp2.|*p2 and |.Hp2.|>0 by A10,A68,A96; p1<>0.TRn by A10,A95,ZFMISC_1:56; then A104: 1/|.Hp1.|*p1<>0.TRn by A100,RLVECT_1:11; then halfline(0.TRn,p1) = halfline(0.TRn,1/|.Hp1.|*p1) by Lm2,TOPREAL9:31 .= halfline(0.TRn,p2) by A97,A99,A103,A104,Lm2,TOPREAL9:31; then Hp1 in {Hp1} & {Hp1}={Hp2} by A10,A84,A96,A101,A102,TARSKI:def 1; then 1/|.Hp1.|=1/|.Hp2.| by TARSKI:def 1; hence thesis by A97,A99,A100,A103,RLVECT_1:36; end; then A105: G is one-to-one by FUNCT_1:def 4; set G0=G+*I0; A106: dom G0 = dom G\/dom I0 by FUNCT_4:def 1 .= cTR0\/{0.TRn} by A32,A66,FUNCOP_1:13 .= cTRn by ZFMISC_1:116; A107: 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 A108: p in cTR0 and A109: Hp1=H1B.p; reconsider p as Point of TRn; consider Hp be Point of TRn such that A110: Hp=H1B.p and Hp in FrA and G.p=1/|.Hp.|*p and A111: |.Hp.|>0 by A68,A108; set Hpp=|.Hp.|*p; p<>0.TRn by A108,ZFMISC_1:56; then A112: Hpp<>0.TRn by A111,RLVECT_1:11; then A113: Hpp in cTR0 by ZFMISC_1:56; then consider HP be Point of TRn such that A114: HP=H1B.Hpp and HP in FrA and A115: G.Hpp=1/|.HP.|*Hpp and |.HP.|>0 by A68; A116: Hp in {Hp} by TARSKI:def 1; {HP} = (Fr A)/\halfline(0.TRn,Hpp) by A84,A113,A114 .= (Fr A)/\halfline(0.TRn,p) by A112,Lm2,TOPREAL9:31 .= {Hp} by A84,A108,A110; then G.Hpp = 1/|.Hp.|*(|.Hp.|*p) by A115,A116,TARSKI:def 1 .= (|.Hp.|/|.Hp.|)*p by RLVECT_1:def 7 .= 1 *p by A111,XCMPLX_1:60 .= p by RLVECT_1:def 8; hence thesis by A66,A109,A110,A112,ZFMISC_1:56; end; A117: S c=G.:FrA proof let p be set; assume A118: p in S; then reconsider p as Point of TRn; |.p.|=1 by A118,TOPREAL9:12; then p<>0.TRn by TOPRNS_1:23; then A119: p in cTR0 by ZFMISC_1:56; then consider Hp be Point of TRn such that A120: Hp=H1B.p and A121: Hp in FrA and G.p=1/|.Hp.|*p and |.Hp.|>0 by A68; set Hpp=|.Hp.|*p; A122: p=G.Hpp & Hpp in dom G by A107,A119,A120; Hp in {Hp} & (Fr A)/\halfline(0.TRn,p)={Hp} by A84,A119,A120,TARSKI:def 1; then A123: Hp in halfline(0.TRn,p) by XBOOLE_0:def 4; A124: Hp-0.TRn=Hp by RLVECT_1:13; abs|.Hp.|=|.Hp.| by ABSVALUE:def 1; then A125: |.Hpp.| = |.Hp.|*|.p.| by TOPRNS_1:7 .= |.Hp.|*1 by A118,TOPREAL9:12; Hpp-0.TRn=Hpp & Hpp in halfline(0.TRn,p) by Lm2,RLVECT_1:13; then Hp=Hpp by A125,A123,A124,Th2; hence thesis by A121,A122,FUNCT_1:def 6; end; A126: 0.TRn in {0.TRn} by TARSKI:def 1; then A127: I0.(0.TRn)=0.TRn by A32,FUNCOP_1:7; rng I0={0.TRn} by A32,FUNCOP_1:8; then rng G0=rng G\/{0.TRn} by A33,A66,NECKLACE:6,XBOOLE_1:79; then reconsider G1=G0 as one-to-one Function of TRn,TRn by A106,A79,A105,FUNCT_2:2,TOPMETR2:1; A128: G1.0.TRn=I0.(0.TRn) by A33,A126,FUNCT_4:13; A129: G.:FrA c=S proof let y be set; assume y in G.:FrA; then consider p be set such that A130: p in dom G and A131: p in FrA and A132: G.p=y by FUNCT_1:def 6; reconsider p as Point of TRn by A131; consider Hp be Point of TRn such that A133: Hp=H1B.p and Hp in FrA and A134: G.p=1/|.Hp.|*p and A135: |.Hp.|>0 by A10,A68,A130; p in halfline(0.TRn,p) by TOPREAL9:28; then A136: p in FrA/\halfline(0.TRn,p) by A131,XBOOLE_0:def 4; FrA/\halfline(0.TRn,p)={Hp} by A10,A84,A130,A133; then A137: p=Hp by A136,TARSKI:def 1; abs(1/|.Hp.|)=1/|.Hp.| by ABSVALUE:def 1; then |.1/|.Hp.|*p.| = (1/|.Hp.|)*|.Hp.| by A137,TOPRNS_1:7 .= 1 by A135,XCMPLX_1:106; then |.1/|.Hp.|*p-0.TRn.|=1 by RLVECT_1:13; hence thesis by A132,A134; end; set TRnCL=TRn|CL; set TRnA=TRn|A; A138: Int A c=A by TOPS_1:16; set GA=G1|TRnA; A139: G1|TRnA=G1|the carrier of TRnA by TMAP_1:def 4; A140: [#]TRnA=A by PRE_TOPC:def 5; then A141: dom GA=A by FUNCT_2:def 1; A142: dom GA=the carrier of TRnA by FUNCT_2:def 1; A143: cl_Ball(0.TRn,1)c=rng GA proof let p be set; assume A144: 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,A138,A5,A127,A139,A140,A128,FUNCT_1:49; hence thesis by A3,A138,A5,A140,A142,FUNCT_1:def 3; end; suppose A145: p<>0.TRn; set h=halfline(0.TRn,p); A146: p in cTR0 by A145,ZFMISC_1:56; then consider Hp be Point of TRn such that A147: Hp=H1B.p and A148: Hp in FrA and G.p=1/|.Hp.|*p and A149: |.Hp.|>0 by A68; A150: abs|.Hp.|=|.Hp.| by ABSVALUE:def 1; Fr A/\h={Hp} by A84,A146,A147; then Hp in Fr A/\h by TARSKI:def 1; then A151: Hp in h by XBOOLE_0:def 4; Hp<>0.TRn by A149,TOPRNS_1:23; then h=halfline(0.TRn,Hp) by A151,TOPREAL9:31; then A152: |.p.|*Hp in h by Lm2; |.p.|<=1 by A144,TOPREAL9:11; then (1- |.p.|)*0.TRn=0.TRn & |.p.|*Hp+(1- |.p.|)*0.TRn in A by A3,A138,A5,A17,A148,RLTOPSP1:def 1,RLVECT_1:10; then |.p.|*Hp in dom GA by A141,RLVECT_1:4; then A153: GA.(|.p.|*Hp) in rng GA & GA.(|.p.|*Hp)=G1.(|.p.|*Hp) by A139,FUNCT_1:47,def 3; A154: |.Hp.|*p in h by Lm2; (|.Hp.|*p) in dom G by A107,A146,A147; then |.Hp.|*p<>0.TRn by A10,ZFMISC_1:56; then not |.Hp.|*p in dom I0 by TARSKI:def 1; then A155: G.(|.Hp.|*p)=G1.(|.Hp.|*p) by FUNCT_4:11; abs|.p.|=|.p.| by ABSVALUE:def 1; then |.|.p.|*Hp.| = |.p.|*|.Hp.| by TOPRNS_1:7 .= |.|.Hp.|*p.| by A150,TOPRNS_1:7; then A156: |.|.p.|*Hp-0.TRn.| = |.|.Hp.|*p.| by RLVECT_1:13 .= |.|.Hp.|*p-0.TRn.| by RLVECT_1:13; p=G.(|.Hp.|*p) by A107,A146,A147; hence thesis by A152,A155,A156,A153,A154,Th2; end; end; rng GA c=cl_Ball(0.TRn,1) proof let x be set; assume x in rng GA; then consider p be set such that A157: p in dom GA and A158: GA.p=x by FUNCT_1:def 3; reconsider p as Point of TRn by A141,A157; A159: GA.p=G1.p by A139,A157,FUNCT_1:47; A160: G1.p-0.TRn=G1.p by RLVECT_1:13; per cases; suppose p=0.TRn; then G1.p=0.TRn by A32,A126,A128,FUNCOP_1:7; then |.G1.p-0.TRn.|=0 by A160,TOPRNS_1:23; hence thesis by A158,A159; end; suppose A161: p<>0.TRn; set h=halfline(0.TRn,p); A162: 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,A162,HAUSDORF:18,TBSP_1:14; then A/\h is bounded by JORDAN2C:11; then consider w be Point of En such that A163: w in (Fr A)/\h and A164: 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)0 by A68; abs(1/|.Hp.|)=1/|.Hp.| by ABSVALUE:def 1; then A170: |.1/|.Hp.|*p.|=|.p.|/|.Hp.| by TOPRNS_1:7; (Fr A)/\h={Hp} by A84,A167,A168; then w=Hp by A163,TARSKI:def 1; then A171: dist(0TRn,w) = |.0.TRn-Hp.| by SPPOL_1:39 .= |.-Hp.| by RLVECT_1:14 .= |.Hp.| by TOPRNS_1:26; dist(0TRn,P) = |.0.TRn-p.| by SPPOL_1:39 .= |.-p.| by RLVECT_1:14 .= |.p.| by TOPRNS_1:26; then |.1/|.Hp.|*p.|<=1 by A164,A165,A170,A171,XREAL_1:183; then |.G1.p.|<=1 by A166,A169,FUNCT_4:11; hence thesis by A158,A159,A160; end; end; then A172: rng GA=CL by A143,XBOOLE_0:def 10; A173: [#]TRnCL=CL by PRE_TOPC:def 5; then reconsider GA as Function of TRnA,TRnCL by A140,A141,A172,FUNCT_2:1; set e2=e/2; A174: GA is one-to-one by A139,FUNCT_1:52; A175: e20.TRn; then A178: x in dom G by A66,ZFMISC_1:56; then reconsider X=x as Point of TRn0; not x in dom I0 by A177,TARSKI:def 1; then A179: G.x=G1.x by FUNCT_4:11; then A180: G1.x<>0.TRn by A75,A178,FUNCT_1:def 3; then reconsider G1x=G1.x as Point of TRn0 by A10,ZFMISC_1:56; G1.x in cTR0 by A180,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 A181: G.:H c=cTR0/\U by A179,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 A32,BOOLMARK:3,XBOOLE_1:17; hence thesis by A181,XBOOLE_1:1; reconsider U1=cTR0/\U as Subset of TRn0 by A10,XBOOLE_1:17; end; suppose A182: x=0.TRn; reconsider 0TRn=0.TRn as Point of Euclid n by EUCLID:67; A183: 0.TRn in Int(U) by A127,A128,A182,CONNSP_2:def 1; then consider r be real number such that A184: r>0 and A185: 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,A184,GOBOARD6:5; then reconsider Bx=B as a_neighborhood of x by A182,CONNSP_2:def 1; take Bx; let y be set; assume A186: y in G1.:Bx; then reconsider p=y as Point of TRn; A187: Int U c=U by TOPS_1:16; per cases; suppose y=0.TRn; hence y in U by A183,A187; end; suppose A188: p<>0.TRn; set PP=e2/|.p.|*p; abs(e2/|.p.|)=e2/|.p.| by A6,ABSVALUE:def 1; then A189: |.PP.| = (e2/|.p.|)*|.p.| by TOPRNS_1:7 .= e2*(|.p.|/|.p.|) .= e2*1 by A188,TOPRNS_1:24,XCMPLX_1:60 .= e2; then |.PP-0.TRn.|0 ex u be Point of En st u in A/\h & dist(w,u)0 by A68; Fr A/\h={Hp} by A84,A194,A195; then w=Hp by A192,TARSKI:def 1; then A197: dist(0TRn,w) = |.0.TRn-Hp.| by SPPOL_1:39 .= |.-Hp.| by RLVECT_1:14 .= |.Hp.| by TOPRNS_1:26; set Hpp=|.Hp.|*p; Hpp in dom G by A107,A194,A195; then Hpp<>0.TRn by A10,ZFMISC_1:56; then not Hpp in dom I0 by TARSKI:def 1; then A198: G.Hpp=G1.Hpp by FUNCT_4:11; |.Hp.|=abs|.Hp.| by ABSVALUE:def 1; then A199: 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 set such that A200: x in dom G1 and A201: x in Bx and A202: G1.x=p by A186,FUNCT_1:def 6; PP in h & Ball(0.TRn,e)=Ball(0TRn,e) by A6,Lm2,TOPREAL9:13; then A203: pp in A/\h by A7,A190,XBOOLE_0:def 4; dist(0TRn,pp) = |.0.TRn-PP.| by SPPOL_1:39 .= |.-PP.| by RLVECT_1:14 .= e2 by A189,TOPRNS_1:26; then e2/|.Hp.|<=1 by A193,A197,A203,XREAL_1:183; then A204: r*(e2/|.Hp.|)<=r*1 by A184,XREAL_1:64; p=G.Hpp by A107,A194,A195; then Hpp=x by A106,A198,A200,A202,FUNCT_1:def 4; then |.p.|<(r*e2)/|.Hp.| by A196,A199,A201,TOPREAL9:10,XREAL_1:81; then |.p.| 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: n in NAT by ORDINAL1:def 12; then A3: B misses S by TOPREAL9:19; A4: B\/S=CB by A2,TOPREAL9:18; A5: Int cb c=B proof reconsider ONE=1 as Real; let x be set; assume x in Int cb; then consider Q be Subset of TR such that A6: Q is open and A7: Q c=CB and A8: x in Q by TOPS_1:22; reconsider q=x as Point of TR by A8; consider w be positive real number such that A9: Ball(q,w)c=Q by A6,A8,TOPS_4:2; assume not x in B; then q in Sphere(p,r) by A4,A7,A8,XBOOLE_0:def 3; then A10: |.q-p.|=r by A2,TOPREAL9:9; set w2=w/2; set wr=(w2/r)*(q-p); A11: abs(w2/r)=w2/r by A1,ABSVALUE:def 1; A12: 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 EUCLID:45 .= |.wr+0.TR.| by RLVECT_1:15 .= |.wr.| by RLVECT_1:def 4 .= (w2/r)*r by A2,A10,A11,TOPRNS_1:7 .= w2 by A1,XCMPLX_1:87; then |.wr+q-q.|0+r by XREAL_1:6; abs((w2+r)/r)=(w2+r)/r by A1,ABSVALUE:def 1; then |.wr+q-p.| = (w2+r)/r*r by A2,A10,A14,A12,TOPRNS_1:7 .= w2+r by A1,XCMPLX_1:87; hence contradiction by A2,A7,A13,A15,TOPREAL9:8; end; B c=Int cb by A2,TOPREAL9:16,TOPS_1:24; then Int cb=B by A5,XBOOLE_0:def 10; then Fr CB=CB\B by TOPS_1:43; hence thesis by A4,A3,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{} by A1,TOPS_1:48; then consider p be set 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; 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 set 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; n in NAT by ORDINAL1:def 12; then Ball(0.TR,1)c=Int cB by TOPREAL9:16,TOPS_1:24; hence thesis; end; 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(-1,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 by BORSUK_1:def 17; 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 set; assume y in rng Mf; then consider x be set 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.| by RLVECT_1:13; 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,XBOOLE_1:1; 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 set 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,BORSUK_1:def 16; 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; A1: n in NAT by ORDINAL1:def 12; set cB=cl_Ball(0.T,1),S=Sphere(0.T,1); A2: [#](T|cB)=cB by PRE_TOPC:def 5; then reconsider s=S as Subset of T|cB by A1,TOPREAL9:17; A3: T|S=T|cB|s by A1,PRE_TOPC:7,TOPREAL9:17; let A be non empty convex Subset of T such that A4: A is compact non boundary; A5: [#](T|A)=A & Fr A c=A by A4,PRE_TOPC:def 5,TOPS_1:35; let FR be non empty SubSpace of T|A such that A6: [#]FR=Fr A; n>0 proof assume n<=0; then n=0; then {0.T} =the carrier of T by EUCLID:22,77; then A7: A=[#]T by ZFMISC_1:33; then Fr A=Cl A\A by TOPS_1:42; hence contradiction by A6,A7,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 A8: F is being_a_retraction by BORSUK_1:def 17; reconsider f=F as Function of T|A,T|A by A6,A5,FUNCT_2:7; A9: f is continuous by PRE_TOPC:26; A10: rng F c=Fr A by A6; reconsider N=n as Element of NAT by ORDINAL1:def 12; set TN=TOP-REAL N; A11: [#](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 A12: not Ts is_a_retract_of T|cB by A3,Lm6; cB is non boundary by Lm5; then consider h be Function of T|cB,T|A such that A13: h is being_homeomorphism and A14: h.:Fr cB=Fr A by A1,A4,Th7; A15: dom h=[#](T|cB) by A13,TOPS_2:def 5; rng((h")*f)=((h")*f).:dom((h")*f) by RELAT_1:113; then A16: rng((h")*f)c=((h")*f).:dom f by RELAT_1:25,123; reconsider H=h as Function; A17: Fr cB=S by Th5; rng h=[#](T|A) by A13,TOPS_2:def 5; then A18: h".:(Fr A) = h"(Fr A) by A13,A5,TOPS_2:55 .= Fr cB by A13,A14,A2,A15,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 A18,A10,RELAT_1:123; then rng((h")*f*h)c=rng((h")*f) & rng((h")*f)c=Fr cB by A16,RELAT_1:26,XBOOLE_1:1; then rng((h")*f*h)c=Fr cB by XBOOLE_1:1; then reconsider hfh=(h")*f*h as Function of T|cB,Ts by A3,A17,A11,FUNCT_2:6; h" is continuous by A13,TOPS_2:def 5; then hfh is continuous by A13,A9,PRE_TOPC:27; then not hfh is being_a_retraction by A12,BORSUK_1:def 17; then consider x be Point of T|cB such that A19: x in S and A20: hfh.x<>x by A3,A11,BORSUK_1:def 16; set hx=h.x; A21: dom hfh=the carrier of(T|cB) by FUNCT_2:def 1; then A22: hfh.x=((h")*f).hx by FUNCT_1:12; x in dom h by A21,FUNCT_1:11; then A23: hx in the carrier of FR by A6,A14,A17,A19,FUNCT_1:def 6; hx in dom((h")*f) by A21,FUNCT_1:11; then A24: ((h")*f).hx=(h").(f.hx) by FUNCT_1:12; A25: H"=h" by A13,TOPS_2:def 4; H".hx=x by A13,A15,FUNCT_1:34; hence contradiction by A8,A25,A20,A22,A24,A23,BORSUK_1:def 16; end;