:: The {B}orsuk-Ulam Theorem :: by Artur Korni{\l}owicz and Marco Riccardi :: :: Received November 3, 2011 :: Copyright (c) 2011-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 PRE_TOPC, ORDINAL2, FUNCT_1, EUCLID, RELAT_1, ARYTM_1, BORSUK_2, GRAPH_1, BORSUK_1, ALGSTR_1, SUBSET_1, RCOMP_1, ZFMISC_1, ARYTM_3, METRIC_1, COMPLEX1, WAYBEL20, EQREL_1, CARD_3, VALUED_0, TOPREALB, FINSEQ_1, XCMPLX_0, SIN_COS, INT_1, TOPMETR, SQUARE_1, MCART_1, RVSUM_1, XREAL_0, TOPALG_5, FUNCOP_1, GR_CY_1, TOPS_1, JGRAPH_4, RELAT_2, JGRAPH_2, FUNCT_4, JORDAN, GROUP_6, TOPS_2, PARTFUN1, WAYBEL_1, FINSEQ_6, VECTMETR, PCOMPS_1, IRRAT_1, COMPTRIG, EUCLID_3, VALUED_2, BORSUK_5, LIMFUNC1, NAT_1, STRUCT_0, XXREAL_1, XXREAL_0, CARD_1, ABIAN, ORDINAL1, TARSKI, XBOOLE_0, VALUED_1, SUPINF_2, ORDINAL4, REAL_1, NUMBERS, RLTOPSP1, BINOP_2, FUNCT_2, TOPALG_6, BORSUK_7; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ENUMSET1, EQREL_1, RELAT_1, RVSUM_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, NUMBERS, ORDINAL1, FCONT_1, LIMFUNC1, FUNCOP_1, XCMPLX_0, XXREAL_0, XREAL_0, REAL_1, SQUARE_1, NAT_1, INT_1, CARD_3, FINSEQ_1, FUNCT_4, COMPTRIG, COMPLEX2, VALUED_0, VALUED_1, FINSEQ_2, IRRAT_1, COMPLEX1, ABIAN, SIN_COS, VALUED_2, STRUCT_0, RLVECT_1, METRIC_1, PRE_TOPC, TOPS_1, TMAP_1, TOPS_2, GR_CY_1, CONNSP_1, TOPMETR, RCOMP_1, BORSUK_1, RLTOPSP1, EUCLID, BORSUK_2, PCOMPS_1, EUCLID_3, BORSUK_5, WAYBEL18, JGRAPH_4, JORDAN24, TOPREAL9, TOPREALB, TOPALG_1, TOPALG_3, TOPALG_5, EUCLID_5, TOPREALC, TOPALG_6; constructors BINOP_2, TOPS_1, GRCAT_1, SIN_COS, SEQ_1, ABIAN, TOPREAL9, SQUARE_1, EUCLID_5, FINSEQ_4, TOPALG_5, FINSEQOP, TOPALG_3, BORSUK_6, FCONT_1, TMAP_1, JORDAN24, COMPLEX2, COMPTRIG, EUCLID_3, JGRAPH_4, TOPREALC, WAYBEL18, CONNSP_1, BORSUK_5, FUNCSDOM, LIMFUNC1, COMPLEX1, TOPALG_6; registrations NUMBERS, XBOOLE_0, RELSET_1, FUNCT_2, XXREAL_0, XREAL_0, NAT_1, MEMBERED, STRUCT_0, BORSUK_1, EUCLID, BORSUK_2, VALUED_0, FUNCT_1, RELAT_1, VALUED_1, TOPREALB, PRE_TOPC, RVSUM_1, XCMPLX_0, INT_1, TOPMETR, ABIAN, SQUARE_1, FINSEQ_1, TOPALG_5, SIN_COS6, FUNCOP_1, FUNCT_4, TOPREAL9, SIN_COS, TOPS_1, JORDAN24, TOPGRP_1, VALUED_2, TOPREALC, BORSUK_5, WAYBEL18, FCONT_1, PCOMPS_1, RCOMP_1, FCONT_3, JGRAPH_4, PARTFUN3, FINSEQ_2, TOPALG_6; requirements BOOLE, SUBSET, NUMERALS, ARITHM, REAL; definitions TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XCMPLX_0, SQUARE_1, FUNCT_1, PARTFUN1, FUNCT_2, COMPLEX1, COMPLEX2, INT_1, FINSEQ_1, VALUED_1, FUNCOP_1, FUNCT_4, STRUCT_0, RLTOPSP1, GR_CY_1, BORSUK_2, RVSUM_1, TMAP_1, EUCLID, EUCLID_3, TOPREALB, LATTICE7, VALUED_2, TOPALG_1, LIMFUNC1, TOPALG_6; theorems TARSKI, FUNCT_1, SIN_COS, TOPREAL9, TOPREALB, TOPALG_5, EUCLID, RVSUM_1, VALUED_1, XCMPLX_1, SQUARE_1, EUCLID_2, XBOOLE_0, TOPMETR, FINSEQ_2, FINSEQ_1, RELSET_1, VALUED_0, TSP_1, EUCLID_5, TOPREAL7, TOPREAL6, XREAL_0, BORSUK_1, COMPLEX2, TREAL_1, FUNCT_2, TOPRNS_1, BORSUK_2, XREAL_1, TOPALG_3, FUNCT_4, BINOP_1, FUNCOP_1, ZFMISC_1, XBOOLE_1, NAT_D, XXREAL_0, JORDAN, TOPALG_1, TOPREALA, TOPREAL3, GOBOARD6, JGRAPH_2, TSEP_1, TOPS_1, JORDAN6, FINSEQ_3, ENUMSET1, CARD_3, RCOMP_1, METRIC_1, COMPLEX1, BINOP_2, BVFUNC14, ABSVALUE, NUMBERS, BORSUK_5, SIN_COS4, COMPTRIG, RELAT_1, PRE_TOPC, WAYBEL18, TOPGEN_5, XXREAL_1, INT_1, JORDAN24, EUCLID_3, JGRAPH_4, RLVECT_1, JORDAN5A, JGRAPH_1, VALUED_2, TOPREALC, CONNSP_1, RLTOPSP1, ORDINAL1, FCONT_1, TOPALG_6; schemes FUNCT_2; begin :: Preliminaries reserve a,b,c,x,y,z,X,Y,Z for set, n for Nat, i,j for Integer, r,r1,r2,r3,s for real number, c,c1,c2 for complex number, p for Point of TOP-REAL n; reconsider Q = 0 as Nat; set T2 = TOP-REAL 2; set o2 = |[0,0]|; set o = |[0,0,0]|; set I = the carrier of I[01]; set II = the carrier of [:I[01],I[01]:]; set R = the carrier of R^1; set X01 = [.0,1.[; set K = R^1(X01); set R01 = R^1 | R^1(].0,1.[); reconsider j0 = 0, j1 = 1 as Point of I[01] by BORSUK_1:def 14,def 15; Lm1: II = [:I,I:] by BORSUK_1:def 2; Lm2: 0 in {0} by TARSKI:def 1; Lm3: now let s; assume s <= 1/2; then s <= 1 by XXREAL_0:2; hence 0 <= s implies s in I by BORSUK_1:43; end; Lm4: now let s; set t = s+1/2; assume 0 <= s & s <= 1/2; then Q+1/2 <= t & t <= 1/2+1/2 by XREAL_1:6; hence t in I by BORSUK_1:43; end; registration cluster -> irrational for Element of IRRAT; coherence by BORSUK_5:17; end; theorem Th1: 0 <= r & 0 <= s & r^2 = s^2 implies r = s proof assume that A1: 0 <= r and A2: 0 <= s and A3: r^2 = s^2 and A4: r <> s; -Q >= --s by A1,A3,A4,SQUARE_1:40; hence contradiction by A4,A2,A3,SQUARE_1:40; end; theorem Th2: frac(r) >= frac(s) implies frac(r-s) = frac(r) - frac(s) proof assume A1: frac(r) >= frac(s); set a = r-s - frac(r) + frac(s); A2: a = r-frac(r) - (s-frac(s)); A3: a = r-s+(-frac(r)+frac(s)); -frac(r) <= -frac(s) by A1,XREAL_1:24; then -frac(r)+frac(s) <= -frac(s)+frac(s) by XREAL_1:6; then A4: a <= r-s+Q by A3,XREAL_1:6; A5: a = r-s-(frac(r)-frac(s)); A6: 0 <= frac(s) by INT_1:43; frac(r) < 1 by INT_1:43; then 1+frac(s) > frac(r)+Q by A6,XREAL_1:8; then 1 > frac(r)-frac(s) by XREAL_1:19; then r-s-1 < a by A5,XREAL_1:10; then a = [\r-s/] by A4,A2,INT_1:def 6; hence thesis; end; theorem Th3: frac(r) < frac(s) implies frac(r-s) = frac(r) - frac(s) + 1 proof assume A1: frac(r) < frac(s); set a = r-s - frac(r) + frac(s) - 1; A2: a = r-frac(r) - (s-frac(s)) - 1; A3: a = r-s+(-frac(r)+frac(s)-1); frac(s) < 1 by INT_1:43; then A4: frac(s)-1 < 1-1 by XREAL_1:9; 0 <= frac(r) by INT_1:43; then frac(s)-1-frac(r) <= frac(r)-frac(r) by A4; then A5: r-s-frac(r)+frac(s)-1 <= r-s+Q by A3,XREAL_1:6; A6: a = r-s-1-(frac(r)-frac(s)); frac(r)-frac(r) > frac(r)-frac(s) by A1,XREAL_1:10; then r-s-1-Q < a by A6,XREAL_1:10; then a = [\r-s/] by A5,A2,INT_1:def 6; hence thesis; end; theorem Th4: ex i st frac(r-s) = frac(r) - frac(s) + i & (i = 0 or i = 1) proof frac(r-s) = frac(r)-frac(s)+Q or frac(r-s) = frac(r)-frac(s)+1 by Th2,Th3; hence thesis; end; theorem Th5: sin(r) = 0 implies r = 2*PI*[\r/(2*PI)/] or r = PI+2*PI*[\r/(2*PI)/] proof set i = [\r/(2*PI)/]; assume A1: sin r = 0; consider w being real number such that A2: w = (2*PI)*(-i)+r and A3: 0 <= w and A4: w < 2*PI by COMPLEX2:1; sin w = sin r by A2,COMPLEX2:8; then w = 0 or w = PI by A1,A3,A4,COMPTRIG:17; hence thesis by A2; end; theorem Th6: cos(r) = 0 implies r = PI/2+2*PI*[\r/(2*PI)/] or r = 3*PI/2+2*PI*[\r/(2*PI)/] proof set i = [\r/(2*PI)/]; assume A1: cos r = 0; consider w being real number such that A2: w = (2*PI)*(-i)+r and A3: 0 <= w and A4: w < 2*PI by COMPLEX2:1; cos w = cos r by A2,COMPLEX2:9; then w = PI/2 or w = 3*PI/2 by A1,A3,A4,COMPTRIG:18; hence thesis by A2; end; theorem Th7: sin(r) = 0 implies ex i st r = PI*i proof assume sin(r) = 0; then r = 2*PI*[\r/(2*PI)/] or r = PI+2*PI*[\r/(2*PI)/] by Th5; then r = PI*(2*[\r/(2*PI)/]) or r = PI*(1+2*[\r/(2*PI)/]); hence thesis; end; theorem Th8: cos(r) = 0 implies ex i st r = PI/2+PI*i proof assume cos(r) = 0; then r = PI/2+2*PI*[\r/(2*PI)/] or r = 3*PI/2+2*PI*[\r/(2*PI)/] by Th6; then r = PI/2+PI*(2*[\r/(2*PI)/]) or r = PI/2+PI*(1+2*[\r/(2*PI)/]); hence thesis; end; Lm5: now let r,s; assume sin((r-s)/2) = 0; then consider i such that A1: (r-s)/2 = PI*i by Th7; r = s+2*PI*i by A1; hence ex i st r = s + 2*PI*i; end; theorem Th9: sin(r) = sin(s) implies ex i st r = s + 2*PI*i or r = PI-s + 2*PI*i proof assume A1: sin(r) = sin(s); A2: sin(r) - sin(s) = 2*(cos((r+s)/2)*sin((r-s)/2)) by SIN_COS4:16; per cases by A1,A2; suppose sin((r-s)/2) = 0; hence thesis by Lm5; end; suppose cos((r+s)/2) = 0; then consider i such that A3: (r+s)/2 = PI/2+PI*i by Th8; r = PI-s+2*PI*i by A3; hence thesis; end; end; theorem Th10: cos(r) = cos(s) implies ex i st r = s + 2*PI*i or r = -s + 2*PI*i proof assume A1: cos(r) = cos(s); A2: cos(r) - cos(s) = -2*(sin((r+s)/2)*sin((r-s)/2)) by SIN_COS4:18; per cases by A1,A2; suppose sin((r-s)/2) = 0; hence thesis by Lm5; end; suppose sin((r+s)/2) = 0; then consider i such that A3: (r+s)/2 = PI*i by Th7; r+s-s = 2*PI*i-s by A3; hence thesis; end; end; theorem Th11: sin(r) = sin(s) & cos(r) = cos(s) implies ex i st r = s + 2*PI*i proof assume that A1: sin(r) = sin(s) and A2: cos(r) = cos(s); consider i such that A3: r = s + 2*PI*i or r = PI-s + 2*PI*i by A1,Th9; consider j such that A4: r = s + 2*PI*j or r = -s + 2*PI*j by A2,Th10; per cases by A3,A4; suppose r = s + 2*PI*i or r = s + 2*PI*j; hence thesis; end; suppose r = PI-s + 2*PI*i & r = -s + 2*PI*j; then PI/PI = PI*(2*(j-i))/PI; then PI/PI = 2*(j-i) by XCMPLX_1:89; then 1 = 2*(j-i) by XCMPLX_1:60; then j-i = 1/2; hence thesis by NAT_D:33; end; end; theorem Th12: |.c1.| = |.c2.| & Arg c1 = Arg c2 + 2*PI*i implies c1 = c2 proof assume A1: |.c1.| = |.c2.| & Arg c1 = Arg c2 + 2*PI*i; A2: cos Arg c2 = cos (Arg c2 + 2*PI*i) & sin Arg c2 = sin (Arg c2 + 2*PI*i) by COMPLEX2:8,9; c1 = |.c1.|*cos Arg c1 + |.c1.|*sin Arg c1 * & c2 = |.c2.|*cos Arg c2 + |.c2.|*sin Arg c2 * by COMPTRIG:62; hence c1 = c2 by A1,A2; end; registration let f be one-to-one complex-valued Function; let c; cluster f+c -> one-to-one; coherence proof let x,y; assume that A1: x in dom (f+c) & y in dom (f+c) and A2: (f+c).x = (f+c).y; A3: dom (f+c) = dom f by VALUED_1:def 2; (f+c).x = f.x+c & (f+c).y = f.y+c by A1,VALUED_1:def 2; hence thesis by A1,A3,A2,FUNCT_1:def 4; end; end; registration let f be one-to-one complex-valued Function; let c; cluster f-c -> one-to-one; coherence; end; theorem Th13: for f being complex-valued FinSequence holds len -f = len f proof let f be complex-valued FinSequence; Seg len -f = dom -f by FINSEQ_1:def 3 .= dom f by VALUED_1:def 5 .= Seg len f by FINSEQ_1:def 3; hence len -f = len f by FINSEQ_1:6; end; theorem Th14: -(0*n) = 0*n proof set f = 0*n, g = -f; thus len f = len g by Th13; let k be Nat such that 1 <= k & k <= len g; A1: f.k = 0; thus f.k = -Q .= g.k by A1,VALUED_1:8; end; theorem Th15: for f being complex-valued Function holds f <> 0*n implies -f <> 0*n proof let f be complex-valued Function; assume A1: f <> 0*n; assume -f = 0*n; then --f = -(0*n); hence thesis by A1,Th14; end; theorem Th16: sqr <*r1,r2,r3*> = <* r1^2, r2^2, r3^2 *> proof A1: r1 in REAL & r2 in REAL & r3 in REAL by XREAL_0:def 1; <* r1,r2*> is FinSequence of REAL & <* r3 *> is FinSequence of REAL by TOPREALC:19; hence sqr <*r1,r2,r3*> = sqr <* r1,r2*> ^ sqr <*r3*> by TOPREAL7:10 .= <* r1^2, r2^2 *> ^ sqr <*r3*> by A1,TOPREAL6:11 .= <* r1^2, r2^2, r3^2 *> by RVSUM_1:55; end; theorem Th17: Sum sqr <*r1,r2,r3*> = r1^2+r2^2+r3^2 proof thus Sum sqr <*r1,r2,r3*> = Sum <*r1^2, r2^2, r3^2*> by Th16 .= r1^2+r2^2+r3^2 by RVSUM_1:78; end; theorem Th18: for f being complex-valued FinSequence holds (c(#)f)^2 = (c^2) (#) (f^2) proof let f be complex-valued FinSequence; A1: dom ((c(#)f)^2) = dom (c(#)f) by VALUED_1:11 .= dom f by VALUED_1:def 5; A2: dom ((c^2) (#) (f^2)) = dom (f^2) by VALUED_1:def 5 .= dom f by VALUED_1:11; now let x; assume x in dom ((c(#)f)^2); thus ((c(#)f)^2).x = ((c(#)f).x)^2 by VALUED_1:11 .= (c*(f.x))^2 by VALUED_1:6 .= c^2*(f.x)^2 .= (c^2) * (f^2).x by VALUED_1:11 .= ((c^2) (#) (f^2)).x by VALUED_1:6; end; hence thesis by A1,A2,FUNCT_1:2; end; theorem Th19: for f being complex-valued FinSequence holds (f(/)c)^2 = (f^2) (/) (c^2) proof let f be complex-valued FinSequence; thus (f(/)c)^2 = (1/c)^2 (#) (f^2) by Th18 .= (1*1)/(c*c) (#) (f^2) by XCMPLX_1:76 .= (f^2) (/) (c^2); end; theorem Th20: for f being real-valued FinSequence st Sum f <> 0 holds Sum (f (/) Sum f) = 1 proof let f be real-valued FinSequence; Sum (f (/) Sum f) = Sum f / Sum f by RVSUM_1:87; hence thesis by XCMPLX_1:60; end; Lm6: 1,2,3 are_mutually_different proof thus 1 <> 2 & 1 <> 3 & 2 <> 3; end; definition let a,b,c,x,y,z be set; func (a,b,c) --> (x,y,z) equals ((a,b) --> (x,y)) +* (c .--> z); coherence; end; registration let a,b,c,x,y,z be set; cluster (a,b,c) --> (x,y,z) -> Function-like Relation-like; coherence; end; theorem dom((a,b,c) --> (x,y,z)) = {a,b,c} by BVFUNC14:11; theorem rng((a,b,c) --> (x,y,z)) c= {x,y,z} proof A1: {x,y} \/ {z} = {x,y,z} by ENUMSET1:3; A2: rng((a,b,c) --> (x,y,z)) c= rng((a,b) --> (x,y)) \/ rng(c .--> z) by FUNCT_4:17; A3: rng(c .--> z) = {z} by FUNCOP_1:8; rng((a,b) --> (x,y)) c= {x,y} by FUNCT_4:62; then rng((a,b) --> (x,y)) \/ rng(c .--> z) c= {x,y} \/ {z} by A3,XBOOLE_1:13; hence thesis by A2,A1,XBOOLE_1:1; end; theorem (a,a,a) --> (x,y,z) = a .--> z proof thus (a,a,a) --> (x,y,z) = (a,a) --> (y,z) by FUNCT_4:81 .= a .--> z by FUNCT_4:81; end; theorem (a,a,b) --> (x,y,z) = (a,b) --> (y,z) by FUNCT_4:81; theorem Th25: a <> b implies (a,b,a) --> (x,y,z) = (a,b) --> (z,y) proof assume A1: a <> b; A2: dom ((a,b,a) --> (x,y,z)) = {a,b,a} by BVFUNC14:11 .= {a,a,b} by ENUMSET1:57 .= {a,b} by ENUMSET1:30; hence dom ((a,b,a) --> (x,y,z)) = dom ((a,b) --> (z,y)) by FUNCT_4:62; let k be set; assume A3: k in dom ((a,b,a) --> (x,y,z)); per cases by A2,A3,TARSKI:def 2; suppose A4: k = a; hence ((a,b,a) --> (x,y,z)).k = z by FUNCT_4:89 .= ((a,b) --> (z,y)).k by A1,A4,FUNCT_4:63; end; suppose A5: k = b; thus ((a,b,a) --> (x,y,z)).k = ((a .--> x) +* ((b,a) --> (y,z))).k by FUNCT_4:14 .= y by A1,A5,FUNCT_4:84 .= ((a,b) --> (z,y)).k by A5,FUNCT_4:63; end; end; theorem Th26: (a,b,b) --> (x,y,z) = (a,b) --> (x,z) proof thus (a,b,b) --> (x,y,z) = (a .--> x) +* ((b,b) -->(y,z)) by FUNCT_4:14 .= (a,b) --> (x,z) by FUNCT_4:81; end; theorem a <> b & a <> c implies ((a,b,c) --> (x,y,z)).a = x by BVFUNC14:13; theorem Th28: a,b,c are_mutually_different implies ((a,b,c) --> (x,y,z)).a = x & ((a,b,c) --> (x,y,z)).b = y & ((a,b,c) --> (x,y,z)).c = z proof assume A1: a,b,c are_mutually_different; set f = (a,b) --> (x,y); set g = c .--> z; set h = (a,b,c) --> (x,y,z); A2: a <> b by A1,ZFMISC_1:def 5; a <> c by A1,ZFMISC_1:def 5; then A3: not a in {c} by TARSKI:def 1; b <> c by A1,ZFMISC_1:def 5; then A4: not b in {c} by TARSKI:def 1; A5: c in {c} by TARSKI:def 1; A6: dom g = {c} by FUNCOP_1:13; hence h.a = f.a by A3,FUNCT_4:11 .= x by A2,FUNCT_4:63; thus h.b = f.b by A4,A6,FUNCT_4:11 .= y by FUNCT_4:63; thus h.c = g.c by A5,A6,FUNCT_4:13 .= z by FUNCOP_1:72; end; theorem Th29: for f being Function st dom f = {a,b,c} & f.a = x & f.b = y & f.c = z holds f = (a,b,c) --> (x,y,z) proof let f be Function such that A1: dom f = {a,b,c} and A2: f.a = x & f.b = y & f.c = z; set g = (a,b,c) --> (x,y,z); thus dom f = dom g by A1,BVFUNC14:11; let k be set; assume k in dom f; then A3: k = a or k = b or k = c by A1,ENUMSET1:def 1; per cases; suppose a,b,c are_mutually_different; hence thesis by A2,A3,Th28; end; suppose A4: not a,b,c are_mutually_different; per cases by A4,ZFMISC_1:def 5; suppose A5: a = b & a <> c; then g = (a,c) --> (y,z) by FUNCT_4:81; hence thesis by A5,A2,A3,FUNCT_4:63; end; suppose A6: a = c; per cases; suppose A7: a <> b; then g = (a,b) --> (z,y) by A6,Th25; hence thesis by A6,A2,A3,A7,FUNCT_4:63; end; suppose a = b; hence thesis by A6,A2,A3,FUNCOP_1:72; end; end; suppose A8: b = c & a <> c; then g = (a,b) --> (x,z) by Th26; hence thesis by A8,A2,A3,FUNCT_4:63; end; end; end; theorem Th30: <*a,b,c*> = (1,2,3) --> (a,b,c) proof set f = (1,2,3) --> (a,b,c); set g = <*a,b,c*>; A1: dom g = Seg len g by FINSEQ_1:def 3 .= {1,2,3} by FINSEQ_3:1,FINSEQ_1:45; A2: dom f = {1,2,3} by BVFUNC14:11; now let x be set; assume A3: x in dom f; per cases by A2,A3,ENUMSET1:def 1; suppose A4: x = 1; hence f.x = a by Lm6,Th28 .= g.x by A4,FINSEQ_1:45; end; suppose A5: x = 2; hence f.x = b by Lm6,Th28 .= g.x by A5,FINSEQ_1:45; end; suppose A6: x = 3; hence f.x = c by Lm6,Th28 .= g.x by A6,FINSEQ_1:45; end; end; hence thesis by A1,BVFUNC14:11,FUNCT_1:2; end; theorem Th31: a,b,c are_mutually_different implies product (a,b,c) --> ({x},{y},{z}) = { (a,b,c) --> (x,y,z) } proof assume A1: a,b,c are_mutually_different; set X = { (a,b,c) --> (x,y,z) }, f = (a,b,c) --> ({x},{y},{z}); A2: dom f = {a,b,c} by BVFUNC14:11; now let m be set; thus m in X implies ex g being Function st m = g & dom g = dom f & for x st x in dom f holds g.x in f.x proof assume A3: m in X; take g = (a,b,c) --> (x,y,z); thus m = g by A3,TARSKI:def 1; thus dom g = dom f by A2,BVFUNC14:11; let k be set; assume k in dom f; then A4: k = a or k = b or k = c by A2,ENUMSET1:def 1; g.a = x & f.a = {x} & g.b = y & f.b = {y} & g.c = z & f.c = {z} by A1,Th28; hence g.k in f.k by A4,TARSKI:def 1; end; given g being Function such that A5: m = g and A6: dom g = dom f and A7: for x st x in dom f holds g.x in f.x; a in dom f & b in dom f & c in dom f by A2,ENUMSET1:def 1; then g.a in f.a & g.b in f.b & g.c in f.c & f.a = {x} & f.b = {y} & f.c = {z} by A1,A7,Th28; then g.a = x & g.b = y & g.c = z by TARSKI:def 1; then g = (a,b,c) --> (x,y,z) by A2,A6,Th29; hence m in X by A5,TARSKI:def 1; end; hence thesis by CARD_3:def 5; end; theorem Th32: for A, B, C, D, E, F being set st A c= B & C c= D & E c= F holds product ((a,b,c) --> (A,C,E)) c= product ((a,b,c) --> (B,D,F)) proof let A, B, C, D, E, F be set such that A1: A c= B & C c= D & E c= F; set f = (a,b,c) --> (A,C,E), g = (a,b,c) --> (B,D,F); A2: dom f = {a,b,c} & dom g = {a,b,c} by BVFUNC14:11; per cases; suppose a = c & a <> b; then f = (a,b) --> (E,C) & g = (a,b) --> (F,D) by Th25; hence product f c= product g by A1,TOPREAL6:21; end; suppose b = c & a <> b; then f = (a,b) --> (A,E) & g = (a,b) --> (B,F) by Th26; hence product f c= product g by A1,TOPREAL6:21; end; suppose a = b; then f = (a,c) --> (C,E) & g = (a,c) --> (D,F) by FUNCT_4:81; hence product f c= product g by A1,TOPREAL6:21; end; suppose A3: a <> b & a <> c & b <> c; for x being set st x in dom f holds f.x c= g.x proof let x be set; assume x in dom f; then A4: x = a or x = b or x = c by A2,ENUMSET1:def 1; a,b,c are_mutually_different by A3,ZFMISC_1:def 5; then f.a = A & f.b = C & f.c = E & g.a = B & g.b = D & g.c = F by Th28; hence thesis by A1,A4; end; hence thesis by A2,CARD_3:27; end; end; theorem Th33: a,b,c are_mutually_different & x in X & y in Y & z in Z implies (a,b,c) --> (x,y,z) in product((a,b,c) --> (X,Y,Z)) proof assume A1: a,b,c are_mutually_different; assume x in X & y in Y & z in Z; then {x} c= X & {y} c= Y & {z} c= Z by ZFMISC_1:31; then product((a,b,c)-->({x},{y},{z})) c= product((a,b,c)-->(X,Y,Z)) by Th32; then {(a,b,c)-->(x,y,z)} c= product((a,b,c)-->(X,Y,Z)) by A1,Th31; hence thesis by ZFMISC_1:31; end; definition let f be Function; attr f is odd means :Def2: for x, y being complex-valued Function st x in dom f & -x in dom f & y = f.x holds f.-x = -y; end; registration cluster {} -> odd; coherence proof thus for x, y being complex-valued Function st x in dom {} & -x in dom {} & y = {}.x holds {}.-x = -y; end; end; registration cluster odd for complex-functions-valued Function; existence proof take {}; thus thesis; end; end; set TC2 = Tunit_circle(2); set TC3 = Tunit_circle(3); Lm7: the carrier of TC3 = Sphere(o,1) by EUCLID_5:4,TOPREALB:9; theorem for p being Point of TOP-REAL 3 holds sqr p = <* p`1^2, p`2^2, p`3^2 *> proof let p be Point of TOP-REAL 3; p = |[ p`1, p`2, p`3 ]| by EUCLID_5:3; hence thesis by Th16; end; theorem Th35: for p being Point of TOP-REAL 3 holds Sum sqr p = p`1^2+p`2^2+p`3^2 proof let p be Point of TOP-REAL 3; p = |[ p`1, p`2, p`3 ]| by EUCLID_5:3; hence thesis by Th17; end; reconsider QQ = RAT as Subset of REAL by NUMBERS:12; set RR = R^1|R^1(QQ); Lm8: the carrier of RR = QQ by PRE_TOPC:8; theorem Th36: for S being Subset of R^1 st S = RAT holds RAT /\ ]. -infty,r .[ is open Subset of R^1 | S proof let S be Subset of R^1 such that A1: S = RAT; set X = ]. -infty,r .[; reconsider R = RAT /\ X as Subset of RR by Lm8,XBOOLE_1:17; A2: R^1(X) is open by BORSUK_5:40; R = R^1(X) /\ the carrier of RR by PRE_TOPC:8; hence thesis by A1,A2,TSP_1:def 1; end; theorem Th37: for S being Subset of R^1 st S = RAT holds RAT /\ ]. r,+infty .[ is open Subset of R^1 | S proof let S be Subset of R^1 such that A1: S = RAT; set X = ]. r,+infty .[; reconsider R = RAT /\ X as Subset of RR by Lm8,XBOOLE_1:17; A2: R^1(X) is open by BORSUK_5:40; R = R^1(X) /\ the carrier of RR by PRE_TOPC:8; hence thesis by A1,A2,TSP_1:def 1; end; Lm9: now let T be connected non empty TopSpace; let f be Function of T, RR; let x, y be set such that A1: x in dom f & y in dom f; assume f.x < f.y; then consider r being irrational real number such that A2: f.x < r & r < f.y by BORSUK_5:27; set GX = Image f; A3: f.x in rng f & f.y in rng f by A1,FUNCT_1:def 3; A4: [#]GX = rng f by WAYBEL18:9; thus ex Q1, Q2 being Subset of GX st Q1 misses Q2 & Q1 <> {}GX & Q2 <> {}GX & Q1 is open & Q2 is open & [#]GX = Q1 \/ Q2 proof set Q1 = {q where q is Element of RAT: q in rng f & q < r}; set Q2 = {q where q is Element of RAT: q in rng f & q > r}; Q1 c= rng f proof let x; assume x in Q1; then ex q being Element of RAT st x = q & q in rng f & q < r; hence thesis; end; then reconsider Q1 as Subset of GX by WAYBEL18:9; Q2 c= rng f proof let x; assume x in Q2; then ex q being Element of RAT st x = q & q in rng f & q > r; hence thesis; end; then reconsider Q2 as Subset of GX by WAYBEL18:9; take Q1,Q2; thus Q1 misses Q2 proof assume not thesis; then consider x such that A5: x in Q1 & x in Q2 by XBOOLE_0:3; (ex q being Element of RAT st x = q & q in rng f & q > r) & ex q being Element of RAT st x = q & q in rng f & q < r by A5; hence thesis; end; f.x in Q1 & f.y in Q2 by A2,A3,Lm8; hence Q1 <> {}GX & Q2 <> {}GX; reconsider G1 = RAT /\ ]. -infty,r .[ as open Subset of RR by Th36; reconsider G2 = RAT /\ ]. r,+infty .[ as open Subset of RR by Th37; Q1 = G1 /\ the carrier of GX proof thus Q1 c= G1 /\ the carrier of GX proof let x; assume x in Q1; then consider q being Element of RAT such that A6: x = q and A7: q in rng f and A8: q < r; q in ]. -infty,r .[ by A8,XXREAL_1:233; then q in G1 by XBOOLE_0:def 4; hence thesis by A4,A6,A7,XBOOLE_0:def 4; end; let x; assume A9: x in G1 /\ the carrier of GX; then A10: x in the carrier of GX by XBOOLE_0:def 4; A11: x in G1 by A9,XBOOLE_0:def 4; then reconsider x as Element of RAT by XBOOLE_0:def 4; x in ]. -infty,r .[ by A11,XBOOLE_0:def 4; then x < r by XXREAL_1:233; hence thesis by A4,A10; end; hence Q1 is open by TSP_1:def 1; Q2 = G2 /\ the carrier of GX proof thus Q2 c= G2 /\ the carrier of GX proof let x; assume x in Q2; then consider q being Element of RAT such that A12: x = q and A13: q in rng f and A14: q > r; q in ]. r,+infty .[ by A14,XXREAL_1:235; then q in G2 by XBOOLE_0:def 4; hence thesis by A4,A12,A13,XBOOLE_0:def 4; end; let x; assume A15: x in G2 /\ the carrier of GX; then A16: x in the carrier of GX by XBOOLE_0:def 4; A17: x in G2 by A15,XBOOLE_0:def 4; then reconsider x as Element of RAT by XBOOLE_0:def 4; x in ]. r,+infty .[ by A17,XBOOLE_0:def 4; then x > r by XXREAL_1:235; hence thesis by A4,A16; end; hence Q2 is open by TSP_1:def 1; thus Q1 \/ Q2 = [#]GX proof thus Q1 \/ Q2 c= [#]GX; let x be Element of GX; assume A18: x in [#]GX; x < r or x > r by Lm8,A4,XXREAL_0:1; then x in Q1 or x in Q2 by A18,Lm8,A4; hence thesis by XBOOLE_0:def 3; end; end; end; registration let X be connected non empty TopSpace, Y be non empty TopSpace; let f be continuous Function of X,Y; cluster Image f -> connected; coherence proof set g = corestr(f); A1: dom g = [#]X by FUNCT_2:def 1; rng g = [#](Image f) by FUNCT_2:def 3; then g.:[#]X = [#](Image f) by A1,RELAT_1:113; hence thesis by CONNSP_1:14,WAYBEL18:10; end; end; theorem Th38: for S being Subset of R^1 st S = RAT for T being connected TopSpace, f being Function of T, R^1 | S st f is continuous holds f is constant proof let S be Subset of R^1 such that A1: S = RAT; let T be connected TopSpace; let f be Function of T, R^1 | S such that A2: f is continuous; per cases; suppose A3: T is non empty; set GX = Image f; let x, y be set such that A4: x in dom f & y in dom f and A5: f.x <> f.y; per cases by A5,XXREAL_0:1; suppose f.x < f.y; then ex Q1, Q2 being Subset of GX st Q1 misses Q2 & Q1 <> {}GX & Q2 <> {}GX & Q1 is open & Q2 is open & [#]GX = Q1 \/ Q2 by A1,A3,A4,Lm9; hence thesis by A1,A2,A3,CONNSP_1:11; end; suppose f.y < f.x; then ex Q1, Q2 being Subset of GX st Q1 misses Q2 & Q1 <> {}GX & Q2 <> {}GX & Q1 is open & Q2 is open & [#]GX = Q1 \/ Q2 by A1,A3,A4,Lm9; hence thesis by A1,A2,A3,CONNSP_1:11; end; end; suppose T is empty; hence thesis; end; end; theorem Th39: for a, b being real number, f being continuous Function of Closed-Interval-TSpace(a,b), R^1, g being PartFunc of REAL, REAL st a <= b & f = g holds g is continuous proof set X = R^1; let a, b be real number; set S = Closed-Interval-TSpace(a,b); let f be continuous Function of S, X; let g be PartFunc of REAL, REAL; assume that A1: a <= b and A2: f = g; set A = left_closed_halfline a; set B = [.a,b.]; set C = right_closed_halfline b; the carrier of S = B by A1,TOPMETR:18; then reconsider a1 = a, b1 = b as Point of S by A1,XXREAL_1:1; set f1 = X|R^1(A) --> f.a1; set f2 = X|R^1(C) --> f.b1; A3: the carrier of (X|R^1(A)) = A by PRE_TOPC:8; S = X|R^1(B) by A1,TOPMETR:19; then reconsider f as continuous Function of X|R^1(B), X; A4: dom f1 = the carrier of (X|R^1(A)) by FUNCT_2:def 1 .= A by PRE_TOPC:8; A5: dom f = the carrier of (X|R^1(B)) by FUNCT_2:def 1 .= B by PRE_TOPC:8; A6: dom f2 = the carrier of (X|R^1(C)) by FUNCT_2:def 1 .= C by PRE_TOPC:8; b in REAL by XREAL_0:def 1; then A7: b < +infty by XXREAL_0:9; f1 tolerates f proof let x be set such that A8: x in dom f1 /\ dom f; a in REAL by XREAL_0:def 1; then A /\ B = {a} by A1,XXREAL_0:12,XXREAL_1:417; then A9: x = a by A4,A5,A8,TARSKI:def 1; then a in A by A4,A8,XBOOLE_0:def 4; hence f1.x = f.x by A3,A9,FUNCOP_1:7; end; then reconsider ff = f1+*f as continuous Function of X| (R^1(A) \/ R^1(B)), X by TOPGEN_5:10; set G = ff+*f2; ff tolerates f2 proof let x be set; assume A10: x in dom ff /\ dom f2; then A11: x in dom ff by XBOOLE_0:def 4; A12: x in dom f2 by A10,XBOOLE_0:def 4; then reconsider y = x as Real by A6; A13: b <= y by A6,A12,XXREAL_1:3; A14: dom ff = dom f1 \/ dom f by FUNCT_4:def 1; per cases by A11,A14,XBOOLE_0:def 3; suppose that A15: x in dom f1 and A16: not x in dom f; y <= a by A4,A15,XXREAL_1:2; then b <= a by A13,XXREAL_0:2; then a = b by A1,XXREAL_0:1; hence f2.x = f.a1 by A10,FUNCOP_1:7 .= f1.x by A15,FUNCOP_1:7 .= ff.x by A16,FUNCT_4:11; end; suppose A17: x in dom f; then y <= b by A5,XXREAL_1:1; then b = y by A13,XXREAL_0:1; hence f2.x = f.x by A10,FUNCOP_1:7 .= ff.x by A17,FUNCT_4:13; end; end; then A18: G is continuous Function of X| (R^1(A\/B) \/ R^1(C)), X by TOPGEN_5:10; A19: A \/ B \/ C c= REAL; A20: dom G = dom ff \/ dom f2 by FUNCT_4:def 1 .= dom f1 \/ dom f \/ dom f2 by FUNCT_4:def 1; A21: dom G = REAL proof thus dom G c= REAL by A4,A5,A6,A19,A20; let x be set; assume x in REAL; then reconsider y = x as Real; A22: y < +infty by XXREAL_0:9; A23: -infty < y by XXREAL_0:12; per cases; suppose A24: y < b; per cases; suppose y < a; then y in A by A23,XXREAL_1:2; then y in dom f1 \/ dom f by A4,XBOOLE_0:def 3; hence thesis by A20,XBOOLE_0:def 3; end; suppose y >= a; then y in B by A24,XXREAL_1:1; then y in dom f1 \/ dom f by A5,XBOOLE_0:def 3; hence thesis by A20,XBOOLE_0:def 3; end; end; suppose y >= b; then y in C by A22,XXREAL_1:3; hence thesis by A6,A20,XBOOLE_0:def 3; end; end; then A \/ B \/ C = [#]X by A4,A5,A6,A20,TOPMETR:17; then A25: X| (R^1(A\/B) \/ R^1(C)) = X by TSEP_1:3; rng G c= REAL by TOPMETR:17; then reconsider G as PartFunc of REAL,REAL by A21,RELSET_1:4; A26: G is continuous by A18,A25,JORDAN5A:7; A27: dom f = dom G /\ B by A5,A21,XBOOLE_1:28; now let x be set; assume A28: x in dom f; then reconsider y = x as Real by A5; A29: y <= b by A5,A28,XXREAL_1:1; per cases by A29,XXREAL_0:1; suppose y < b; then not y in dom f2 by A6,XXREAL_1:3; hence G.x = ff.x by FUNCT_4:11 .= f.x by A28,FUNCT_4:13; end; suppose A30: y = b; then A31: x in dom f2 by A6,A7,XXREAL_1:3; hence G.x = f2.x by FUNCT_4:13 .= f.x by A30,A31,FUNCOP_1:7; end; end; then g = G|B by A2,A27,FUNCT_1:46; hence g is continuous by A26; end; definition let s be Point of R^1; let r be real number; redefine func s+r -> Point of R^1; coherence by TOPMETR:17,XREAL_0:def 1; end; definition let s be Point of R^1; let r be real number; redefine func s-r -> Point of R^1; coherence by TOPMETR:17,XREAL_0:def 1; end; definition let X be set; let f be Function of X,R^1; let r; redefine func f+r -> Function of X,R^1; coherence proof r+f is Function of X,REAL; hence thesis by TOPMETR:17; end; end; definition let X be set; let f be Function of X,R^1; let r; redefine func f-r -> Function of X,R^1; coherence proof f-r is Function of X,REAL; hence thesis by TOPMETR:17; end; end; definition let s, t be Point of R^1; let f be Path of s,t; let r be real number; redefine func f+r -> Path of s+r,t+r; coherence proof now thus f+r is continuous; thus (f+r).0 = f.j0+r by VALUED_1:2 .= s+r by BORSUK_2:def 4; thus (f+r).1 = f.j1+r by VALUED_1:2 .= t+r by BORSUK_2:def 4; end; hence thesis by BORSUK_2:def 4; end; redefine func f-r -> Path of s-r,t-r; coherence proof now thus f-r is continuous; thus (f-r).0 = f.j0-r by VALUED_1:2 .= s-r by BORSUK_2:def 4; thus (f-r).1 = f.j1-r by VALUED_1:2 .= t-r by BORSUK_2:def 4; end; hence thesis by BORSUK_2:def 4; end; end; definition func c[100] -> Point of Tunit_circle(3) equals |[1,0,0]|; coherence proof set p = |[1,0,0]|; |. p - 0.TOP-REAL 3 .| = |. p .| by RLVECT_1:13 .= sqrt(p`1^2+p`2^2+p`3^2) by Th35 .= sqrt(1^2+p`2^2+p`3^2) by EUCLID_5:2 .= sqrt(1^2+Q^2+p`3^2) by EUCLID_5:2 .= 1 by EUCLID_5:2,SQUARE_1:18; then p in Sphere(0.TOP-REAL 3,1) by TOPREAL9:9; hence thesis by TOPREALB:9; end; end; reconsider c100 = c[100] as Point of TOP-REAL 3; reconsider c100a = c[100] as Point of Tunit_circle(2+1); definition func c[-100] -> Point of Tunit_circle(3) equals |[-1,0,0]|; coherence proof |[-1,-Q,-Q]| = -c100 by EUCLID_5:11 .= -c[100]; hence thesis by TOPREALC:60; end; end; reconsider mc100 = c[-100] as Point of TOP-REAL 3; theorem Th40: -c[100] = c[-100] proof -c100 = |[-1,-Q,-Q]| by EUCLID_5:11 .= c[-100]; hence thesis; end; theorem -c[-100] = c[100] by Th40; theorem c[100] - c[-100] = |[2,0,0]| proof c100 - mc100 = |[1--1,Q-Q,Q-Q]| by EUCLID_5:13 .= |[2,0,0]|; hence thesis; end; theorem for p being Point of TOP-REAL 2 holds p`1 = |.p.|*cos(Arg p) & p`2 = |.p.|*sin(Arg p) proof let p be Point of T2; set c = euc2cpx(p); A1: c = |.c.|*cos(Arg c) + |.c.|*sin(Arg c)* by COMPTRIG:62; A2: |.c.| = |.p.| by EUCLID_3:25; Re c = p`1 & Im c = p`2 by COMPLEX1:12; hence thesis by A1,A2,COMPLEX1:12; end; theorem for p being Point of TOP-REAL 2 holds p = cpx2euc(|.p.|*cos(Arg p) + |.p.|*sin(Arg p)*) proof let p be Point of T2; set c = euc2cpx(p); A1: c = |.c.|*cos(Arg c) + |.c.|*sin(Arg c)* by COMPTRIG:62; |.c.| = |.p.| by EUCLID_3:25; hence thesis by A1,EUCLID_3:2; end; theorem Th45: for p1, p2 being Point of TOP-REAL 2 holds |.p1.| = |.p2.| & Arg p1 = Arg p2 + 2*PI*i implies p1 = p2 proof let p1, p2 be Point of T2; |.euc2cpx(p1).| = |.p1.| & |.euc2cpx(p2).| = |.p2.| by EUCLID_3:25; hence thesis by Th12,EUCLID_3:4; end; set CM = CircleMap; theorem Th46: for p being Point of TOP-REAL 2 st p = CircleMap.r holds Arg(p) = 2*PI*frac(r) proof let p be Point of T2; set z = euc2cpx(p); set A = 2*PI*frac(r); assume A1: p = CM.r; reconsider q = CM.R^1(r) as Point of T2 by PRE_TOPC:25; A2: |.z.| = |.p.| by EUCLID_3:25; A3: |.q.| = 1 by TOPREALB:12; frac r < 1 & 0 <= frac r by INT_1:43; then A4: 2*PI*Q <= A & A < 2*PI*1 by XREAL_1:68; A5: |[cos(2*PI*r),sin(2*PI*r)]|`1 = cos(2*PI*r) & |[cos(2*PI*r),sin(2*PI*r)]|`2 = sin(2*PI*r) by EUCLID:52; A6: CM.r = |[cos(2*PI*r),sin(2*PI*r)]| by TOPREALB:def 11; A = 2*PI*r + 2*PI*(-[\r/]); then cos(2*PI*r) = cos A & sin(2*PI*r) = sin A by COMPLEX2:8,9; then z = |.z.|*cos A + |.z.|*sin A* by A1,A2,A3,A5,A6; hence thesis by A4,A2,A1,A3,COMPLEX1:44,COMPTRIG:def 1; end; theorem Th47: for p1, p2 being Point of TOP-REAL 3, u1, u2 being Point of Euclid 3 holds u1 = p1 & u2 = p2 implies (Pitag_dist 3).(u1,u2) = sqrt ((p1`1 - p2`1)^2 + (p1`2 - p2`2)^2 + (p1`3 - p2`3)^2) proof let p1, p2 be Point of TOP-REAL 3, u1, u2 be Point of Euclid 3; assume A1: u1 = p1 & u2 = p2; A2: p1 = |[p1`1,p1`2,p1`3]| by EUCLID_5:3; A3: u2 = <* p2`1,p2`2,p2`3 *> by A1,EUCLID_5:3; reconsider v1 = u1, v2 = u2 as Element of REAL 3; v1-v2= <* diffreal.(p1`1,p2`1), diffreal.(p1`2,p2`2), diffreal.(p1`3,p2`3) *> by A1,A2,A3,FINSEQ_2:76 .= <* p1`1-p2`1, diffreal.(p1`2,p2`2), diffreal.(p1`3,p2`3) *> by BINOP_2:def 10 .= <* p1`1-p2`1, p1`2-p2`2, diffreal.(p1`3,p2`3) *> by BINOP_2:def 10 .= <* p1`1-p2`1, p1`2-p2`2, p1`3-p2`3 *> by BINOP_2:def 10; then abs(v1-v2) = <* absreal.(p1`1-p2`1),absreal.(p1`2-p2`2), absreal.(p1`3-p2`3) *> by FINSEQ_2:37 .= <* abs(p1`1-p2`1),absreal.(p1`2-p2`2),absreal.(p1`3-p2`3) *> by EUCLID:def 2 .= <* abs(p1`1-p2`1),abs(p1`2-p2`2),absreal.(p1`3-p2`3) *> by EUCLID:def 2 .= <* abs(p1`1-p2`1),abs(p1`2-p2`2),abs(p1`3-p2`3) *> by EUCLID:def 2; then A4: sqr abs (v1-v2) = <* sqrreal.(abs(p1`1-p2`1)),sqrreal.(abs(p1`2-p2`2)), sqrreal.(abs(p1`3-p2`3)) *> by FINSEQ_2:37 .= <* (abs(p1`1-p2`1))^2,sqrreal.(abs(p1`2-p2`2)), sqrreal.(abs(p1`3-p2`3)) *> by RVSUM_1:def 2 .= <* (abs(p1`1-p2`1))^2,(abs(p1`2-p2`2))^2,sqrreal.(abs(p1`3-p2`3)) *> by RVSUM_1:def 2 .= <* (abs(p1`1-p2`1))^2,(abs(p1`2-p2`2))^2,(abs(p1`3-p2`3))^2 *> by RVSUM_1:def 2 .= <* (p1`1-p2`1)^2,(abs(p1`2-p2`2))^2,(abs(p1`3-p2`3))^2 *> by COMPLEX1:75 .= <* (p1`1-p2`1)^2,(p1`2-p2`2)^2,(abs(p1`3-p2`3))^2 *> by COMPLEX1:75 .= <* (p1`1-p2`1)^2,(p1`2-p2`2)^2,(p1`3-p2`3)^2 *> by COMPLEX1:75; (Pitag_dist 3).(u1,u2) = |.v1 - v2.| by EUCLID:def 6 .= sqrt Sum sqr abs (v1-v2) by EUCLID:25; hence thesis by A4,RVSUM_1:78; end; theorem Th48: for p being Point of TOP-REAL 3, e being Point of Euclid 3 holds p = e & p`3 = 0 implies product ((1,2,3) --> (].p`1-r/sqrt 2,p`1+r/sqrt 2.[, ].p`2-r/sqrt 2,p`2+r/sqrt 2.[,{0})) c= Ball(e,r) proof let p be Point of TOP-REAL 3, e be Point of Euclid 3; set A = ].p`1-r/sqrt 2,p`1+r/sqrt 2.[, B = ].p`2-r/sqrt 2,p`2+r/sqrt 2.[, C = {0}, f = (1,2,3) --> (A,B,C); assume that A1: p = e and A2: p`3 = 0; let a be set; assume a in product f; then consider g being Function such that A3: a = g and A4: dom g = dom f and A5: for x being set st x in dom f holds g.x in f.x by CARD_3:def 5; A6: A = {m where m is Real : p`1-r/sqrt 2 < m & m < p`1+r/sqrt 2 } by RCOMP_1:def 2; A7: B = {n where n is Real : p`2-r/sqrt 2 < n & n < p`2+r/sqrt 2 } by RCOMP_1:def 2; A8: dom f = {1,2,3} by BVFUNC14:11; then A9: 1 in dom f & 2 in dom f & 3 in dom f by ENUMSET1:def 1; A10: f.1 = A & f.2 = B & f.3 = C by Lm6,Th28; then A11: g.1 in A & g.2 in B & g.3 in C by A5,A9; then consider m being Real such that A12: m = g.1 and p`1-r/sqrt 2 < m & m < p`1+r/sqrt 2 by A6; consider n being Real such that A13: n = g.2 and p`2-r/sqrt 2 < n & n < p`2+r/sqrt 2 by A7,A11; g.3 in f.3 by A5,A9; then A14: g.3 = 0 by A10,TARSKI:def 1; p`1+r/sqrt 2 > p`1-r/sqrt 2 by A11,XXREAL_1:28; then p`1-(p`1+r/sqrt 2) < p`1-(p`1-r/sqrt 2) by XREAL_1:10; then -r/sqrt 2+r/sqrt 2 < r/sqrt 2+r/sqrt 2 by XREAL_1:6; then A15: 0 < r; A16: dom <*g.1,g.2,g.3*> = Seg len <*g.1,g.2,g.3*> by FINSEQ_1:def 3 .= {1,2,3} by FINSEQ_3:1,FINSEQ_1:45; now let k be set; assume k in dom g; then k = 1 or k = 2 or k = 3 by A4,A8,ENUMSET1:def 1; hence g.k = <*g.1,g.2,g.3*>.k by FINSEQ_1:45; end; then A17: a = |[m,n,0]| by A3,A4,A12,A13,A16,A14,BVFUNC14:11,FUNCT_1:2; then reconsider c = a as Point of TOP-REAL 3; reconsider b = c as Point of Euclid 3 by TOPREAL3:8; abs(m-p`1) < r/sqrt 2 & abs(n-p`2) < r/sqrt 2 by A11,A12,A13,RCOMP_1:1; then (abs(m-p`1))^2 < (r/sqrt 2)^2 & (abs(n-p`2))^2 < (r/sqrt 2)^2 by SQUARE_1:16; then (abs(m-p`1))^2 < r^2/(sqrt 2)^2 & (abs(n-p`2))^2 < r^2/(sqrt 2)^2 by XCMPLX_1:76; then (abs(m-p`1))^2 < r^2/2 & (abs(n-p`2))^2 < r^2/2 by SQUARE_1:def 2; then (m-p`1)^2 < r^2/2 & (n-p`2)^2 < r^2/2 by COMPLEX1:75; then (m-p`1)^2 + (n-p`2)^2 < r^2/2 + r^2/2 by XREAL_1:8; then sqrt((m-p`1)^2 + (n-p`2)^2) < sqrt(r^2) by SQUARE_1:27; then A18: sqrt((m-p`1)^2 + (n-p`2)^2) < r by A15,SQUARE_1:22; A19: m = c`1 & n = c`2 by A17,EUCLID_5:2; dist(b,e) = (Pitag_dist 3).(b,e) by METRIC_1:def 1 .= sqrt ((c`1 - p`1)^2 + (c`2 - p`2)^2 + (c`3 - p`3)^2) by A1,Th47 .= sqrt ((c`1 - p`1)^2 + (c`2 - p`2)^2 + (Q-Q)^2) by A2,A17,EUCLID_5:2 .= sqrt ((c`1 - p`1)^2 + (c`2 - p`2)^2 + Q); hence a in Ball(e,r) by A18,A19,METRIC_1:11; end; theorem Th49: for s being Real holds Rotate(c,s) = Rotate(c,s+2*PI*i) proof let s be Real; cos (s+Arg c) = cos (s+Arg c+2*PI*i) & sin (s+Arg c) = sin (s+Arg c+2*PI*i) by COMPLEX2:8,9; hence thesis; end; theorem for s being Real holds Rotate(s) = Rotate(s+2*PI*i) proof let s be Real; let p be Point of T2; set q = p`1+(p`2)*; A1: Rotate(q,s) = Rotate(q,s+2*PI*i) by Th49; thus (Rotate(s)).p = |[Re Rotate(q,s),Im Rotate(q,s)]| by JORDAN24:def 3 .= (Rotate(s+2*PI*i)).p by A1,JORDAN24:def 3; end; theorem Th51: for s being Real, p being Point of TOP-REAL 2 holds |.(Rotate(s)).p.| = |.p.| proof let s be Real; let p be Point of T2; set c = euc2cpx(p); set q = (Rotate(s)).p; A1: Re Rotate(c,s) = |.c.|*cos (s+Arg c) & Im Rotate(c,s) = |.c.|*sin (s+Arg c) by COMPLEX1:12; q = cpx2euc(Rotate(c,s)) by JORDAN24:def 3; then A2: q`1 = Re Rotate(c,s) & q`2 = Im Rotate(c,s) by EUCLID:52; |.p.|^2 = |.c.|^2*1 by EUCLID_3:25 .= |.c.|^2*((cos(s+Arg c))^2 + (sin(s+Arg c))^2) by SIN_COS:29 .= (|.c.|*cos(s+Arg c))^2 + (|.c.|*sin(s+Arg c))^2 .= |.q.|^2 by A1,A2,JGRAPH_1:29; hence |.p.| = |.q.| by Th1; end; theorem Th52: for s being Real, p being Point of TOP-REAL 2 holds Arg((Rotate(s)).p) = Arg Rotate(euc2cpx(p),s) proof let s be Real; let p be Point of T2; (Rotate(s)).p = cpx2euc(Rotate(euc2cpx(p),s)) by JORDAN24:def 3; hence thesis by EUCLID_3:1; end; theorem Th53: for s being Real, p being Point of TOP-REAL 2 st p <> 0.TOP-REAL 2 ex i st Arg((Rotate(s)).p) = s+(Arg p)+2*PI*i proof let s be Real; let p be Point of T2; set c = euc2cpx(p); assume p <> 0.T2; then ex i st Arg(Rotate(c,s)) = 2*PI*i+(s+Arg(c)) by COMPLEX2:54,EUCLID_3:18; hence thesis by Th52; end; theorem Th54: for s being Real holds (Rotate(s)).(0.TOP-REAL 2) = 0.TOP-REAL 2 proof let s be Real; thus (Rotate(s)).(0.T2) = cpx2euc(Rotate(euc2cpx(0.T2),s)) by JORDAN24:def 3 .= 0.T2 by COMPLEX2:52,EUCLID_3:16,17; end; theorem Th55: for s being Real, p being Point of TOP-REAL 2 holds (Rotate(s)).p = 0.TOP-REAL 2 implies p = 0.TOP-REAL 2 proof let s be Real; let p be Point of T2; |.p.| = |.(Rotate(s)).p.| by Th51; hence thesis by TOPRNS_1:23,24; end; theorem Th56: for s being Real, p being Point of TOP-REAL 2 holds (Rotate(s)).((Rotate(-s)).p) = p proof let s be Real; let p be Point of T2; set f = Rotate(s); set g = Rotate(-s); per cases; suppose A1: p <> 0.T2; then consider i such that A2: Arg(g.p) = -s+(Arg p)+2*PI*i by Th53; consider j such that A3: Arg(f.(g.p)) = s+(Arg(g.p))+2*PI*j by A1,Th55,Th53; A4: |.f.(g.p).| = |.g.p.| by Th51 .= |.p.| by Th51; Arg(f.(g.p)) = Arg p + 2*PI*(i+j) by A2,A3; hence f.(g.p) = p by A4,Th45; end; suppose A5: p = 0.T2; (Rotate(s)).((Rotate(-s)).(0.T2)) = (Rotate(s)).((0.T2)) by Th54 .= 0.T2 by Th54; hence thesis by A5; end; end; theorem for s being Real holds (Rotate(s)) * (Rotate(-s)) = id TOP-REAL 2 proof let s be Real; let p be Point of T2; set f = Rotate(s); set g = Rotate(-s); thus (f*g).p = f.(g.p) by FUNCT_2:15 .= p by Th56 .= (id T2).p by FUNCT_1:18; end; theorem Th58: for s being Real, p being Point of TOP-REAL 2 holds p in Sphere(0.TOP-REAL 2,r) iff (Rotate(s)).p in Sphere(0.TOP-REAL 2,r) proof let s be Real; let p be Point of T2; A1: |.p.| = |.(Rotate(s)).p.| by Th51; A2: (Rotate(s)).p-0.T2 = (Rotate(s)).p by RLVECT_1:13; hereby assume p in Sphere(0.T2,r); then |.p.| = r by TOPREAL9:12; hence (Rotate(s)).p in Sphere(0.T2,r) by A1,A2,TOPREAL9:9; end; assume (Rotate(s)).p in Sphere(0.T2,r); then A3: |.(Rotate(s)).p.| = r by TOPREAL9:12; A4: (Rotate(-s)).((Rotate(--s)).p) = p by Th56; (Rotate(-s)).((Rotate(s)).p)-0.T2 = (Rotate(-s)).((Rotate(s)).p) by RLVECT_1:13; hence p in Sphere(0.T2,r) by A4,A3,A1,TOPREAL9:9; end; theorem Th59: for r being non negative real number, s being Real holds (Rotate(s)).:Sphere(0.TOP-REAL 2,r) = Sphere(0.TOP-REAL 2,r) proof let r be non negative real number; let s be Real; set f = Rotate(s); set C = Sphere(0.T2,r); thus f.:C c= C proof let y be Point of T2; assume y in f.:C; then ex c being Element of T2 st c in C & y = f.c by FUNCT_2:65; hence y in C by Th58; end; let y be Point of T2; set x = (Rotate(-s)).y; assume y in C; then x in C by Th58; then f.x in f.:C by FUNCT_2:35; hence y in f.:C by Th56; end; definition let r be non negative real number; let s be Real; func RotateCircle(r,s) -> Function of Tcircle(0.TOP-REAL 2,r),Tcircle(0.TOP-REAL 2,r) equals (Rotate(s)) | Tcircle(0.TOP-REAL 2,r); coherence proof set T = Tcircle(0.T2,r); set f = (Rotate(s)) | T; set C = the carrier of T; A1: dom f = C by FUNCT_2:def 1; for x st x in C holds f.x in C proof let x; assume A2: x in C; then A3: f.x = (Rotate(s)).x by FUNCT_1:49; the carrier of T = Sphere(0.T2,r) by TOPREALB:9; hence thesis by A3,A2,Th58; end; hence thesis by A1,FUNCT_2:3; end; end; registration let r be non negative real number, s be Real; cluster RotateCircle(r,s) -> being_homeomorphism; coherence proof set T = Tcircle(0.T2,r); set C = [#]T; C c= [#]T2 by PRE_TOPC:def 4; then reconsider C as Subset of T2; A1: the TopStruct of T2 = TopSpaceMetr Euclid 2 by EUCLID:def 8; then reconsider f = Rotate(s) as Function of TopSpaceMetr Euclid 2, TopSpaceMetr Euclid 2; A2: f is onto isometric by JORDAN24:2; reconsider A = C as Subset of TopSpaceMetr Euclid 2 by A1; T2|C = T by PRE_TOPC:def 5; then A3: (TopSpaceMetr Euclid 2) | A = T by A1,PRE_TOPC:36; the carrier of T = Sphere(0.T2,r) by TOPREALB:9; then (Rotate(s)).:C = C by Th59; hence thesis by A2,A3,JORDAN24:14; end; end; theorem Th60: for p being Point of TOP-REAL 2 st p = CircleMap.r2 holds RotateCircle(1,-Arg(p)).(CircleMap.r1) = CircleMap.(r1-r2) proof let p be Point of T2; assume A1: p = CM.r2; set s = -Arg(p); reconsider q = CM.R^1(r1), w = CM.R^1(r1-r2) as Point of T2 by PRE_TOPC:25; |.q.| = 1 by TOPREALB:12; then q <> 0.T2 by TOPRNS_1:23; then consider i such that A2: Arg((Rotate(s)).q) = s+(Arg q)+2*PI*i by Th53; A3: Arg(p) = 2*PI*frac(r2) by A1,Th46; A4: |.(Rotate(s)).q.| = |.q.| by Th51 .= 1 by TOPREALB:12 .= |.w.| by TOPREALB:12; consider j such that A5: frac(r1-r2) = frac(r1) - frac(r2) + j and j = 0 or j = 1 by Th4; A6: Arg (Rotate(s)).q = -(2*PI*frac(r2))+2*PI*frac(r1)+2*PI*i by A2,A3,Th46 .= 2*PI*frac(r1-r2) + 2*PI*(i-j) by A5 .= Arg w + 2*PI*(i-j) by Th46; thus RotateCircle(1,s).(CM.r1) = (Rotate(s)).q by FUNCT_1:49 .= CM.(r1-r2) by A4,A6,Th45; end; begin :: Main definition let n be non empty Nat; let p be Point of TOP-REAL n; let r be non negative real number; func CircleIso(p,r) -> Function of Tunit_circle(n), Tcircle(p,r) means :Def6: for a being Point of Tunit_circle(n), b being Point of TOP-REAL n st a = b holds it.a = r*b+p; existence proof set U = Tunit_circle(n), C = Tcircle(p,r); defpred P[Point of U,set] means ex w being Point of TOP-REAL n st w = $1 & $2 = r*w+p; A1: r is Real by XREAL_0:def 1; A2: n in NAT by ORDINAL1:def 12; then A3: the carrier of C = Sphere(p,r) by TOPREALB:9; A4: for u being Point of U ex y being Point of C st P[u,y] proof let u be Point of U; reconsider v = u as Point of TOP-REAL n by PRE_TOPC:25; set y = r*v+p; |. y-p .| = |. r*v .| by EUCLID:48 .= abs(r)*|. v .| by A2,A1,TOPRNS_1:7 .= r*|. v .| by ABSVALUE:def 1 .= r*1 by A2,TOPREALB:12; then reconsider y as Point of C by A2,A3,TOPREAL9:9; take y; thus P[u,y]; end; consider f being Function of U,C such that A5: for x being Point of U holds P[x,f.x] from FUNCT_2:sch 3(A4); take f; let a be Point of U, b be Point of TOP-REAL n; P[a,f.a] by A5; hence thesis; end; uniqueness proof let f, g be Function of Tunit_circle(n), Tcircle(p,r) such that A6: for a being Point of Tunit_circle(n), b being Point of TOP-REAL n st a = b holds f.a = r*b+p and A7: for a being Point of Tunit_circle(n), b being Point of TOP-REAL n st a = b holds g.a = r*b+p; let x be Point of Tunit_circle(n); reconsider y = x as Point of TOP-REAL n by PRE_TOPC:25; thus f.x = r*y+p by A6 .= g.x by A7; end; end; registration let n be non empty Nat, p be Point of TOP-REAL n, r be positive real number; cluster CircleIso(p,r) -> being_homeomorphism; coherence proof A1: n in NAT by ORDINAL1:def 12; for a being Point of Tunit_circle(n), b being Point of TOP-REAL n st a = b holds CircleIso(p,r).a = r*b+p by Def6; hence thesis by A1,TOPREALB:19; end; end; definition func SphereMap -> Function of R^1, Tunit_circle(3) means :Def7: for x being real number holds it.x = |[ cos(2*PI*x), sin(2*PI*x), 0 ]|; existence proof defpred P[real number,set] means $2 = |[ cos(2*PI*$1), sin(2*PI*$1), 0 ]|; A1: for x being Element of R^1 ex y being Element of TC3 st P[x,y] proof let x be Element of R^1; set y = |[ cos(2*PI*x), sin(2*PI*x), 0 ]|; |. y - o .| = |. y .| by EUCLID_5:4,RLVECT_1:13 .= sqrt(y`1^2+y`2^2+y`3^2) by Th35 .= sqrt((cos(2*PI*x))^2+y`2^2+y`3^2) by EUCLID_5:2 .= sqrt((cos(2*PI*x))^2+(sin(2*PI*x))^2+y`3^2) by EUCLID_5:2 .= sqrt((cos(2*PI*x))^2+(sin(2*PI*x))^2+Q^2) by EUCLID_5:2 .= 1 by SIN_COS:29,SQUARE_1:18; then y is Element of TC3 by Lm7,TOPREAL9:9; hence thesis; end; consider f being Function of R, TC3 such that A2: for x being Element of R^1 holds P[x,f.x] from FUNCT_2:sch 3(A1); take f; let x be real number; x is Point of R^1 by TOPMETR:17,XREAL_0:def 1; hence thesis by A2; end; uniqueness proof let f, g be Function of R^1, TC3 such that A3: for x being real number holds f.x = |[cos(2*PI*x),sin(2*PI*x),0]| and A4: for x being real number holds g.x = |[cos(2*PI*x),sin(2*PI*x),0]|; let x be Point of R^1; thus f.x = |[cos(2*PI*x),sin(2*PI*x),0]| by A3 .= g.x by A4; end; end; set SM = SphereMap; theorem SphereMap.i = c[100] proof thus SM.i = |[cos(2*PI*i+Q),sin(2*PI*i)+Q,0]| by Def7 .= |[cos(0),sin(2*PI*i+Q),0]| by COMPLEX2:9 .= c[100] by COMPLEX2:8,SIN_COS:31; end; Lm10: sin is Function of R^1,R^1 proof A1: sin = R^1(sin); R^1 | (R^1 dom sin) = R^1 by SIN_COS:24,TOPREALB:6; hence thesis by A1,TOPREALA:7; end; Lm11: cos is Function of R^1,R^1 proof A1: cos = R^1(cos); R^1 | (R^1 dom cos) = R^1 by SIN_COS:24,TOPREALB:6; hence thesis by A1,TOPREALA:7; end; Lm12: SphereMap.r = |[(cos*AffineMap(2*PI,Q)).r, (sin*AffineMap(2*PI,0)).r,0]| proof SphereMap.r = |[cos(2*PI*r+Q),sin(2*PI*r),0]| by Def7 .= |[(cos*AffineMap(2*PI,0)).r,sin(2*PI*r+Q),0]| by TOPREALB:2 .= |[(cos*AffineMap(2*PI,0)).r,(sin*AffineMap(2*PI,0)).r,0]| by TOPREALB:1; hence thesis; end; registration cluster SphereMap -> continuous; coherence proof A1: AffineMap(2*PI,0) = R^1(AffineMap(2*PI,0)); A2: R^1 | (R^1 dom sin) = R^1 by SIN_COS:24,TOPREALB:6; A3: R^1 | (R^1 dom cos) = R^1 by SIN_COS:24,TOPREALB:6; set sR = R^1(sin), cR = R^1(cos); reconsider sR, cR as Function of R^1,R^1 by Lm10,Lm11; reconsider l = AffineMap(2*PI,0) as Function of R^1,R^1 by TOPREALB:8; A4: dom AffineMap(2*PI,0) = REAL by FUNCT_2:def 1; A5: rng AffineMap(2*PI,0) = [#]REAL by FCONT_1:55; set s = sR*l; set c = cR*l; reconsider g = SM as Function of R^1,TOP-REAL 3 by TOPREALA:7; for p being Point of R^1, V being Subset of TOP-REAL 3 st g.p in V & V is open ex W being Subset of R^1 st p in W & W is open & g.:W c= V proof let p be Point of R^1, V be Subset of TOP-REAL 3 such that A6: g.p in V and A7: V is open; A8: V = Int V by A7,TOPS_1:23; A9: c.p is Real & s.p is Real by XREAL_0:def 1; reconsider e = g.p as Point of Euclid 3 by TOPREAL3:8; consider r being real number such that A10: r > 0 and A11: Ball(e,r) c= V by A6,A8,GOBOARD6:5; set A = ].(g.p)`1-r/sqrt 2,(g.p)`1+r/sqrt 2.[; set B = ].(g.p)`2-r/sqrt 2,(g.p)`2+r/sqrt 2.[; set F = (1,2,3) --> (A,B,{0}); A12: g.p = |[c.p,s.p,0]| by Lm12; then A13: (g.p)`2 = s.p by A9,EUCLID_5:2; (g.p)`3 = 0 by A9,A12,EUCLID_5:2; then A14: product F c= Ball(e,r) by Th48; reconsider A, B as Subset of R^1 by TOPMETR:17; A15: A is open by JORDAN6:35; A16: B is open by JORDAN6:35; A17: sR is continuous by A2,PRE_TOPC:26; s.p in B by A10,A13,TOPREAL6:15; then consider Ws being Subset of R^1 such that A18: p in Ws and A19: Ws is open and A20: s.:Ws c= B by A16,A17,A1,A4,A5,JGRAPH_2:10,TOPREALB:5; A21: (g.p)`1 = c.p by A12,A9,EUCLID_5:2; A22: cR is continuous by A3,PRE_TOPC:26; c.p in A by A10,A21,TOPREAL6:15; then consider Wc being Subset of R^1 such that A23: p in Wc and A24: Wc is open and A25: c.:Wc c= A by A15,A22,A1,A4,A5,JGRAPH_2:10,TOPREALB:5; set W = Ws /\ Wc; take W; thus p in W by A18,A23,XBOOLE_0:def 4; thus W is open by A19,A24; let y be Point of TOP-REAL 3; assume y in g.:W; then consider x being Element of R^1 such that A26: x in W and A27: y = g.x by FUNCT_2:65; A28: g.x = |[c.x,s.x,0]| by Lm12; x in Ws by A26,XBOOLE_0:def 4; then A29: s.x in s.:Ws by FUNCT_2:35; x in Wc by A26,XBOOLE_0:def 4; then A30: c.x in c.:Wc by FUNCT_2:35; |[c.x,s.x,0]| = (1,2,3) --> (c.x,s.x,0) by Th30; then |[c.x,s.x,0]| in product F by A20,A25,A29,A30,Lm2,Lm6,Th33; then |[c.x,s.x,0]| in Ball(e,r) by A14; hence y in V by A11,A27,A28; end; then g is continuous by JGRAPH_2:10; hence thesis by PRE_TOPC:27; end; end; definition let r be real number; func eLoop(r) -> Function of I[01], Tunit_circle(3) means :Def8: for x being Point of I[01] holds it.x = |[cos(2*PI*r*x), sin(2*PI*r*x), 0]|; existence proof defpred P[real number,set] means $2 = |[cos(2*PI*r*$1),sin(2*PI*r*$1),0]|; A1: for x being Element of I[01] ex y being Element of TC3 st P[x,y] proof let x be Element of I[01]; set y = |[ cos(2*PI*r*x), sin(2*PI*r*x), 0 ]|; |. y - o .| = |. y .| by EUCLID_5:4,RLVECT_1:13 .= sqrt(y`1^2+y`2^2+y`3^2) by Th35 .= sqrt((cos(2*PI*r*x))^2+y`2^2+y`3^2) by EUCLID_5:2 .= sqrt((cos(2*PI*r*x))^2+(sin(2*PI*r*x))^2+y`3^2) by EUCLID_5:2 .= sqrt((cos(2*PI*r*x))^2+(sin(2*PI*r*x))^2+Q^2) by EUCLID_5:2 .= 1 by SIN_COS:29,SQUARE_1:18; then reconsider y as Element of TC3 by Lm7,TOPREAL9:9; take y; thus P[x,y]; end; ex f being Function of I, TC3 st for x being Element of I[01] holds P[x,f.x] from FUNCT_2:sch 3(A1); hence thesis; end; uniqueness proof let f, g be Function of I[01], TC3 such that A2: for x being Point of I[01] holds f.x = |[cos(2*PI*r*x),sin(2*PI*r*x),0]| and A3: for x being Point of I[01] holds g.x = |[cos(2*PI*r*x),sin(2*PI*r*x),0]|; let x be Point of I[01]; thus f.x = |[cos(2*PI*r*x),sin(2*PI*r*x),0]| by A2 .= g.x by A3; end; end; theorem Th62: eLoop(r) = SphereMap * ExtendInt(r) proof let x be Point of I[01]; A1: (ExtendInt(r)).x = r*x by TOPALG_5:def 1; thus (eLoop(r)).x = |[ cos(2*PI*r*x), sin(2*PI*r*x), 0 ]| by Def8 .= |[ cos(2*PI*(ExtendInt(r)).x), sin(2*PI*(ExtendInt(r)).x), 0 ]| by A1 .= SM.((ExtendInt(r)).x) by Def7 .= (SM * ExtendInt(r)).x by FUNCT_2:15; end; definition let i; redefine func eLoop(i) -> Loop of c[100]; coherence proof set f = eLoop(i); thus c[100],c[100] are_connected; f = SM * ExtendInt(i) by Th62; hence f is continuous; thus f.0 = |[cos(2*PI*i*j0),sin(2*PI*i*j0),0]| by Def8 .= c[100] by SIN_COS:31; thus f.1 = |[cos(2*PI*i*j1),sin(2*PI*i*j1),0]| by Def8 .= |[cos(0),sin(2*PI*i+Q),0]| by COMPLEX2:9 .= c[100] by COMPLEX2:8,SIN_COS:31; end; end; registration let i; cluster eLoop(i) -> nullhomotopic for Loop of c[100]; coherence proof Tunit_circle(3) is having_trivial_Fundamental_Group by TOPALG_6:47; hence thesis; end; end; theorem Th63: p <> 0.TOP-REAL n implies |. p (/) |. p .| .| = 1 proof A1: |.p.|^2 = Sum sqr p by TOPREAL9:5; assume p <> 0.TOP-REAL n; then |.p.| <> 0 by EUCLID_2:42; then Sum (sqr p (/) Sum sqr p) = 1 by A1,Th20; hence thesis by A1,Th19,SQUARE_1:18; end; definition let n be Nat; let p be Point of TOP-REAL n; assume A1: p <> 0.TOP-REAL n; func Rn->S1(p) -> Point of Tcircle(0.TOP-REAL n,1) equals :Def9: p (/) |. p .|; coherence proof A2: n in NAT by ORDINAL1:def 12; |. p (/) |. p .| - 0.TOP-REAL n .| = |. p (/) |. p .| .| by RLVECT_1:13 .= 1 by A1,Th63; then p (/) |. p .| in Sphere(0.TOP-REAL n,1) by A2,TOPREAL9:9; hence thesis by A2,TOPREALB:9; end; end; reserve n for non zero Nat; definition let n be non zero Nat; let f be Function of Tcircle(0.TOP-REAL(n+1),1),TOP-REAL n; set TC4 = Tcircle(0.TOP-REAL(n+1),1); set TC3 = Tunit_circle(n+1); set TC2 = Tunit_circle(n); func Sn1->Sn(f) -> Function of Tunit_circle(n+1),Tunit_circle(n) means :Def10: for x, y being Point of Tcircle(0.TOP-REAL(n+1),1) st y = -x holds it.x = Rn->S1(f.x-f.y); existence proof defpred P[Point of TC4,set] means for y be Point of TC4 st y = -$1 holds $2 = Rn->S1(f.$1-f.y); A1: for x being Element of TC4 ex z being Element of TC2 st P[x,z] proof let x be Element of TC4; reconsider y = -x as Element of TC4 by TOPREALC:60; reconsider z = Rn->S1(f.x-f.y) as Point of TC2; take z; thus thesis; end; ex g being Function of TC4,TC2 st for x being Element of TC4 holds P[x,g.x] from FUNCT_2:sch 3(A1); hence thesis; end; uniqueness proof let F,G be Function of TC3,TC2 such that A2: for x, y being Point of TC4 st y = -x holds F.x = Rn->S1(f.x-f.y) and A3: for x, y being Point of TC4 st y = -x holds G.x = Rn->S1(f.x-f.y); let p be Point of TC3; reconsider p2 = p as Point of TC4; reconsider p1 = -p as Point of TC4 by TOPREALC:60; thus F.p = Rn->S1(f.p2-f.p1) by A2 .= G.p by A3; end; end; definition let x0, y0 be Point of Tunit_circle(2), xt be set, f be Path of x0,y0 such that A1: xt in (CircleMap)"{x0}; func liftPath(f,xt) -> Function of I[01], R^1 means :Def11: it.0 = xt & f = CircleMap*it & it is continuous & for f1 being Function of I[01], R^1 st f1 is continuous & f = CircleMap*f1 & f1.0 = xt holds it = f1; existence by A1,TOPALG_5:23; uniqueness; end; definition let n be Nat, p, x, y be Point of TOP-REAL n, r be real number; pred x,y are_antipodals_of p,r means :Def12: x is Point of Tcircle(p,r) & y is Point of Tcircle(p,r) & p in LSeg(x,y); end; definition let n be Nat, p, x, y be Point of TOP-REAL n, r be real number, f be Function; pred x,y are_antipodals_of p,r,f means :Def13: x,y are_antipodals_of p,r & x in dom f & y in dom f & f.x = f.y; end; definition let m,n be Nat, p be Point of TOP-REAL m, r be real number, f be Function of Tcircle(p,r), TOP-REAL n; attr f is with_antipodals means :Def14: ex x, y being Point of TOP-REAL m st x,y are_antipodals_of p,r,f; end; notation let m,n be Nat, p be Point of TOP-REAL m, r be real number, f be Function of Tcircle(p,r), TOP-REAL n; antonym f is without_antipodals for f is with_antipodals; end; theorem Th64: for n being non empty Nat, r being non negative real number, x being Point of TOP-REAL n st x is Point of Tcircle(0.TOP-REAL n,r) holds x,-x are_antipodals_of 0.TOP-REAL n,r proof let n be non empty Nat, r be non negative real number, x be Point of TOP-REAL n such that A1: x is Point of Tcircle(0.TOP-REAL n,r); reconsider y = x as Point of Tcircle(0.TOP-REAL n,r) by A1; -x = -y; hence x is Point of Tcircle(0.TOP-REAL n,r) & -x is Point of Tcircle(0.TOP-REAL n,r) by TOPREALC:60; (1-1/2)*x + (1/2)*(-x) = (1/2)*x +- (1/2)*x by EUCLID:40 .= 0.TOP-REAL n by EUCLID:36; hence thesis; end; theorem Th65: for n being non empty Nat, p, x, y, x1, y1 being Point of TOP-REAL n, r being positive real number st x,y are_antipodals_of 0.TOP-REAL n,1 & x1 = CircleIso(p,r).x & y1 = CircleIso(p,r).y holds x1,y1 are_antipodals_of p,r proof let n be non empty Nat, p, x, y, x1, y1 be Point of TOP-REAL n, r be positive real number; set h = CircleIso(p,r); assume that A1: x,y are_antipodals_of 0.TOP-REAL n,1 and A2: x1 = h.x and A3: y1 = h.y; A4: x is Point of Tcircle(0.TOP-REAL n,1) by A1,Def12; hence x1 is Point of Tcircle(p,r) by A2,FUNCT_2:5; A5: y is Point of Tcircle(0.TOP-REAL n,1) by A1,Def12; hence y1 is Point of Tcircle(p,r) by A3,FUNCT_2:5; 0.TOP-REAL n in LSeg(x,y) by A1,Def12; then consider a being Real such that A6: 0.TOP-REAL n = (1-a)*x + a*y and A7: 0 <= a & a <= 1; A8: (1-a)*x1 = (1-a)*(r*x+p) by A2,A4,Def6 .= (1-a)*(r*x)+(1-a)*p by EUCLID:32 .= r*(1-a)*x+(1-a)*p by EUCLID:30 .= r*((1-a)*x)+(1-a)*p by EUCLID:30; a*y1 = a*(r*y+p) by A3,A5,Def6 .= a*(r*y)+a*p by EUCLID:32 .= r*a*y+a*p by EUCLID:30 .= r*(a*y)+a*p by EUCLID:30; then (1-a)*x1 + a*y1 = r*((1-a)*x)+(1-a)*p + r*(a*y)+a*p by A8,EUCLID:26 .= r*((1-a)*x) + r*(a*y) + (1-a)*p + a*p by EUCLID:26 .= r*((1-a)*x+(a*y)) + (1-a)*p + a*p by EUCLID:32 .= 0.TOP-REAL n + (1-a)*p + a*p by A6,EUCLID:28 .= (1-a)*p + a*p by EUCLID:27 .= 1*p - a*p + a*p by EUCLID:50 .= 1*p by EUCLID:48 .= p by EUCLID:29; hence thesis by A7; end; theorem Th66: for f being Function of Tcircle(0.TOP-REAL(n+1),1),TOP-REAL n for x being Point of Tcircle(0.TOP-REAL(n+1),1) st f is without_antipodals holds f.x - f.-x <> 0.TOP-REAL n proof set TC4 = Tcircle(0.TOP-REAL(n+1),1); let f be Function of TC4,TOP-REAL n; let x be Point of TC4; assume A1: f is without_antipodals; A2: dom f = the carrier of TC4 by FUNCT_2:def 1; reconsider y = -x as Point of TC4 by TOPREALC:60; reconsider a = x, b = y as Point of TC4; reconsider x1 = x as Point of TOP-REAL(n+1) by PRE_TOPC:25; assume A3: f.x-f.-x = 0.TOP-REAL n; x1,-x1 are_antipodals_of 0.TOP-REAL(n+1),1,f proof thus x1,-x1 are_antipodals_of 0.TOP-REAL(n+1),1 by Th64; f.x = f.a & f.y = f.b; hence x1 in dom f & -x1 in dom f by A2; f.a-f.y = 0.TOP-REAL n by A3; hence f.x1 = f.-x1 by EUCLID:43; end; hence contradiction by A1,Def14; end; theorem Th67: for f being Function of Tcircle(0.TOP-REAL(n+1),1),TOP-REAL n holds f is without_antipodals implies Sn1->Sn(f) is odd proof set TC4 = Tcircle(0.TOP-REAL(n+1),1); let f be Function of TC4,TOP-REAL n; assume A1: f is without_antipodals; set g = Sn1->Sn(f); let x, y be complex-valued Function such that A2: x in dom g and A3: -x in dom g and A4: y = g.x; reconsider b = -x as Point of TC4 by A3; reconsider a = -b as Point of TC4 by A2; set p = f.b-f.a; set q = f.a-f.b; A5: p = -q by EUCLID:44; A6: n in NAT by ORDINAL1:def 12; 0.TOP-REAL n = 0*n by EUCLID:70; then A7: -(p qua real-valued Function) <> 0.TOP-REAL n by A1,Th66,Th15; thus g.-x = Rn->S1(p) by Def10 .= p (/) |. p .| by A1,Th66,Def9 .= p (/) |. -q .| by EUCLID:44 .= (-q) (/) |. -q .| by EUCLID:44 .= -(q qua real-valued Function) (/) |. -q .| by VALUED_2:30 .= -q (/) |.q.| by A6,TOPRNS_1:26 .= -Rn->S1(q) by A5,A7,Def9 .= -y by A4,Def10; end; theorem Th68: for f being Function of Tcircle(0.TOP-REAL(n+1),1),TOP-REAL n for g, B1 being Function of Tcircle(0.TOP-REAL(n+1),1),TOP-REAL n st g = f(-) & B1 = f<-->g & f is without_antipodals holds Sn1->Sn(f) = B1 (n NormF * B1) proof let f be Function of Tcircle(0.TOP-REAL(n+1),1),TOP-REAL n; let g, B1 be Function of Tcircle(0.TOP-REAL(n+1),1),TOP-REAL n such that A1: g = f(-) and A2: B1 = f<-->g and A3: f is without_antipodals; set T = Tcircle(0.TOP-REAL(n+1),1); set B = Sn1->Sn(f); set B2 = (n NormF)*B1; set BB = B1 B2; set TC3 = Tunit_circle(n+1); A4: dom B1 = the carrier of TC3 by FUNCT_2:def 1; dom(n NormF) = the carrier of TOP-REAL n by FUNCT_2:def 1; then rng B1 c= dom(n NormF); then A5: dom B2 = dom B1 by RELAT_1:27; A6: dom BB = dom B1 /\ dom B2 by VALUED_2:71 .= the carrier of TC3 by A5,FUNCT_2:def 1; hence dom B = dom BB by FUNCT_2:def 1; let x be set; assume x in dom B; then reconsider x1 = x as Point of T; reconsider y1 = -x1 as Point of T by TOPREALC:60; set p = f.x1-f.y1; A7: dom g = the carrier of T by FUNCT_2:def 1; A8: B1.x1 = (f.x1) qua real-valued Function - g.x1 by A4,A2,VALUED_2:def 46 .= p by A7,A1,VALUED_2:def 34; A9: B2.x1 = (n NormF).(B1.x1) by FUNCT_2:15 .= |.p.| by A8,JGRAPH_4:def 1; B.x1 = Rn->S1(p) by Def10 .= B1.x1 (/) B2.x1 by A8,A9,A3,Th66,Def9 .= B1.x1 (#) (B2 qua complex-valued Function").x1 by VALUED_1:10 .= BB.x1 by A6,VALUED_2:def 43; hence thesis; end; Lm13: for f being Function of Tcircle(0.TOP-REAL(n+1),1),TOP-REAL n holds f is without_antipodals continuous implies Sn1->Sn(f) is continuous proof set T = Tcircle(0.TOP-REAL(n+1),1); let f be Function of T,TOP-REAL n; assume that A1: f is without_antipodals and A2: f is continuous; set B = Sn1->Sn(f); reconsider g = f(-) as Function of T,TOP-REAL n by TOPREALC:61; reconsider B1 = f<-->g as Function of T,TOP-REAL n by TOPREALC:40; set B2 = (n NormF)*B1; A3: dom g = the carrier of T by FUNCT_2:def 1; A4: dom B1 = the carrier of T by FUNCT_2:def 1; A5: now let t be Point of T; thus B2.t = (n NormF).(B1.t) by FUNCT_2:15 .= |.B1.t.| by JGRAPH_4:def 1; end; A6: now let t be Point of T; A7: n in NAT by ORDINAL1:def 12; A8: B1.t = (f.t) qua real-valued Function - g.t by A4,VALUED_2:def 46 .= (f.t) qua real-valued Function - f.-t by A3,VALUED_2:def 34; f.t - f.-t <> 0.TOP-REAL n by A1,Th66; hence |.B1.t.| <> 0 by A8,A7,TOPRNS_1:24; end; A9: B2 is non-empty proof let x; assume x in dom B2; then reconsider x as Point of T; B2.x = |. B1.x .| by A5; hence thesis by A6; end; A10: g is continuous Function of T,TOP-REAL n by A2,TOPREALC:62; B1B2 is Function of T,TOP-REAL n by TOPREALC:46; hence thesis by A1,Th68,TOPMETR:6,A9,A2,A10; end; deffunc BU(Function of Tcircle(0.TOP-REAL(2+1),1),TOP-REAL 2) = Sn1->Sn($1) * eLoop(1); Lm14: for f being Function of Tcircle(0.TOP-REAL(2+1),1),TOP-REAL 2 holds f is without_antipodals & 0 <= s & s <= 1/2 implies BU(f).(s+1/2) = -(BU(f).s) proof let f be Function of Tcircle(0.TOP-REAL(2+1),1),T2; set l = eLoop(1); set g = Sn1->Sn(f); set t = s+1/2; assume f is without_antipodals; then A1: g is odd by Th67; assume A2: 0 <= s & s <= 1/2; then A3: t in I by Lm4; reconsider s1 = s as Point of I[01] by A2,Lm3; A4: dom g = the carrier of Tunit_circle(2+1) by FUNCT_2:def 1; A5: -(l.s1) is Point of Tcircle(0.TOP-REAL(3),1) by TOPREALC:60; A6: l.t = |[cos(2*PI*1*t), sin(2*PI*1*t), 0]| by A3,Def8 .= |[-cos(2*PI*s), sin(2*PI*s+PI), 0]| by SIN_COS:79 .= |[-cos(2*PI*s), -sin(2*PI*s), -Q]| by SIN_COS:79 .= -|[cos(2*PI*1*s), sin(2*PI*1*s), 0]| by EUCLID_5:11 .= -(l.s1) by Def8; thus BU(f).t = g.(l.t) by A2,Lm4,FUNCT_2:15 .= -(g.(l.s1)) by A1,A4,A5,A6,Def2 .= -(BU(f).s1) by FUNCT_2:15 .= -(BU(f).s); end; defpred qqI[Point of R^1,Point of R^1,Integer] means $1 = $2 + $3/2; Lm15: now let a, b be Point of R^1 such that A1: CircleMap.a = -(CircleMap.b); thus ex I being odd Integer st qqI[a,b,I] proof A2: CM.a = |[cos(2*PI*a),sin(2*PI*a)]| & CM.b = |[cos(2*PI*b),sin(2*PI*b)]| by TOPREALB:def 11; A3: -|[cos(2*PI*b),sin(2*PI*b)]| = |[-cos(2*PI*b),-sin(2*PI*b)]| by EUCLID:60; then A4: cos(2*PI*a) = -cos(2*PI*b) by A1,A2,FINSEQ_1:77 .= cos(PI+2*PI*b) by SIN_COS:79; sin(2*PI*a) = -sin(2*PI*b) by A1,A2,A3,FINSEQ_1:77 .= sin(PI+2*PI*b) by SIN_COS:79; then consider i such that A5: 2*PI*a = PI+2*PI*b + 2*PI*i by A4,Th11; A6: 2*a = PI*(2*a)/PI by XCMPLX_1:89 .= PI * (1 + 2*b + 2*i) / PI by A5 .= 1 + 2*b + 2*i by XCMPLX_1:89; take I = 2*i+1; thus qqI[a,b,I] by A6; end; end; Lm16: for f being Function of Tcircle(0.TOP-REAL(2+1),1),TOP-REAL 2 holds f is without_antipodals continuous implies BU(f) is nullhomotopic Loop of Sn1->Sn(f).c100a proof let f be Function of Tcircle(0.TOP-REAL(2+1),1),TOP-REAL 2; assume f is without_antipodals continuous; then reconsider g = Sn1->Sn(f) as continuous Function of TC3,TC2 by Lm13; BU(f) = g*eLoop(1); hence thesis; end; Lm17: now let f be Function of Tcircle(0.TOP-REAL(2+1),1),TOP-REAL 2; let s; let xt be set such that A1: f is without_antipodals continuous and A2: xt in (CircleMap)"{Sn1->Sn(f).c[100]} and A3: 0 <= s & s <= 1/2; thus ex IT being odd Integer st for L being Loop of Sn1->Sn(f).c100a st L = BU(f) holds liftPath(L,xt).(s+1/2) = (liftPath(L,xt).s) + IT/2 proof reconsider s as Point of I[01] by A3,Lm3; reconsider L = BU(f) as Loop of Sn1->Sn(f).c100a by A1,Lm16; set l = liftPath(L,xt); set t = R^1(s+1/2); reconsider t1 = t as Point of I[01] by A3,Lm4; A4: BU(f) = CM*l by A2,Def11; (CM*l).t1 = CM.(l.t1) & (CM*l).s = CM.(l.s) by FUNCT_2:15; then CM.(l.t) = -CM.(l.s) by A4,A3,A1,Lm14; then consider I being odd Integer such that A5: qqI[l.t1,l.s,I] by Lm15; take I; thus thesis by A5; end; end; defpred qqP[Function of Tcircle(0.TOP-REAL(2+1),1),TOP-REAL 2,set,Integer] means for L being Loop of Sn1->Sn($1).c100a st L = BU($1) for s being real number st 0 <= s & s <= 1/2 holds liftPath(L,$2).(s+1/2) = (liftPath(L,$2).s) + $3/2; Lm18: now let f be Function of Tcircle(0.TOP-REAL(2+1),1),TOP-REAL 2; let xt be set such that A1: f is without_antipodals continuous and A2: xt in (CircleMap)"{Sn1->Sn(f).c[100]}; reconsider L1 = BU(f) as Loop of Sn1->Sn(f).c100a by A1,Lm16; thus ex I being odd Integer st qqP[f,xt,I] proof set l1 = liftPath(L1,xt); set S = [.0,1/2.]; set AF = AffineMap(1,1/2); set W = 2 (#) (l1*(AF|S) - l1); dom AF = REAL by FUNCT_2:def 1; then A3: dom(AF|S) = S by RELAT_1:62; A4: dom l1 = I by FUNCT_2:def 1; A5: rng (AF|S) c= I proof let y be set; assume y in rng(AF|S); then consider x being set such that A6: x in dom(AF|S) and A7: (AF|S).x = y by FUNCT_1:def 3; reconsider x as real number by A6; A8: (AF|S).x = AF.x by A6,FUNCT_1:47 .= 1*x+1/2 by FCONT_1:def 4; 0 <= x & x <= 1/2 by A6,A3,XXREAL_1:1; then Q+1/2 <= x+1/2 & x+1/2 <= 1/2+1/2 by XREAL_1:6; hence thesis by A7,A8,BORSUK_1:43; end; A9: dom(l1*(AF|S) - l1) = dom(l1*(AF|S)) /\ dom l1 by VALUED_1:12 .= dom (AF|S) /\ dom l1 by A4,A5,RELAT_1:27 .= S by A3,A4,BORSUK_1:40,XBOOLE_1:28,XXREAL_1:34; A10: dom W = dom(l1*(AF|S) - l1) by VALUED_1:def 5; rng W c= REAL by VALUED_0:def 3; then reconsider W as PartFunc of REAL,REAL by A9,A10,RELSET_1:4; consider ITj0 being odd Integer such that A11: for L being Loop of Sn1->Sn(f).c100a st L = BU(f) holds liftPath(L,xt).(j0+1/2) = (liftPath(L,xt).j0) + ITj0/2 by A1,A2,Lm17; take ITj0; let L be Loop of Sn1->Sn(f).c100a such that A12: L = BU(f); let s be real number such that A13: 0 <= s & s <= 1/2; set l = liftPath(L,xt); A14: s in S by A13,XXREAL_1:1; A15: 0 in S by XXREAL_1:1; then A16: (AF|S).0 = AF.0 by FUNCT_1:49 .= 1*Q+1/2 by FCONT_1:def 4; A17: (AF|S).s = AF.s by A14,FUNCT_1:49 .= 1*s+1/2 by FCONT_1:def 4; consider ITs being odd Integer such that A18: for L being Loop of Sn1->Sn(f).c100a st L = BU(f) holds liftPath(L,xt).(s+1/2) = (liftPath(L,xt).s) + ITs/2 by A1,A2,A13,Lm17; A19: l1.(j0+1/2) = l1.j0 + ITj0/2 by A11; A20: l1.(s+1/2) = l1.s + ITs/2 by A18; A21: W.0 = 2*((l1*(AF|S) - l1).0) by VALUED_1:6 .= 2*((l1*(AF|S)).0 - l1.0) by A9,A15,VALUED_1:13 .= 2*(l1.(1/2) - l1.0) by A16,A3,A15,FUNCT_1:13 .= 2*(ITj0/2) by A19; A22: W.s = 2*((l1*(AF|S) - l1).s) by VALUED_1:6 .= 2*((l1*(AF|S)).s - l1.s) by A9,A14,VALUED_1:13 .= 2*(l1.(s+1/2) - l1.s) by A17,A3,A14,FUNCT_1:13 .= 2*(ITs/2) by A20; A23: rng W c= INT proof let y be set; assume y in rng W; then consider s being set such that A24: s in dom W and A25: W.s = y by FUNCT_1:def 3; reconsider s as real number by A24; A26: (AF|S).s = AF.s by A9,A10,A24,FUNCT_1:49 .= 1*s+1/2 by FCONT_1:def 4; 0 <= s & s <= 1/2 by A9,A10,A24,XXREAL_1:1; then consider ITs being odd Integer such that A27: for L being Loop of Sn1->Sn(f).c100a st L = BU(f) holds liftPath(L,xt).(s+1/2) = (liftPath(L,xt).s) + ITs/2 by A1,A2,Lm17; A28: l1.(s+1/2) = l1.s + ITs/2 by A27; W.s = 2*(((l1*(AF|S) - l1)).s) by VALUED_1:6 .= 2*((l1*(AF|S)).s - l1.s) by A10,A24,VALUED_1:13 .= 2*(l1.(s+1/2) - l1.s) by A26,A3,A9,A10,A24,FUNCT_1:13 .= 2*(ITs/2) by A28; hence thesis by A25,INT_1:def 2; end; set T = Closed-Interval-TSpace(0,1/2); A29: the carrier of T = S by TOPMETR:18; A30: rng W c= RAT by A23,NUMBERS:14,XBOOLE_1:1; reconsider SR = RAT as Subset of R^1 by NUMBERS:12,TOPMETR:17; reconsider W1 = W as Function of T, R^1 | SR by A10,A9,Lm8,A29,A23,FUNCT_2:2,NUMBERS:14,XBOOLE_1:1; A31: T is connected by TREAL_1:20; A32: R^1 | R^1(dom W) = T by A10,A9,A29,PRE_TOPC:8,TSEP_1:5; reconsider f1 = R^1(AF|S) as Function of T,I[01] by A5,A3,A29,FUNCT_2:2; rng l1 c= REAL by TOPMETR:17; then reconsider ll1 = l1 as PartFunc of REAL,REAL by A4,BORSUK_1:40,RELSET_1:4; l1 is continuous by A2,Def11; then A33: ll1 is continuous by Th39,TOPMETR:20; ll1*(AF|S) - ll1 is continuous by A33; then reconsider W as continuous PartFunc of REAL,REAL; the carrier of R^1 | R^1(rng W) = rng W by PRE_TOPC:8; then A34: R^1 | R^1(rng W) is SubSpace of RR by A30,Lm8,TSEP_1:4; R^1(W) is continuous; then W1 is continuous by A32,A34,PRE_TOPC:26; then W1 is constant by A31,Th38; hence thesis by A20,A12,A21,A22,A9,A10,A15,A14,FUNCT_1:def 10; end; end; Lm19: for f being Function of Tcircle(0.TOP-REAL(2+1),1),TOP-REAL 2 for xt being Point of R^1 for L being Loop of Sn1->Sn(f).c100a st L = BU(f) for I being Integer st qqP[f,xt,I] holds liftPath(L,xt).1 = liftPath(L,xt).0 + I proof let f be Function of Tcircle(0.TOP-REAL(2+1),1),TOP-REAL 2; let xt be Point of R^1; let L be Loop of Sn1->Sn(f).c100a such that A1: L = BU(f); let I be Integer such that A2: qqP[f,xt,I]; set l = liftPath(L,xt); 1/2+1/2 = 1; hence l.1 = l.(Q+1/2) + I/2 by A1,A2 .= l.0 + I/2 + I/2 by A1,A2 .= l.0 + I; end; Lm20: for f being Function of Tcircle(0.TOP-REAL(2+1),1),TOP-REAL 2 holds f is without_antipodals continuous implies not BU(f) is nullhomotopic Loop of Sn1->Sn(f).c100a proof let f be Function of Tcircle(0.TOP-REAL(2+1),1),TOP-REAL 2; assume A1: f is without_antipodals continuous; then reconsider L = BU(f) as Loop of Sn1->Sn(f).c100a by Lm16; set g = Sn1->Sn(f); set s = g.c100a; not L is nullhomotopic proof let c be constant Loop of s; rng CM = the carrier of TC2 by FUNCT_2:def 3; then consider xt being set such that A2: xt in R and A3: CM.xt = s by FUNCT_2:11; reconsider xt as Point of R^1 by A2; s in {s} by TARSKI:def 1; then A4: xt in CM"{s} by A3,FUNCT_2:38; then consider q being odd Integer such that A5: qqP[f,xt,q] by A1,Lm18; reconsider l = liftPath(L,xt) as continuous Function of I[01], R^1 by A4,Def11; A6: l.1 = l.0 + q by A5,Lm19; A7: CM.q = c[10] by TOPREALB:32; A8: CM.0 = c[10] by TOPREALB:32; set hh = l-xt; hh is Path of R^1(0),R^1(q) proof thus hh is continuous; thus hh.0 = l.j0-xt by VALUED_1:4 .= xt-xt by A4,Def11 .= R^1(0); thus hh.1 = l.j1-xt by VALUED_1:4 .= xt+q-xt by A6,A4,Def11 .= R^1(q); end; then reconsider hh as Path of R^1(0),R^1(q); reconsider Ch = CM*hh as Loop of c[10] by A7,TOPREALB:32; reconsider X = I[01] --> xt as Loop of xt by JORDAN:41; set xx = X-xt; reconsider Cx = CM*xx as Loop of c[10] by A8; A9: dom Ciso = the carrier of INT.Group by FUNCT_2:def 1; A10: Ciso.q = Class(EqRel(TC2,c[10]),CM*hh) by TOPALG_5:25; A11: Ciso.0 = Class(EqRel(TC2,c[10]),CM*xx) by TOPALG_5:25; Ciso.@'0 <> Ciso.@'q by A9,FUNCT_1:def 4; then A12: not Cx,Ch are_homotopic by A10,A11,TOPALG_1:46; assume L,c are_homotopic; then consider F being Function of [:I[01],I[01]:], TC2 such that A13: F is continuous and A14: for t being Point of I[01] holds F.(t,0) = BU(f).t & F.(t,1) = c.t & F.(0,t) = s & F.(1,t) = s by BORSUK_2:def 7; reconsider S = s as Point of T2 by PRE_TOPC:25; set A = -Arg(S); set H = RotateCircle(1,A); set G = H*F; A15: |.euc2cpx(S).| = |.S.| by EUCLID_3:25 .= 1 by TOPREALB:12; A16: Rotate(euc2cpx(S),A) = |.euc2cpx(S).| by COMPLEX2:55; A17: H.s = (Rotate(A)).S by FUNCT_1:49 .= c[10] by A16,A15,COMPLEX1:6,JORDAN24:def 3; now let t be Point of I[01]; reconsider E = eLoop(1) as Function of I[01],Tunit_circle(2+1); reconsider BU = BU(f) as Function of I[01],Tunit_circle(2); reconsider T = BU.t as Point of T2 by PRE_TOPC:25; BU(f) = CM*l by A4,Def11; then A18: (BU(f)).t = CM.(l.t) by FUNCT_2:15; thus G.(t,0) = H.(F.(t,j0)) by Lm1,BINOP_1:18 .= H.T by A14 .= CM.(l.t-xt) by A3,A18,Th60 .= CM.(hh.t) by VALUED_1:4 .= Ch.t by FUNCT_2:15; thus G.(t,1) = H.(F.(t,j1)) by Lm1,BINOP_1:18 .= H.(c.t) by A14 .= H.s by TOPALG_3:21 .= CM.(xt-xt) by A17,TOPREALB:32 .= CM.(X.t-xt) by TOPALG_3:21 .= CM.(xx.t) by VALUED_1:4 .= Cx.t by FUNCT_2:15; thus G.(0,t) = H.(F.(j0,t)) by Lm1,BINOP_1:18 .= c[10] by A14,A17; thus G.(1,t) = H.(F.(j1,t)) by Lm1,BINOP_1:18 .= c[10] by A14,A17; end; hence contradiction by A12,A13,BORSUK_2:def 7; end; hence thesis; end; Lm21: for f being continuous Function of Tcircle(0.TOP-REAL(2+1),1),TOP-REAL 2 holds f is with_antipodals proof let f be continuous Function of Tcircle(0.TOP-REAL(2+1),1),T2; assume A1: not thesis; then not BU(f) is nullhomotopic Loop of Sn1->Sn(f).c100a by Lm20; hence contradiction by A1,Lm16; end; registration let n; let r be negative real number, p be Point of TOP-REAL(n+1); cluster -> without_antipodals for Function of Tcircle(p,r),TOP-REAL n; coherence proof let f be Function of Tcircle(p,r),TOP-REAL n; let x, y be Point of TOP-REAL(n+1); not x in dom f; hence not x,y are_antipodals_of p,r,f by Def13; end; end; ::$N Borsuk-Ulam Theorem registration let r be non negative real number, p be Point of TOP-REAL 3; cluster continuous -> with_antipodals for Function of Tcircle(p,r),TOP-REAL 2; coherence proof let f be Function of Tcircle(p,r),T2; assume A1: f is continuous; A2: dom f = the carrier of Tcircle(p,r) by FUNCT_2:def 1; per cases; suppose r is positive; then reconsider r1 = r as positive real number; reconsider f1 = f as continuous Function of Tcircle(p,r1),T2 by A1; reconsider h = CircleIso(p,r1) as Function of Tcircle(0.TOP-REAL 3,1),Tcircle(p,r1); f1*h is with_antipodals by Lm21; then consider x, y being Point of TOP-REAL 3 such that A3: x,y are_antipodals_of 0.TOP-REAL 3,1,f1*h by Def14; A4: x in dom (f*h) by A3,Def13; A5: y in dom (f*h) by A3,Def13; A6: (f*h).x = (f*h).y by A3,Def13; h.x is Point of Tcircle(p,r1) & h.y is Point of Tcircle(p,r1) by A4,A5,FUNCT_2:5; then reconsider hx = h.x, hy = h.y as Point of TOP-REAL 3 by PRE_TOPC:25; take hx,hy; x,y are_antipodals_of 0.TOP-REAL 3,1 by A3,Def13; hence hx,hy are_antipodals_of p,r by Th65; thus hx in dom f by A2,A4,FUNCT_2:5; thus hy in dom f by A2,A5,FUNCT_2:5; thus f.hx = (f*h).x by A4,FUNCT_2:15 .= f.hy by A5,A6,FUNCT_2:15; end; suppose A7: r is zero; take p,p; reconsider e = p as Point of Euclid 3 by TOPREAL3:8; A8: the carrier of Tcircle(p,r) = Sphere(p,r) by TOPREALB:9 .= Sphere(e,r) by TOPREAL9:15 .= {e} by A7,TOPREAL6:54; thus p,p are_antipodals_of p,r proof thus p is Point of Tcircle(p,r) & p is Point of Tcircle(p,r) by A8,TARSKI:def 1; thus p in LSeg(p,p) by RLTOPSP1:68; end; thus p in dom f & p in dom f by A2,A8,TARSKI:def 1; thus f.p = f.p; end; end; end;