:: The {B}orsuk-Ulam Theorem
:: by Artur Korni{\l}owicz and Marco Riccardi
::
:: Received November 3, 2011
:: Copyright (c) 2011-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies 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,
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, 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, ORDINAL1,
NUMBERS, 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, 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,
FUNCT_4, REAL_1;
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, ORDINAL1;
requirements BOOLE, SUBSET, NUMERALS, ARITHM, REAL;
definitions TARSKI, XBOOLE_0, FUNCT_1, PARTFUN1, FUNCT_2, FINSEQ_1, BORSUK_2,
LATTICE7, TOPALG_6;
equalities SUBSET_1, XCMPLX_0, SQUARE_1, COMPLEX1, COMPLEX2, INT_1, FINSEQ_1,
VALUED_1, FUNCT_4, STRUCT_0, RLTOPSP1, GR_CY_1, RVSUM_1, TMAP_1, EUCLID,
EUCLID_3, TOPREALB, VALUED_2, TOPALG_1, LIMFUNC1, RLVECT_1;
expansions TARSKI, ZFMISC_1, FUNCT_1, FUNCT_2, BORSUK_2;
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, 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,
COMPLSP2, RLVECT_4;
schemes FUNCT_2;
begin :: Preliminaries
reserve a,b,c,x,y,z for object,X,Y,Z for set,
n for Nat,
i,j for Integer,
r,r1,r2,r3,s for Real,
c1,c2 for Complex,
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 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 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 * <i> &
c2 = |.c2.|*cos Arg c2 + |.c2.|*sin Arg c2 * <i> by COMPTRIG:62;
hence c1 = c2 by A1,A2;
end;
registration
let f be one-to-one complex-valued Function;
let c be Complex;
cluster f+c -> one-to-one;
coherence
proof
let x,y be object;
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 be Complex;
cluster f-c -> one-to-one;
coherence;
end;
::$CT
theorem Th13:
-(0*n) = 0*n
proof
set f = 0*n, g = -f;
thus len f = len g by COMPLSP2:5;
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 Th14:
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,Th13;
end;
theorem Th15:
sqr <*r1,r2,r3*> = <* r1^2, r2^2, r3^2 *>
proof
<* 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 TOPREAL6:11
.= <* r1^2, r2^2, r3^2 *> by RVSUM_1:55;
end;
theorem Th16:
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 Th15
.= r1^2+r2^2+r3^2 by RVSUM_1:78;
end;
theorem Th17:
for c being Complex
for f being complex-valued FinSequence holds (c(#)f)^2 = (c^2) (#) (f^2)
proof
let c be Complex;
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 be object;
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;
end;
theorem Th18:
for c being Complex
for f being complex-valued FinSequence holds (f(/)c)^2 = (f^2) (/) (c^2)
proof
let c be Complex;
let f be complex-valued FinSequence;
thus (f(/)c)^2 = (1/c)^2 (#) (f^2) by Th17
.= (1*1)/(c*c) (#) (f^2) by XCMPLX_1:76
.= (f^2) (/) (c^2);
end;
theorem Th19:
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_distinct;
::$CD
::$CT 9
theorem Th20:
<*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_1:45,FINSEQ_3:1;
A2: dom f = {1,2,3} by FUNCT_4:128;
now
let x be object;
assume
A3: x in dom f;
per cases by A2,A3,ENUMSET1:def 1;
suppose
A4: x = 1;
hence f.x = a by FUNCT_4:134
.= g.x by A4;
end;
suppose
A5: x = 2;
hence f.x = b by FUNCT_4:135
.= g.x by A5;
end;
suppose
A6: x = 3;
hence f.x = c by FUNCT_4:135
.= g.x by A6;
end;
end;
hence thesis by A1,FUNCT_4:128,FUNCT_1:2;
end;
theorem Th21:
a,b,c are_mutually_distinct implies
product (a,b,c) --> ({x},{y},{z}) = { (a,b,c) --> (x,y,z) }
proof
assume
A1: a,b,c are_mutually_distinct;
set X = { (a,b,c) --> (x,y,z) }, f = (a,b,c) --> ({x},{y},{z});
A2: dom f = {a,b,c} by FUNCT_4:128;
now
let m be object;
thus m in X implies ex g being Function st m = g & dom g = dom f &
for x being object 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,FUNCT_4:128;
let k be object;
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,FUNCT_4:135,134;
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 being object 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,FUNCT_4:135,134;
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,FUNCT_4:136;
hence m in X by A5,TARSKI:def 1;
end;
hence thesis by CARD_3:def 5;
end;
theorem Th22:
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 FUNCT_4:128;
per cases;
suppose a = c & a <> b;
then f = (a,b) --> (E,C) & g = (a,b) --> (F,D) by FUNCT_4:132;
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 FUNCT_4:133;
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 object st x in dom f holds f.x c= g.x
proof
let x be object;
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_distinct by A3;
then f.a = A & f.b = C & f.c = E & g.a = B & g.b = D & g.c = F
by FUNCT_4:135,134;
hence thesis by A1,A4;
end;
hence thesis by A2,CARD_3:27;
end;
end;
theorem Th23:
a,b,c are_mutually_distinct & 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_distinct;
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 Th22;
then {(a,b,c)-->(x,y,z)} c= product((a,b,c)-->(X,Y,Z)) by A1,Th21;
hence thesis by ZFMISC_1:31;
end;
definition
let f be Function;
attr f is odd means
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;
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 Th15;
end;
theorem Th25:
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 Th16;
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 Th26:
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 Th27:
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 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 be object;
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 be object;
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 being object 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 Th26;
reconsider G2 = RAT /\ ]. r,+infty .[ as open Subset of RR by Th27;
Q1 = G1 /\ the carrier of GX
proof
thus Q1 c= G1 /\ the carrier of GX
proof
let x be object;
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 be object;
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 be object;
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 be object;
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 Th28:
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 object 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 Th29:
for a, b being Real,
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;
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))
.= 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))
.= 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 object 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 object;
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;
then
reconsider y = x as Real;
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 object;
assume x in REAL;
then reconsider y = x as Element of 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;
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 object;
assume
A28: x in dom f;
then reconsider y = x as Real;
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;
redefine func s+r -> Point of R^1; :: redefines + (XCMPLX_0, definition)
coherence by TOPMETR:17,XREAL_0:def 1;
end;
definition
let s be Point of R^1;
let r be Real;
redefine func s-r -> Point of R^1; :: redefines - (XCMPLX_0, definition)
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; :: redefines + (VALUED_1, synonym) → + (VALUED_1, definition)
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; :: redefines - (VALUED_1, definition)
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;
redefine func f+r -> Path of s+r,t+r; :: redefines + (VALUED_1, synonym) → + (VALUED_1, definition)
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; :: redefines - (VALUED_1, definition)
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 Th25
.= 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 Th30:
-c[100] = c[-100]
proof
-c100 = |[-1,-Q,-Q]| by EUCLID_5:11
.= c[-100];
hence thesis;
end;
theorem
-c[-100] = c[100] by Th30;
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)*<i> 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)*<i>)
proof
let p be Point of T2;
set c = euc2cpx(p);
A1: c = |.c.|*cos(Arg c) + |.c.|*sin(Arg c)*<i> by COMPTRIG:62;
|.c.| = |.p.| by EUCLID_3:25;
hence thesis by A1,EUCLID_3:2;
end;
theorem Th35:
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 Th36:
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;
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*<i> by A1,A2,A3,A6;
hence thesis by A4,A2,A1,A3,COMPLEX1:44,COMPTRIG:def 1;
end;
theorem Th37:
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;
reconsider p21 = p2`1, p22 = p2`2, p23 = p2`3 as Element of REAL
by XREAL_0:def 1;
reconsider p11 = p1`1, p12 = p1`2, p13 = p1`3 as Element of REAL
by XREAL_0:def 1;
A3: u2 = <* p21,p22,p23 *> by A1,EUCLID_5:3;
reconsider v1 = u1, v2 = u2 as Element of REAL 3;
reconsider d1 = diffreal.(p11,p21), d2 = diffreal.(p12,p22),
d3 = diffreal.(p13,p23) as Element of REAL;
v1-v2= <* d1, d2, d3 *> 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
.= <* |.p1`1-p2`1.|,absreal.(p1`2-p2`2),absreal.(p1`3-p2`3) *>
by EUCLID:def 2
.= <* |.p1`1-p2`1.|,|.p1`2-p2`2.|,absreal.(p1`3-p2`3) *> by EUCLID:def 2
.= <* |.p1`1-p2`1.|,|.p1`2-p2`2.|,|.p1`3-p2`3.| *> by EUCLID:def 2;
then
A4: sqr abs (v1-v2) = <* sqrreal.(|.p1`1-p2`1.|),sqrreal.(|.p1`2-p2`2.|),
sqrreal. |.p1`3-p2`3.| *> by FINSEQ_2:37
.= <* (|.p1`1-p2`1.|)^2,sqrreal.(|.p1`2-p2`2.|),
sqrreal.(|.p1`3-p2`3.|) *> by RVSUM_1:def 2
.= <* (|.p1`1-p2`1.|)^2,(|.p1`2-p2`2.|)^2,sqrreal.(|.p1`3-p2`3.|) *>
by RVSUM_1:def 2
.= <* (|.p1`1-p2`1.|)^2,(|.p1`2-p2`2.|)^2,(|.p1`3-p2`3.|)^2 *>
by RVSUM_1:def 2
.= <* (p1`1-p2`1)^2,(|.p1`2-p2`2.|)^2,(|.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
.= <* (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 Th38:
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 object;
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 object 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 FUNCT_4:128;
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 FUNCT_4:135,134;
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_1:45,FINSEQ_3:1;
now
let k be object;
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;
end;
then
A17: a = |[m,n,0]| by A3,A4,A12,A13,A16,A14,FUNCT_4:128,FUNCT_1:2;
then reconsider c = a as Point of TOP-REAL 3;
reconsider b = c as Point of Euclid 3 by TOPREAL3:8;
|.m-p`1.| < r/sqrt 2 & |.n-p`2.| < r/sqrt 2 by A11,A12,A13,RCOMP_1:1;
then (|.m-p`1.|)^2 < (r/sqrt 2)^2 & (|.n-p`2.|)^2 < (r/sqrt 2)^2
by SQUARE_1:16;
then (|.m-p`1.|)^2 < r^2/(sqrt 2)^2 & (|.n-p`2.|)^2 < r^2/(sqrt 2)^2
by XCMPLX_1:76;
then (|.m-p`1.|)^2 < r^2/2 & (|.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,Th37
.= 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 Th39:
for c being Complex
for s being Real holds Rotate(c,s) = Rotate(c,s+2*PI*i)
proof
let c be Complex;
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)*<i>;
A1: Rotate(q,s) = Rotate(q,s+2*PI*i) by Th39;
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 Th41:
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);
|.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 Th42:
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 Th43:
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 Th42;
end;
theorem Th44:
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 Th45:
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 Th41;
hence thesis by TOPRNS_1:23,24;
end;
theorem Th46:
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 Th43;
consider j such that
A3: Arg(f.(g.p)) = s+(Arg(g.p))+2*PI*j by A1,Th45,Th43;
A4: |.f.(g.p).| = |.g.p.| by Th41
.= |.p.| by Th41;
Arg(f.(g.p)) = Arg p + 2*PI*(i+j) by A2,A3;
hence f.(g.p) = p by A4,Th35;
end;
suppose
A5: p = 0.T2;
(Rotate(s)).((Rotate(-s)).(0.T2)) = (Rotate(s)).((0.T2)) by Th44
.= 0.T2 by Th44;
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 Th46
.= (id T2).p;
end;
theorem Th48:
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 Th41;
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 Th46;
(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 Th49:
for r being non negative Real, 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;
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 Th48;
end;
let y be Point of T2;
set x = (Rotate(-s)).y;
assume y in C;
then x in C by Th48;
then f.x in f.:C by FUNCT_2:35;
hence y in f.:C by Th46;
end;
definition
let r be non negative Real;
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,Th48;
end;
hence thesis by A1,FUNCT_2:3;
end;
end;
registration
let r be non negative Real, 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 Th49;
hence thesis by A2,A3,JORDAN24:14;
end;
end;
theorem Th50:
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 Th43;
A3: Arg(p) = 2*PI*frac(r2) by A1,Th36;
A4: |.(Rotate(s)).q.| = |.q.| by Th41
.= 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,Th36
.= 2*PI*frac(r1-r2) + 2*PI*(i-j) by A5
.= Arg w + 2*PI*(i-j) by Th36;
thus RotateCircle(1,s).(CM.r1) = (Rotate(s)).q by FUNCT_1:49
.= CM.(r1-r2) by A4,A6,Th35;
end;
begin :: Main
definition
let n be non zero Nat;
let p be Point of TOP-REAL n;
let r be non negative Real;
func CircleIso(p,r) -> Function of Tunit_circle(n), Tcircle(p,r) means
:Def5:
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: n in NAT by ORDINAL1:def 12;
then
A2: the carrier of C = Sphere(p,r) by TOPREALB:9;
A3: 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 RLVECT_4:1
.= |.r.|*|. v .| by TOPRNS_1:7
.= r*|. v .| by ABSVALUE:def 1
.= r*1 by A1,TOPREALB:12;
then reconsider y as Point of C by A2,TOPREAL9:9;
take y;
thus P[u,y];
end;
consider f being Function of U,C such that
A4: for x being Point of U holds P[x,f.x] from FUNCT_2:sch 3(A3);
take f;
let a be Point of U, b be Point of TOP-REAL n;
P[a,f.a] by A4;
hence thesis;
end;
uniqueness
proof
let f, g be Function of Tunit_circle(n), Tcircle(p,r) such that
A5: 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
A6: 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 A5
.= g.x by A6;
end;
end;
registration
let n be non zero Nat, p be Point of TOP-REAL n,
r be positive Real;
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 Def5;
hence thesis by A1,TOPREALB:19;
end;
end;
definition
func SphereMap -> Function of R^1, Tunit_circle(3) means
:Def6:
for x being Real holds it.x = |[ cos(2*PI*x), sin(2*PI*x), 0 ]|;
existence
proof
defpred P[Real,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 Th25
.= 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;
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 holds f.x = |[cos(2*PI*x),sin(2*PI*x),0]| and
A4: for x being Real 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 Def6
.= |[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;
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;
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 Def6
.= |[(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;
reconsider e = g.p as Point of Euclid 3 by TOPREAL3:8;
consider r being Real such that
A9: r > 0 and
A10: 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});
A11: g.p = |[c.p,s.p,0]| by Lm12;
then
A12: (g.p)`2 = s.p by EUCLID_5:2;
(g.p)`3 = 0 by A11,EUCLID_5:2;
then
A13: product F c= Ball(e,r) by Th38;
reconsider A, B as Subset of R^1 by TOPMETR:17;
A14: A is open by JORDAN6:35;
A15: B is open by JORDAN6:35;
A16: sR is continuous by A2,PRE_TOPC:26;
s.p in B by A9,A12,TOPREAL6:15;
then consider Ws being Subset of R^1 such that
A17: p in Ws and
A18: Ws is open and
A19: s.:Ws c= B by A15,A16,A1,A4,A5,JGRAPH_2:10,TOPREALB:5;
A20: (g.p)`1 = c.p by A11,EUCLID_5:2;
A21: cR is continuous by A3,PRE_TOPC:26;
c.p in A by A9,A20,TOPREAL6:15;
then consider Wc being Subset of R^1 such that
A22: p in Wc and
A23: Wc is open and
A24: c.:Wc c= A by A14,A21,A1,A4,A5,JGRAPH_2:10,TOPREALB:5;
set W = Ws /\ Wc;
take W;
thus p in W by A17,A22,XBOOLE_0:def 4;
thus W is open by A18,A23;
let y be Point of TOP-REAL 3;
assume y in g.:W;
then consider x being Element of R^1 such that
A25: x in W and
A26: y = g.x by FUNCT_2:65;
A27: g.x = |[c.x,s.x,0]| by Lm12;
x in Ws by A25,XBOOLE_0:def 4;
then
A28: s.x in s.:Ws by FUNCT_2:35;
x in Wc by A25,XBOOLE_0:def 4;
then
A29: c.x in c.:Wc by FUNCT_2:35;
|[c.x,s.x,0]| = (1,2,3) --> (c.x,s.x,0) by Th20;
then |[c.x,s.x,0]| in product F
by A19,A24,A28,A29,Lm2,Lm6,Th23;
then |[c.x,s.x,0]| in Ball(e,r) by A13;
hence y in V by A10,A26,A27;
end;
then g is continuous by JGRAPH_2:10;
hence thesis by PRE_TOPC:27;
end;
end;
definition
let r be Real;
func eLoop(r) -> Function of I[01], Tunit_circle(3) means
:Def7:
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,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 Th25
.= 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 Th52:
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 Def7
.= |[ cos(2*PI*(ExtendInt(r)).x), sin(2*PI*(ExtendInt(r)).x), 0 ]| by A1
.= SM.((ExtendInt(r)).x) by Def6
.= (SM * ExtendInt(r)).x by FUNCT_2:15;
end;
definition
let i;
redefine func eLoop(i) -> Loop of c[100]; :: redefines eLoop (BORSUK_7, definition)
coherence
proof
set f = eLoop(i);
thus c[100],c[100] are_connected;
f = SM * ExtendInt(i) by Th52;
hence f is continuous;
thus f.0 = |[cos(2*PI*i*j0),sin(2*PI*i*j0),0]| by Def7
.= c[100] by SIN_COS:31;
thus f.1 = |[cos(2*PI*i*j1),sin(2*PI*i*j1),0]| by Def7
.= |[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 Th53:
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,Th19;
hence thesis by A1,Th18,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
:Def8:
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,Th53;
then p (/) |. p .| in Sphere(0.TOP-REAL n,1) by 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
:Def9:
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
:Def10:
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;
pred x,y are_antipodals_of p,r means
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,
f be Function;
pred x,y are_antipodals_of p,r,f means
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,
f be Function of Tcircle(p,r), TOP-REAL n;
attr f is with_antipodals means
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,
f be Function of Tcircle(p,r), TOP-REAL n;
antonym f is without_antipodals for f is with_antipodals;
end;
theorem Th54:
for n being non zero Nat,
r being non negative Real,
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 zero Nat,
r be non negative Real,
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 RLVECT_1:25
.= 0.TOP-REAL n by RLVECT_1:5;
hence thesis;
end;
theorem Th55:
for n being non zero Nat,
p, x, y, x1, y1 being Point of TOP-REAL n,
r being positive Real
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 zero Nat,
p, x, y, x1, y1 be Point of TOP-REAL n,
r be positive Real;
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;
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;
hence y1 is Point of Tcircle(p,r) by A3,FUNCT_2:5;
0.TOP-REAL n in LSeg(x,y) by A1;
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,Def5
.= (1-a)*(r*x)+(1-a)*p by RLVECT_1:def 5
.= r*(1-a)*x+(1-a)*p by RLVECT_1:def 7
.= r*((1-a)*x)+(1-a)*p by RLVECT_1:def 7;
a*y1 = a*(r*y+p) by A3,A5,Def5
.= a*(r*y)+a*p by RLVECT_1:def 5
.= r*a*y+a*p by RLVECT_1:def 7
.= r*(a*y)+a*p by RLVECT_1:def 7;
then (1-a)*x1 + a*y1 = r*((1-a)*x)+(1-a)*p + r*(a*y)+a*p
by A8,RLVECT_1:def 3
.= r*((1-a)*x) + r*(a*y) + (1-a)*p + a*p by RLVECT_1:def 3
.= r*((1-a)*x+(a*y)) + (1-a)*p + a*p by RLVECT_1:def 5
.= 0.TOP-REAL n + (1-a)*p + a*p by A6,RLVECT_1:10
.= (1-a)*p + a*p by RLVECT_1:4
.= 1*p - a*p + a*p by RLVECT_1:35
.= 1*p by RLVECT_4:1
.= p by RLVECT_1:def 8;
hence thesis by A7;
end;
theorem Th56:
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 Th54;
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 RLVECT_1:21;
end;
hence contradiction by A1;
end;
theorem Th57:
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 RLVECT_1:33;
0.TOP-REAL n = 0*n by EUCLID:70;
then
A6: -(p qua real-valued Function) <> 0.TOP-REAL n by A1,Th56,Th14;
thus g.-x = Rn->S1(p) by Def9
.= p (/) |. p .| by A1,Th56,Def8
.= p (/) |. -q .| by RLVECT_1:33
.= (-q) (/) |. -q .| by RLVECT_1:33
.= -(q qua real-valued Function) (/) |. -q .| by VALUED_2:30
.= -q (/) |.q.| by TOPRNS_1:26
.= -Rn->S1(q) by A5,A6,Def8
.= -y by A4,Def9;
end;
theorem Th58:
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 object;
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 Def9
.= B1.x1 (/) B2.x1 by A8,A9,A3,Th56,Def8
.= 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: 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,Th56;
hence |.B1.t.| <> 0 by A7,TOPRNS_1:24;
end;
A8: B2 is non-empty
proof
let x be object;
assume x in dom B2;
then reconsider x as Point of T;
B2.x = |. B1.x .| by A5;
hence thesis by A6;
end;
A9: g is continuous Function of T,TOP-REAL n by A2,TOPREALC:62;
B1</>B2 is Function of T,TOP-REAL n by TOPREALC:46;
hence thesis by A1,Th58,A8,A2,A9,TOPMETR:6;
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 Th57;
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,Def7
.= |[-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 Def7;
thus BU(f).t = g.(l.t) by A2,Lm4,FUNCT_2:15
.= -(g.(l.s1)) by A1,A4,A5,A6
.= -(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,Def10;
(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 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 object;
assume y in rng(AF|S);
then consider x being object such that
A6: x in dom(AF|S) and
A7: (AF|S).x = y by FUNCT_1:def 3;
reconsider x as Real 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;
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 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 object;
assume y in rng W;
then consider s being object such that
A24: s in dom W and
A25: W.s = y by FUNCT_1:def 3;
reconsider s as Real 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;
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,Def10;
then
A33: ll1 is continuous by Th29,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,Th28;
hence thesis by A20,A12,A21,A22,A9,A10,A15,A14;
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 object 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,Def10;
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,Def10
.= R^1(0);
thus hh.1 = l.j1-xt by VALUED_1:4
.= xt+q-xt by A6,A4,Def10
.= 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;
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,Def10;
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,Th50
.= 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)
.= 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, 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);
thus not x,y are_antipodals_of p,r,f;
end;
end;
::$N Borsuk-Ulam Theorem
::$L https://en.wikipedia.org/wiki/BorsukâUlam_theorem Borsuk-Ulam Theorem
registration
let r be non negative Real, 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;
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;
A4: x in dom (f*h) by A3;
A5: y in dom (f*h) by A3;
A6: (f*h).x = (f*h).y by A3;
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;
hence hx,hy are_antipodals_of p,r by Th55;
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
by A8,TARSKI:def 1,RLTOPSP1:68;
thus p in dom f & p in dom f by A2,A8,TARSKI:def 1;
thus f.p = f.p;
end;
end;
end;