:: Brouwer Fixed Point Theorem in the General Case :: by Karol P\kak :: :: Received December 21, 2010 :: Copyright (c) 2010-2018 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)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+00 ex w be Point of Euclid n st w in AH & dist(spq,w)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)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){} 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)0; then consider U be Point of E such that A7: 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; 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)0 ex u be Point of En st u in AH & dist(W,u)=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)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=InN0 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} by FUNCOP_1:13; 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=INH1B 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,A69,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,FUNCOP_1:13 .= 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)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: e20.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.|0 ex u be Point of En st u in A/\h & dist(w,u)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.| 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.|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{} 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; 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;