:: The {B}orsuk-Ulam Theorem
:: by Artur Korni{\l}owicz and Marco Riccardi
::
:: Received November 3, 2011
:: Copyright (c) 2011-2021 Association of Mizar Users


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 [.0,1.[;

set R01 = R^1 | (R^1 ].0,1.[);

reconsider j0 = 0 , j1 = 1 as Point of I[01] by BORSUK_1:def 14, BORSUK_1:def 15;

Lm1: the carrier of [:I[01],I[01]:] = [: the carrier of I[01], the carrier of I[01]:]
by BORSUK_1:def 2;

Lm2: 0 in {0}
by TARSKI:def 1;

Lm3: now :: thesis: for s being Real st s <= 1 / 2 & 0 <= s holds
s in the carrier of I[01]
let s be Real; :: thesis: ( s <= 1 / 2 & 0 <= s implies s in the carrier of I[01] )
assume s <= 1 / 2 ; :: thesis: ( 0 <= s implies s in the carrier of I[01] )
then s <= 1 by XXREAL_0:2;
hence ( 0 <= s implies s in the carrier of I[01] ) by BORSUK_1:43; :: thesis: verum
end;

Lm4: now :: thesis: for s being Real st 0 <= s & s <= 1 / 2 holds
s + (1 / 2) in the carrier of I[01]
let s be Real; :: thesis: ( 0 <= s & s <= 1 / 2 implies s + (1 / 2) in the carrier of I[01] )
set t = s + (1 / 2);
assume ( 0 <= s & s <= 1 / 2 ) ; :: thesis: s + (1 / 2) in the carrier of I[01]
then ( Q + (1 / 2) <= s + (1 / 2) & s + (1 / 2) <= (1 / 2) + (1 / 2) ) by XREAL_1:6;
hence s + (1 / 2) in the carrier of I[01] by BORSUK_1:43; :: thesis: verum
end;

registration
cluster -> irrational for Element of IRRAT ;
coherence
for b1 being Element of IRRAT holds b1 is irrational
by BORSUK_5:17;
end;

theorem Th1: :: BORSUK_7:1
for r, s being Real st 0 <= r & 0 <= s & r ^2 = s ^2 holds
r = s
proof end;

theorem Th2: :: BORSUK_7:2
for r, s being Real st frac r >= frac s holds
frac (r - s) = (frac r) - (frac s)
proof end;

theorem Th3: :: BORSUK_7:3
for r, s being Real st frac r < frac s holds
frac (r - s) = ((frac r) - (frac s)) + 1
proof end;

theorem Th4: :: BORSUK_7:4
for r, s being Real ex i being Integer st
( frac (r - s) = ((frac r) - (frac s)) + i & ( i = 0 or i = 1 ) )
proof end;

theorem Th5: :: BORSUK_7:5
for r being Real holds
( not sin r = 0 or r = (2 * PI) * [\(r / (2 * PI))/] or r = PI + ((2 * PI) * [\(r / (2 * PI))/]) )
proof end;

theorem Th6: :: BORSUK_7:6
for r being Real holds
( not cos r = 0 or r = (PI / 2) + ((2 * PI) * [\(r / (2 * PI))/]) or r = ((3 * PI) / 2) + ((2 * PI) * [\(r / (2 * PI))/]) )
proof end;

theorem Th7: :: BORSUK_7:7
for r being Real st sin r = 0 holds
ex i being Integer st r = PI * i
proof end;

theorem Th8: :: BORSUK_7:8
for r being Real st cos r = 0 holds
ex i being Integer st r = (PI / 2) + (PI * i)
proof end;

Lm5: now :: thesis: for r, s being Real st sin ((r - s) / 2) = 0 holds
ex i being Integer st r = s + ((2 * PI) * i)
let r, s be Real; :: thesis: ( sin ((r - s) / 2) = 0 implies ex i being Integer st r = s + ((2 * PI) * i) )
assume sin ((r - s) / 2) = 0 ; :: thesis: ex i being Integer st r = s + ((2 * PI) * i)
then consider i being Integer such that
A1: (r - s) / 2 = PI * i by Th7;
r = s + ((2 * PI) * i) by A1;
hence ex i being Integer st r = s + ((2 * PI) * i) ; :: thesis: verum
end;

theorem Th9: :: BORSUK_7:9
for r, s being Real st sin r = sin s holds
ex i being Integer st
( r = s + ((2 * PI) * i) or r = (PI - s) + ((2 * PI) * i) )
proof end;

theorem Th10: :: BORSUK_7:10
for r, s being Real st cos r = cos s holds
ex i being Integer st
( r = s + ((2 * PI) * i) or r = (- s) + ((2 * PI) * i) )
proof end;

theorem Th11: :: BORSUK_7:11
for r, s being Real st sin r = sin s & cos r = cos s holds
ex i being Integer st r = s + ((2 * PI) * i)
proof end;

theorem Th12: :: BORSUK_7:12
for i being Integer
for c1, c2 being Complex st |.c1.| = |.c2.| & Arg c1 = (Arg c2) + ((2 * PI) * i) holds
c1 = c2
proof end;

registration
let f be one-to-one complex-valued Function;
let c be Complex;
cluster c + f -> one-to-one ;
coherence
f + c is one-to-one
proof end;
end;

registration
let f be one-to-one complex-valued Function;
let c be Complex;
cluster f - c -> one-to-one ;
coherence
f - c is one-to-one
;
end;

theorem :: BORSUK_7:13
canceled;

::$CT
theorem Th13: :: BORSUK_7:14
for n being Nat holds - (0* n) = 0* n
proof end;

theorem Th14: :: BORSUK_7:15
for n being Nat
for f being complex-valued Function st f <> 0* n holds
- f <> 0* n
proof end;

theorem Th15: :: BORSUK_7:16
for r1, r2, r3 being Real holds sqr <*r1,r2,r3*> = <*(r1 ^2),(r2 ^2),(r3 ^2)*>
proof end;

theorem Th16: :: BORSUK_7:17
for r1, r2, r3 being Real holds Sum (sqr <*r1,r2,r3*>) = ((r1 ^2) + (r2 ^2)) + (r3 ^2)
proof end;

theorem Th17: :: BORSUK_7:18
for c being Complex
for f being complex-valued FinSequence holds (c (#) f) ^2 = (c ^2) (#) (f ^2)
proof end;

theorem Th18: :: BORSUK_7:19
for c being Complex
for f being complex-valued FinSequence holds (f (/) c) ^2 = (f ^2) (/) (c ^2)
proof end;

theorem Th19: :: BORSUK_7:20
for f being real-valued FinSequence st Sum f <> 0 holds
Sum (f (/) (Sum f)) = 1
proof end;

Lm6: 1,2,3 are_mutually_distinct
;

canceled;

theorem :: BORSUK_7:21
canceled;

theorem :: BORSUK_7:22
canceled;

theorem :: BORSUK_7:23
canceled;

theorem :: BORSUK_7:24
canceled;

theorem :: BORSUK_7:25
canceled;

theorem :: BORSUK_7:26
canceled;

theorem :: BORSUK_7:27
canceled;

theorem :: BORSUK_7:28
canceled;

theorem :: BORSUK_7:29
canceled;

::$CD
::$CT 9
theorem Th20: :: BORSUK_7:30
for a, b, c being object holds <*a,b,c*> = (1,2,3) --> (a,b,c)
proof end;

theorem Th21: :: BORSUK_7:31
for a, b, c, x, y, z being object st a,b,c are_mutually_distinct holds
product ((a,b,c) --> ({x},{y},{z})) = {((a,b,c) --> (x,y,z))}
proof end;

theorem Th22: :: BORSUK_7:32
for a, b, c being object
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 end;

theorem Th23: :: BORSUK_7:33
for a, b, c, x, y, z being object
for X, Y, Z being set st a,b,c are_mutually_distinct & x in X & y in Y & z in Z holds
(a,b,c) --> (x,y,z) in product ((a,b,c) --> (X,Y,Z))
proof end;

definition
let f be Function;
attr f is odd means :: BORSUK_7:def 1
for x, y being complex-valued Function st x in dom f & - x in dom f & y = f . x holds
f . (- x) = - y;
end;

:: deftheorem defines odd BORSUK_7:def 1 :
for f being Function holds
( f is odd iff for x, y being complex-valued Function st x in dom f & - x in dom f & y = f . x holds
f . (- x) = - y );

registration
cluster {} -> odd ;
coherence
{} is odd
;
end;

registration
cluster Relation-like Function-like Function-yielding V168() complex-functions-valued odd for set ;
existence
ex b1 being complex-functions-valued Function st b1 is odd
proof end;
end;

set TC2 = Tunit_circle 2;

set TC3 = Tunit_circle 3;

Lm7: the carrier of (Tunit_circle 3) = Sphere (|[0,0,0]|,1)
by EUCLID_5:4, TOPREALB:9;

theorem :: BORSUK_7:34
for p being Point of (TOP-REAL 3) holds sqr p = <*((p `1) ^2),((p `2) ^2),((p `3) ^2)*>
proof end;

theorem Th25: :: BORSUK_7:35
for p being Point of (TOP-REAL 3) holds Sum (sqr p) = (((p `1) ^2) + ((p `2) ^2)) + ((p `3) ^2)
proof end;

reconsider QQ = RAT as Subset of REAL by NUMBERS:12;

set RR = R^1 | (R^1 QQ);

Lm8: the carrier of (R^1 | (R^1 QQ)) = QQ
by PRE_TOPC:8;

theorem Th26: :: BORSUK_7:36
for r being Real
for S being Subset of R^1 st S = RAT holds
RAT /\ ].-infty,r.[ is open Subset of (R^1 | S)
proof end;

theorem Th27: :: BORSUK_7:37
for r being Real
for S being Subset of R^1 st S = RAT holds
RAT /\ ].r,+infty.[ is open Subset of (R^1 | S)
proof end;

Lm9: now :: thesis: for T being non empty connected TopSpace
for f being Function of T,(R^1 | (R^1 QQ))
for x, y being set st x in dom f & y in dom f & f . x < f . y holds
ex Q1, Q2 being Subset of (Image f) st
( Q1 misses Q2 & Q1 <> {} (Image f) & Q2 <> {} (Image f) & Q1 is open & Q2 is open & [#] (Image f) = Q1 \/ Q2 )
let T be non empty connected TopSpace; :: thesis: for f being Function of T,(R^1 | (R^1 QQ))
for x, y being set st x in dom f & y in dom f & f . x < f . y holds
ex Q1, Q2 being Subset of (Image f) st
( Q1 misses Q2 & Q1 <> {} (Image f) & Q2 <> {} (Image f) & Q1 is open & Q2 is open & [#] (Image f) = Q1 \/ Q2 )

let f be Function of T,(R^1 | (R^1 QQ)); :: thesis: for x, y being set st x in dom f & y in dom f & f . x < f . y holds
ex Q1, Q2 being Subset of (Image f) st
( Q1 misses Q2 & Q1 <> {} (Image f) & Q2 <> {} (Image f) & Q1 is open & Q2 is open & [#] (Image f) = Q1 \/ Q2 )

let x, y be set ; :: thesis: ( x in dom f & y in dom f & f . x < f . y implies ex Q1, Q2 being Subset of (Image f) st
( Q1 misses Q2 & Q1 <> {} (Image f) & Q2 <> {} (Image f) & Q1 is open & Q2 is open & [#] (Image f) = Q1 \/ Q2 ) )

assume A1: ( x in dom f & y in dom f ) ; :: thesis: ( f . x < f . y implies ex Q1, Q2 being Subset of (Image f) st
( Q1 misses Q2 & Q1 <> {} (Image f) & Q2 <> {} (Image f) & Q1 is open & Q2 is open & [#] (Image f) = Q1 \/ Q2 ) )

assume f . x < f . y ; :: thesis: ex Q1, Q2 being Subset of (Image f) st
( Q1 misses Q2 & Q1 <> {} (Image f) & Q2 <> {} (Image f) & Q1 is open & Q2 is open & [#] (Image f) = Q1 \/ Q2 )

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: [#] (Image f) = rng f by WAYBEL18:9;
thus ex Q1, Q2 being Subset of (Image f) st
( Q1 misses Q2 & Q1 <> {} (Image f) & Q2 <> {} (Image f) & Q1 is open & Q2 is open & [#] (Image f) = Q1 \/ Q2 ) :: thesis: verum
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 ) } ;
{ q where q is Element of RAT : ( q in rng f & q < r ) } c= rng f
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { q where q is Element of RAT : ( q in rng f & q < r ) } or x in rng f )
assume x in { q where q is Element of RAT : ( q in rng f & q < r ) } ; :: thesis: x in rng f
then ex q being Element of RAT st
( x = q & q in rng f & q < r ) ;
hence x in rng f ; :: thesis: verum
end;
then reconsider Q1 = { q where q is Element of RAT : ( q in rng f & q < r ) } as Subset of (Image f) by WAYBEL18:9;
{ q where q is Element of RAT : ( q in rng f & q > r ) } c= rng f
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { q where q is Element of RAT : ( q in rng f & q > r ) } or x in rng f )
assume x in { q where q is Element of RAT : ( q in rng f & q > r ) } ; :: thesis: x in rng f
then ex q being Element of RAT st
( x = q & q in rng f & q > r ) ;
hence x in rng f ; :: thesis: verum
end;
then reconsider Q2 = { q where q is Element of RAT : ( q in rng f & q > r ) } as Subset of (Image f) by WAYBEL18:9;
take Q1 ; :: thesis: ex Q2 being Subset of (Image f) st
( Q1 misses Q2 & Q1 <> {} (Image f) & Q2 <> {} (Image f) & Q1 is open & Q2 is open & [#] (Image f) = Q1 \/ Q2 )

take Q2 ; :: thesis: ( Q1 misses Q2 & Q1 <> {} (Image f) & Q2 <> {} (Image f) & Q1 is open & Q2 is open & [#] (Image f) = Q1 \/ Q2 )
thus Q1 misses Q2 :: thesis: ( Q1 <> {} (Image f) & Q2 <> {} (Image f) & Q1 is open & Q2 is open & [#] (Image f) = Q1 \/ Q2 )
proof
assume not Q1 misses Q2 ; :: thesis: contradiction
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 contradiction ; :: thesis: verum
end;
( f . x in Q1 & f . y in Q2 ) by A2, A3, Lm8;
hence ( Q1 <> {} (Image f) & Q2 <> {} (Image f) ) ; :: thesis: ( Q1 is open & Q2 is open & [#] (Image f) = Q1 \/ Q2 )
reconsider G1 = RAT /\ ].-infty,r.[ as open Subset of (R^1 | (R^1 QQ)) by Th26;
reconsider G2 = RAT /\ ].r,+infty.[ as open Subset of (R^1 | (R^1 QQ)) by Th27;
Q1 = G1 /\ the carrier of (Image f)
proof
thus Q1 c= G1 /\ the carrier of (Image f) :: according to XBOOLE_0:def 10 :: thesis: G1 /\ the carrier of (Image f) c= Q1
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Q1 or x in G1 /\ the carrier of (Image f) )
assume x in Q1 ; :: thesis: x in G1 /\ the carrier of (Image f)
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 x in G1 /\ the carrier of (Image f) by A4, A6, A7, XBOOLE_0:def 4; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in G1 /\ the carrier of (Image f) or x in Q1 )
assume A9: x in G1 /\ the carrier of (Image f) ; :: thesis: x in Q1
then A10: x in the carrier of (Image f) by XBOOLE_0:def 4;
A11: x in G1 by A9, XBOOLE_0:def 4;
then reconsider x = 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 x in Q1 by A4, A10; :: thesis: verum
end;
hence Q1 is open by TSP_1:def 1; :: thesis: ( Q2 is open & [#] (Image f) = Q1 \/ Q2 )
Q2 = G2 /\ the carrier of (Image f)
proof
thus Q2 c= G2 /\ the carrier of (Image f) :: according to XBOOLE_0:def 10 :: thesis: G2 /\ the carrier of (Image f) c= Q2
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Q2 or x in G2 /\ the carrier of (Image f) )
assume x in Q2 ; :: thesis: x in G2 /\ the carrier of (Image f)
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 x in G2 /\ the carrier of (Image f) by A4, A12, A13, XBOOLE_0:def 4; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in G2 /\ the carrier of (Image f) or x in Q2 )
assume A15: x in G2 /\ the carrier of (Image f) ; :: thesis: x in Q2
then A16: x in the carrier of (Image f) by XBOOLE_0:def 4;
A17: x in G2 by A15, XBOOLE_0:def 4;
then reconsider x = 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 x in Q2 by A4, A16; :: thesis: verum
end;
hence Q2 is open by TSP_1:def 1; :: thesis: [#] (Image f) = Q1 \/ Q2
thus Q1 \/ Q2 = [#] (Image f) :: thesis: verum
proof
thus Q1 \/ Q2 c= [#] (Image f) ; :: according to XBOOLE_0:def 10 :: thesis: [#] (Image f) c= Q1 \/ Q2
let x be Element of (Image f); :: according to LATTICE7:def 1 :: thesis: ( not x in [#] (Image f) or x in Q1 \/ Q2 )
assume A18: x in [#] (Image f) ; :: thesis: x in Q1 \/ Q2
( x < r or x > r ) by Lm8, A4, XXREAL_0:1;
then ( x in Q1 or x in Q2 ) by A18, Lm8, A4;
hence x in Q1 \/ Q2 by XBOOLE_0:def 3; :: thesis: verum
end;
end;
end;

registration
let X be non empty connected TopSpace;
let Y be non empty TopSpace;
let f be continuous Function of X,Y;
cluster Image f -> connected ;
coherence
Image f is connected
proof end;
end;

theorem Th28: :: BORSUK_7:38
for S being Subset of R^1 st S = RAT holds
for T being connected TopSpace
for f being Function of T,(R^1 | S) st f is continuous holds
f is constant
proof end;

theorem Th29: :: BORSUK_7:39
for a, b being Real
for f being continuous Function of (Closed-Interval-TSpace (a,b)),R^1
for g being PartFunc of REAL,REAL st a <= b & f = g holds
g is continuous
proof end;

definition
let s be Point of R^1;
let r be Real;
:: original: +
redefine func s + r -> Point of R^1;
coherence
s + r is Point of R^1
by TOPMETR:17, XREAL_0:def 1;
end;

definition
let s be Point of R^1;
let r be Real;
:: original: -
redefine func s - r -> Point of R^1;
coherence
s - r is Point of R^1
by TOPMETR:17, XREAL_0:def 1;
end;

definition
let X be set ;
let f be Function of X,R^1;
let r be Real;
:: original: +
redefine func f + r -> Function of X,R^1;
coherence
r + f is Function of X,R^1
proof end;
end;

definition
let X be set ;
let f be Function of X,R^1;
let r be Real;
:: original: -
redefine func f - r -> Function of X,R^1;
coherence
f - r is Function of X,R^1
proof end;
end;

definition
let s, t be Point of R^1;
let f be Path of s,t;
let r be Real;
:: original: +
redefine func f + r -> Path of s + r,t + r;
coherence
r + f is Path of s + r,t + r
proof end;
:: original: -
redefine func f - r -> Path of s - r,t - r;
coherence
f - r is Path of s - r,t - r
proof end;
end;

definition
func c[100] -> Point of (Tunit_circle 3) equals :: BORSUK_7:def 2
|[1,0,0]|;
coherence
|[1,0,0]| is Point of (Tunit_circle 3)
proof end;
end;

:: deftheorem defines c[100] BORSUK_7:def 2 :
c[100] = |[1,0,0]|;

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 :: BORSUK_7:def 3
|[(- 1),0,0]|;
coherence
|[(- 1),0,0]| is Point of (Tunit_circle 3)
proof end;
end;

:: deftheorem defines c[-100] BORSUK_7:def 3 :
c[-100] = |[(- 1),0,0]|;

reconsider mc100 = c[-100] as Point of (TOP-REAL 3) ;

theorem Th30: :: BORSUK_7:40
- c[100] = c[-100]
proof end;

theorem :: BORSUK_7:41
- c[-100] = c[100] by Th30;

theorem :: BORSUK_7:42
c[100] - c[-100] = |[2,0,0]|
proof end;

theorem :: BORSUK_7:43
for p being Point of (TOP-REAL 2) holds
( p `1 = |.p.| * (cos (Arg p)) & p `2 = |.p.| * (sin (Arg p)) )
proof end;

theorem :: BORSUK_7:44
for p being Point of (TOP-REAL 2) holds p = cpx2euc ((|.p.| * (cos (Arg p))) + ((|.p.| * (sin (Arg p))) * <i>))
proof end;

theorem Th35: :: BORSUK_7:45
for i being Integer
for p1, p2 being Point of (TOP-REAL 2) st |.p1.| = |.p2.| & Arg p1 = (Arg p2) + ((2 * PI) * i) holds
p1 = p2
proof end;

set CM = CircleMap ;

theorem Th36: :: BORSUK_7:46
for r being Real
for p being Point of (TOP-REAL 2) st p = CircleMap . r holds
Arg p = (2 * PI) * (frac r)
proof end;

theorem Th37: :: BORSUK_7:47
for p1, p2 being Point of (TOP-REAL 3)
for u1, u2 being Point of (Euclid 3) st u1 = p1 & u2 = p2 holds
(Pitag_dist 3) . (u1,u2) = sqrt (((((p1 `1) - (p2 `1)) ^2) + (((p1 `2) - (p2 `2)) ^2)) + (((p1 `3) - (p2 `3)) ^2))
proof end;

theorem Th38: :: BORSUK_7:48
for r being Real
for p being Point of (TOP-REAL 3)
for e being Point of (Euclid 3) st p = e & p `3 = 0 holds
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 end;

theorem Th39: :: BORSUK_7:49
for i being Integer
for c being Complex
for s being Real holds Rotate (c,s) = Rotate (c,(s + ((2 * PI) * i)))
proof end;

theorem :: BORSUK_7:50
for i being Integer
for s being Real holds Rotate s = Rotate (s + ((2 * PI) * i))
proof end;

theorem Th41: :: BORSUK_7:51
for s being Real
for p being Point of (TOP-REAL 2) holds |.((Rotate s) . p).| = |.p.|
proof end;

theorem Th42: :: BORSUK_7:52
for s being Real
for p being Point of (TOP-REAL 2) holds Arg ((Rotate s) . p) = Arg (Rotate ((euc2cpx p),s))
proof end;

theorem Th43: :: BORSUK_7:53
for s being Real
for p being Point of (TOP-REAL 2) st p <> 0. (TOP-REAL 2) holds
ex i being Integer st Arg ((Rotate s) . p) = (s + (Arg p)) + ((2 * PI) * i)
proof end;

theorem Th44: :: BORSUK_7:54
for s being Real holds (Rotate s) . (0. (TOP-REAL 2)) = 0. (TOP-REAL 2)
proof end;

theorem Th45: :: BORSUK_7:55
for s being Real
for p being Point of (TOP-REAL 2) st (Rotate s) . p = 0. (TOP-REAL 2) holds
p = 0. (TOP-REAL 2)
proof end;

theorem Th46: :: BORSUK_7:56
for s being Real
for p being Point of (TOP-REAL 2) holds (Rotate s) . ((Rotate (- s)) . p) = p
proof end;

theorem :: BORSUK_7:57
for s being Real holds (Rotate s) * (Rotate (- s)) = id (TOP-REAL 2)
proof end;

theorem Th48: :: BORSUK_7:58
for r, s being Real
for 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 end;

theorem Th49: :: BORSUK_7:59
for r being non negative Real
for s being Real holds (Rotate s) .: (Sphere ((0. (TOP-REAL 2)),r)) = Sphere ((0. (TOP-REAL 2)),r)
proof 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 :: BORSUK_7:def 4
(Rotate s) | (Tcircle ((0. (TOP-REAL 2)),r));
coherence
(Rotate s) | (Tcircle ((0. (TOP-REAL 2)),r)) is Function of (Tcircle ((0. (TOP-REAL 2)),r)),(Tcircle ((0. (TOP-REAL 2)),r))
proof end;
end;

:: deftheorem defines RotateCircle BORSUK_7:def 4 :
for r being non negative Real
for s being Real holds RotateCircle (r,s) = (Rotate s) | (Tcircle ((0. (TOP-REAL 2)),r));

registration
let r be non negative Real;
let s be Real;
cluster RotateCircle (r,s) -> being_homeomorphism ;
coherence
RotateCircle (r,s) is being_homeomorphism
proof end;
end;

theorem Th50: :: BORSUK_7:60
for r1, r2 being Real
for p being Point of (TOP-REAL 2) st p = CircleMap . r2 holds
(RotateCircle (1,(- (Arg p)))) . (CircleMap . r1) = CircleMap . (r1 - r2)
proof end;

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: :: BORSUK_7:def 5
for a being Point of (Tunit_circle n)
for b being Point of (TOP-REAL n) st a = b holds
it . a = (r * b) + p;
existence
ex b1 being Function of (Tunit_circle n),(Tcircle (p,r)) st
for a being Point of (Tunit_circle n)
for b being Point of (TOP-REAL n) st a = b holds
b1 . a = (r * b) + p
proof end;
uniqueness
for b1, b2 being Function of (Tunit_circle n),(Tcircle (p,r)) st ( for a being Point of (Tunit_circle n)
for b being Point of (TOP-REAL n) st a = b holds
b1 . a = (r * b) + p ) & ( for a being Point of (Tunit_circle n)
for b being Point of (TOP-REAL n) st a = b holds
b2 . a = (r * b) + p ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines CircleIso BORSUK_7:def 5 :
for n being non zero Nat
for p being Point of (TOP-REAL n)
for r being non negative Real
for b4 being Function of (Tunit_circle n),(Tcircle (p,r)) holds
( b4 = CircleIso (p,r) iff for a being Point of (Tunit_circle n)
for b being Point of (TOP-REAL n) st a = b holds
b4 . a = (r * b) + p );

registration
let n be non zero Nat;
let p be Point of (TOP-REAL n);
let r be positive Real;
cluster CircleIso (p,r) -> being_homeomorphism ;
coherence
CircleIso (p,r) is being_homeomorphism
proof end;
end;

definition
func SphereMap -> Function of R^1,(Tunit_circle 3) means :Def6: :: BORSUK_7:def 6
for x being Real holds it . x = |[(cos ((2 * PI) * x)),(sin ((2 * PI) * x)),0]|;
existence
ex b1 being Function of R^1,(Tunit_circle 3) st
for x being Real holds b1 . x = |[(cos ((2 * PI) * x)),(sin ((2 * PI) * x)),0]|
proof end;
uniqueness
for b1, b2 being Function of R^1,(Tunit_circle 3) st ( for x being Real holds b1 . x = |[(cos ((2 * PI) * x)),(sin ((2 * PI) * x)),0]| ) & ( for x being Real holds b2 . x = |[(cos ((2 * PI) * x)),(sin ((2 * PI) * x)),0]| ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines SphereMap BORSUK_7:def 6 :
for b1 being Function of R^1,(Tunit_circle 3) holds
( b1 = SphereMap iff for x being Real holds b1 . x = |[(cos ((2 * PI) * x)),(sin ((2 * PI) * x)),0]| );

set SM = SphereMap ;

theorem :: BORSUK_7:61
for i being Integer holds SphereMap . i = c[100]
proof end;

Lm10: sin is Function of R^1,R^1
proof end;

Lm11: cos is Function of R^1,R^1
proof end;

Lm12: for r being Real holds SphereMap . r = |[((cos * (AffineMap ((2 * PI),Q))) . r),((sin * (AffineMap ((2 * PI),0))) . r),0]|
proof end;

registration
cluster SphereMap -> continuous ;
coherence
SphereMap is continuous
proof end;
end;

definition
let r be Real;
func eLoop r -> Function of I[01],(Tunit_circle 3) means :Def7: :: BORSUK_7:def 7
for x being Point of I[01] holds it . x = |[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x)),0]|;
existence
ex b1 being Function of I[01],(Tunit_circle 3) st
for x being Point of I[01] holds b1 . x = |[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x)),0]|
proof end;
uniqueness
for b1, b2 being Function of I[01],(Tunit_circle 3) st ( for x being Point of I[01] holds b1 . x = |[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x)),0]| ) & ( for x being Point of I[01] holds b2 . x = |[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x)),0]| ) holds
b1 = b2
proof end;
end;

:: deftheorem Def7 defines eLoop BORSUK_7:def 7 :
for r being Real
for b2 being Function of I[01],(Tunit_circle 3) holds
( b2 = eLoop r iff for x being Point of I[01] holds b2 . x = |[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x)),0]| );

theorem Th52: :: BORSUK_7:62
for r being Real holds eLoop r = SphereMap * (ExtendInt r)
proof end;

definition
let i be Integer;
:: original: eLoop
redefine func eLoop i -> Loop of c[100] ;
coherence
eLoop i is Loop of c[100]
proof end;
end;

registration
let i be Integer;
cluster eLoop i -> nullhomotopic for Loop of c[100] ;
coherence
for b1 being Loop of c[100] st b1 = eLoop i holds
b1 is nullhomotopic
proof end;
end;

theorem Th53: :: BORSUK_7:63
for n being Nat
for p being Point of (TOP-REAL n) st p <> 0. (TOP-REAL n) holds
|.(p (/) |.p.|).| = 1
proof 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: :: BORSUK_7:def 8
p (/) |.p.|;
coherence
p (/) |.p.| is Point of (Tcircle ((0. (TOP-REAL n)),1))
proof end;
end;

:: deftheorem Def8 defines Rn->S1 BORSUK_7:def 8 :
for n being Nat
for p being Point of (TOP-REAL n) st p <> 0. (TOP-REAL n) holds
Rn->S1 p = p (/) |.p.|;

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: :: BORSUK_7:def 9
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
ex b1 being Function of (Tunit_circle (n + 1)),(Tunit_circle n) st
for x, y being Point of (Tcircle ((0. (TOP-REAL (n + 1))),1)) st y = - x holds
b1 . x = Rn->S1 ((f . x) - (f . y))
proof end;
uniqueness
for b1, b2 being Function of (Tunit_circle (n + 1)),(Tunit_circle n) st ( for x, y being Point of (Tcircle ((0. (TOP-REAL (n + 1))),1)) st y = - x holds
b1 . x = Rn->S1 ((f . x) - (f . y)) ) & ( for x, y being Point of (Tcircle ((0. (TOP-REAL (n + 1))),1)) st y = - x holds
b2 . x = Rn->S1 ((f . x) - (f . y)) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def9 defines Sn1->Sn BORSUK_7:def 9 :
for n being non zero Nat
for f being Function of (Tcircle ((0. (TOP-REAL (n + 1))),1)),(TOP-REAL n)
for b3 being Function of (Tunit_circle (n + 1)),(Tunit_circle n) holds
( b3 = Sn1->Sn f iff for x, y being Point of (Tcircle ((0. (TOP-REAL (n + 1))),1)) st y = - x holds
b3 . x = Rn->S1 ((f . x) - (f . y)) );

definition
let x0, y0 be Point of (Tunit_circle 2);
let xt be set ;
let f be Path of x0,y0;
assume A1: xt in CircleMap " {x0} ;
func liftPath (f,xt) -> Function of I[01],R^1 means :Def10: :: BORSUK_7:def 10
( 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
ex b1 being Function of I[01],R^1 st
( b1 . 0 = xt & f = CircleMap * b1 & b1 is continuous & ( for f1 being Function of I[01],R^1 st f1 is continuous & f = CircleMap * f1 & f1 . 0 = xt holds
b1 = f1 ) )
by A1, TOPALG_5:23;
uniqueness
for b1, b2 being Function of I[01],R^1 st b1 . 0 = xt & f = CircleMap * b1 & b1 is continuous & ( for f1 being Function of I[01],R^1 st f1 is continuous & f = CircleMap * f1 & f1 . 0 = xt holds
b1 = f1 ) & b2 . 0 = xt & f = CircleMap * b2 & b2 is continuous & ( for f1 being Function of I[01],R^1 st f1 is continuous & f = CircleMap * f1 & f1 . 0 = xt holds
b2 = f1 ) holds
b1 = b2
;
end;

:: deftheorem Def10 defines liftPath BORSUK_7:def 10 :
for x0, y0 being Point of (Tunit_circle 2)
for xt being set
for f being Path of x0,y0 st xt in CircleMap " {x0} holds
for b5 being Function of I[01],R^1 holds
( b5 = liftPath (f,xt) iff ( b5 . 0 = xt & f = CircleMap * b5 & b5 is continuous & ( for f1 being Function of I[01],R^1 st f1 is continuous & f = CircleMap * f1 & f1 . 0 = xt holds
b5 = f1 ) ) );

definition
let n be Nat;
let p, x, y be Point of (TOP-REAL n);
let r be Real;
pred x,y are_antipodals_of p,r means :: BORSUK_7:def 11
( x is Point of (Tcircle (p,r)) & y is Point of (Tcircle (p,r)) & p in LSeg (x,y) );
end;

:: deftheorem defines are_antipodals_of BORSUK_7:def 11 :
for n being Nat
for p, x, y being Point of (TOP-REAL n)
for r being Real holds
( x,y are_antipodals_of p,r iff ( x is Point of (Tcircle (p,r)) & y is Point of (Tcircle (p,r)) & p in LSeg (x,y) ) );

definition
let n be Nat;
let p, x, y be Point of (TOP-REAL n);
let r be Real;
let f be Function;
pred x,y are_antipodals_of p,r,f means :: BORSUK_7:def 12
( x,y are_antipodals_of p,r & x in dom f & y in dom f & f . x = f . y );
end;

:: deftheorem defines are_antipodals_of BORSUK_7:def 12 :
for n being Nat
for p, x, y being Point of (TOP-REAL n)
for r being Real
for f being Function holds
( x,y are_antipodals_of p,r,f iff ( x,y are_antipodals_of p,r & x in dom f & y in dom f & f . x = f . y ) );

definition
let m, n be Nat;
let p be Point of (TOP-REAL m);
let r be Real;
let f be Function of (Tcircle (p,r)),(TOP-REAL n);
attr f is with_antipodals means :: BORSUK_7:def 13
ex x, y being Point of (TOP-REAL m) st x,y are_antipodals_of p,r,f;
end;

:: deftheorem defines with_antipodals BORSUK_7:def 13 :
for m, n being Nat
for p being Point of (TOP-REAL m)
for r being Real
for f being Function of (Tcircle (p,r)),(TOP-REAL n) holds
( f is with_antipodals iff ex x, y being Point of (TOP-REAL m) st x,y are_antipodals_of p,r,f );

notation
let m, n be Nat;
let p be Point of (TOP-REAL m);
let r be Real;
let f be Function of (Tcircle (p,r)),(TOP-REAL n);
antonym without_antipodals f for with_antipodals ;
end;

theorem Th54: :: BORSUK_7:64
for n being non zero Nat
for r being non negative Real
for 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 end;

theorem Th55: :: BORSUK_7:65
for n being non zero Nat
for p, x, y, x1, y1 being Point of (TOP-REAL n)
for 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 end;

theorem Th56: :: BORSUK_7:66
for n being non zero Nat
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 end;

theorem Th57: :: BORSUK_7:67
for n being non zero Nat
for f being Function of (Tcircle ((0. (TOP-REAL (n + 1))),1)),(TOP-REAL n) st f is without_antipodals holds
Sn1->Sn f is odd
proof end;

theorem Th58: :: BORSUK_7:68
for n being non zero Nat
for f, 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 end;

Lm13: for n being non zero Nat
for f being Function of (Tcircle ((0. (TOP-REAL (n + 1))),1)),(TOP-REAL n) st f is without_antipodals & f is continuous holds
Sn1->Sn f is continuous

proof end;

deffunc H1( Function of (Tcircle ((0. (TOP-REAL (2 + 1))),1)),(TOP-REAL 2)) -> Element of bool [: the carrier of I[01], the carrier of (Tunit_circle 2):] = (Sn1->Sn $1) * (eLoop 1);

Lm14: for s being Real
for f being Function of (Tcircle ((0. (TOP-REAL (2 + 1))),1)),(TOP-REAL 2) st f is without_antipodals & 0 <= s & s <= 1 / 2 holds
H1(f) . (s + (1 / 2)) = - (H1(f) . s)

proof end;

defpred S1[ Point of R^1, Point of R^1, Integer] means $1 = $2 + ($3 / 2);

Lm15: now :: thesis: for a, b being Point of R^1 st CircleMap . a = - (CircleMap . b) holds
ex I being odd Integer st S1[a,b,I]
let a, b be Point of R^1; :: thesis: ( CircleMap . a = - (CircleMap . b) implies ex I being odd Integer st S1[a,b,I] )
assume A1: CircleMap . a = - (CircleMap . b) ; :: thesis: ex I being odd Integer st S1[a,b,I]
thus ex I being odd Integer st S1[a,b,I] :: thesis: verum
proof
A2: ( CircleMap . a = |[(cos ((2 * PI) * a)),(sin ((2 * PI) * a))]| & CircleMap . 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 being Integer 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; :: thesis: S1[a,b,I]
thus S1[a,b,I] by A6; :: thesis: verum
end;
end;

Lm16: for f being Function of (Tcircle ((0. (TOP-REAL (2 + 1))),1)),(TOP-REAL 2) st f is without_antipodals & f is continuous holds
H1(f) is nullhomotopic Loop of (Sn1->Sn f) . c100a

proof end;

Lm17: now :: thesis: for f being Function of (Tcircle ((0. (TOP-REAL (2 + 1))),1)),(TOP-REAL 2)
for s being Real
for xt being set st f is without_antipodals & f is continuous & xt in CircleMap " {((Sn1->Sn f) . c[100])} & 0 <= s & s <= 1 / 2 holds
ex IT being odd Integer st
for L being Loop of (Sn1->Sn f) . c100a st L = H1(f) holds
(liftPath (L,xt)) . (s + (1 / 2)) = ((liftPath (L,xt)) . s) + (IT / 2)
let f be Function of (Tcircle ((0. (TOP-REAL (2 + 1))),1)),(TOP-REAL 2); :: thesis: for s being Real
for xt being set st f is without_antipodals & f is continuous & xt in CircleMap " {((Sn1->Sn f) . c[100])} & 0 <= s & s <= 1 / 2 holds
ex IT being odd Integer st
for L being Loop of (Sn1->Sn f) . c100a st L = H1(f) holds
(liftPath (L,xt)) . (s + (1 / 2)) = ((liftPath (L,xt)) . s) + (IT / 2)

let s be Real; :: thesis: for xt being set st f is without_antipodals & f is continuous & xt in CircleMap " {((Sn1->Sn f) . c[100])} & 0 <= s & s <= 1 / 2 holds
ex IT being odd Integer st
for L being Loop of (Sn1->Sn f) . c100a st L = H1(f) holds
(liftPath (L,xt)) . (s + (1 / 2)) = ((liftPath (L,xt)) . s) + (IT / 2)

let xt be set ; :: thesis: ( f is without_antipodals & f is continuous & xt in CircleMap " {((Sn1->Sn f) . c[100])} & 0 <= s & s <= 1 / 2 implies ex IT being odd Integer st
for L being Loop of (Sn1->Sn f) . c100a st L = H1(f) holds
(liftPath (L,xt)) . (s + (1 / 2)) = ((liftPath (L,xt)) . s) + (IT / 2) )

assume that
A1: ( f is without_antipodals & f is continuous ) and
A2: xt in CircleMap " {((Sn1->Sn f) . c[100])} and
A3: ( 0 <= s & s <= 1 / 2 ) ; :: thesis: ex IT being odd Integer st
for L being Loop of (Sn1->Sn f) . c100a st L = H1(f) holds
(liftPath (L,xt)) . (s + (1 / 2)) = ((liftPath (L,xt)) . s) + (IT / 2)

thus ex IT being odd Integer st
for L being Loop of (Sn1->Sn f) . c100a st L = H1(f) holds
(liftPath (L,xt)) . (s + (1 / 2)) = ((liftPath (L,xt)) . s) + (IT / 2) :: thesis: verum
proof
reconsider s = s as Point of I[01] by A3, Lm3;
reconsider L = H1(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 = R^1 (s + (1 / 2)) as Point of I[01] by A3, Lm4;
A4: H1(f) = CircleMap * (liftPath (L,xt)) by A2, Def10;
( (CircleMap * (liftPath (L,xt))) . t1 = CircleMap . ((liftPath (L,xt)) . t1) & (CircleMap * (liftPath (L,xt))) . s = CircleMap . ((liftPath (L,xt)) . s) ) by FUNCT_2:15;
then CircleMap . ((liftPath (L,xt)) . (R^1 (s + (1 / 2)))) = - (CircleMap . ((liftPath (L,xt)) . s)) by A4, A3, A1, Lm14;
then consider I being odd Integer such that
A5: S1[(liftPath (L,xt)) . t1,(liftPath (L,xt)) . s,I] by Lm15;
take I ; :: thesis: for L being Loop of (Sn1->Sn f) . c100a st L = H1(f) holds
(liftPath (L,xt)) . (s + (1 / 2)) = ((liftPath (L,xt)) . s) + (I / 2)

thus for L being Loop of (Sn1->Sn f) . c100a st L = H1(f) holds
(liftPath (L,xt)) . (s + (1 / 2)) = ((liftPath (L,xt)) . s) + (I / 2) by A5; :: thesis: verum
end;
end;

defpred S2[ 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 = H1($1) holds
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 :: thesis: for f being Function of (Tcircle ((0. (TOP-REAL (2 + 1))),1)),(TOP-REAL 2)
for xt being set st f is without_antipodals & f is continuous & xt in CircleMap " {((Sn1->Sn f) . c[100])} holds
ex I being odd Integer st S2[f,xt,I]
let f be Function of (Tcircle ((0. (TOP-REAL (2 + 1))),1)),(TOP-REAL 2); :: thesis: for xt being set st f is without_antipodals & f is continuous & xt in CircleMap " {((Sn1->Sn f) . c[100])} holds
ex I being odd Integer st S2[f,xt,I]

let xt be set ; :: thesis: ( f is without_antipodals & f is continuous & xt in CircleMap " {((Sn1->Sn f) . c[100])} implies ex I being odd Integer st S2[f,xt,I] )
assume that
A1: ( f is without_antipodals & f is continuous ) and
A2: xt in CircleMap " {((Sn1->Sn f) . c[100])} ; :: thesis: ex I being odd Integer st S2[f,xt,I]
reconsider L1 = H1(f) as Loop of (Sn1->Sn f) . c100a by A1, Lm16;
thus ex I being odd Integer st S2[f,xt,I] :: thesis: verum
proof
set l1 = liftPath (L1,xt);
set S = [.0,(1 / 2).];
set AF = AffineMap (1,(1 / 2));
set W = 2 (#) (((liftPath (L1,xt)) * ((AffineMap (1,(1 / 2))) | [.0,(1 / 2).])) - (liftPath (L1,xt)));
dom (AffineMap (1,(1 / 2))) = REAL by FUNCT_2:def 1;
then A3: dom ((AffineMap (1,(1 / 2))) | [.0,(1 / 2).]) = [.0,(1 / 2).] by RELAT_1:62;
A4: dom (liftPath (L1,xt)) = the carrier of I[01] by FUNCT_2:def 1;
A5: rng ((AffineMap (1,(1 / 2))) | [.0,(1 / 2).]) c= the carrier of I[01]
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng ((AffineMap (1,(1 / 2))) | [.0,(1 / 2).]) or y in the carrier of I[01] )
assume y in rng ((AffineMap (1,(1 / 2))) | [.0,(1 / 2).]) ; :: thesis: y in the carrier of I[01]
then consider x being object such that
A6: x in dom ((AffineMap (1,(1 / 2))) | [.0,(1 / 2).]) and
A7: ((AffineMap (1,(1 / 2))) | [.0,(1 / 2).]) . x = y by FUNCT_1:def 3;
reconsider x = x as Real by A6;
A8: ((AffineMap (1,(1 / 2))) | [.0,(1 / 2).]) . x = (AffineMap (1,(1 / 2))) . 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 y in the carrier of I[01] by A7, A8, BORSUK_1:43; :: thesis: verum
end;
A9: dom (((liftPath (L1,xt)) * ((AffineMap (1,(1 / 2))) | [.0,(1 / 2).])) - (liftPath (L1,xt))) = (dom ((liftPath (L1,xt)) * ((AffineMap (1,(1 / 2))) | [.0,(1 / 2).]))) /\ (dom (liftPath (L1,xt))) by VALUED_1:12
.= (dom ((AffineMap (1,(1 / 2))) | [.0,(1 / 2).])) /\ (dom (liftPath (L1,xt))) by A4, A5, RELAT_1:27
.= [.0,(1 / 2).] by A3, A4, BORSUK_1:40, XBOOLE_1:28, XXREAL_1:34 ;
A10: dom (2 (#) (((liftPath (L1,xt)) * ((AffineMap (1,(1 / 2))) | [.0,(1 / 2).])) - (liftPath (L1,xt)))) = dom (((liftPath (L1,xt)) * ((AffineMap (1,(1 / 2))) | [.0,(1 / 2).])) - (liftPath (L1,xt))) by VALUED_1:def 5;
rng (2 (#) (((liftPath (L1,xt)) * ((AffineMap (1,(1 / 2))) | [.0,(1 / 2).])) - (liftPath (L1,xt)))) c= REAL by VALUED_0:def 3;
then reconsider W = 2 (#) (((liftPath (L1,xt)) * ((AffineMap (1,(1 / 2))) | [.0,(1 / 2).])) - (liftPath (L1,xt))) 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 = H1(f) holds
(liftPath (L,xt)) . (j0 + (1 / 2)) = ((liftPath (L,xt)) . j0) + (ITj0 / 2) by A1, A2, Lm17;
take ITj0 ; :: thesis: S2[f,xt,ITj0]
let L be Loop of (Sn1->Sn f) . c100a; :: thesis: ( L = H1(f) implies for s being Real st 0 <= s & s <= 1 / 2 holds
(liftPath (L,xt)) . (s + (1 / 2)) = ((liftPath (L,xt)) . s) + (ITj0 / 2) )

assume A12: L = H1(f) ; :: thesis: for s being Real st 0 <= s & s <= 1 / 2 holds
(liftPath (L,xt)) . (s + (1 / 2)) = ((liftPath (L,xt)) . s) + (ITj0 / 2)

let s be Real; :: thesis: ( 0 <= s & s <= 1 / 2 implies (liftPath (L,xt)) . (s + (1 / 2)) = ((liftPath (L,xt)) . s) + (ITj0 / 2) )
assume A13: ( 0 <= s & s <= 1 / 2 ) ; :: thesis: (liftPath (L,xt)) . (s + (1 / 2)) = ((liftPath (L,xt)) . s) + (ITj0 / 2)
set l = liftPath (L,xt);
A14: s in [.0,(1 / 2).] by A13, XXREAL_1:1;
A15: 0 in [.0,(1 / 2).] by XXREAL_1:1;
then A16: ((AffineMap (1,(1 / 2))) | [.0,(1 / 2).]) . 0 = (AffineMap (1,(1 / 2))) . 0 by FUNCT_1:49
.= (1 * Q) + (1 / 2) by FCONT_1:def 4 ;
A17: ((AffineMap (1,(1 / 2))) | [.0,(1 / 2).]) . s = (AffineMap (1,(1 / 2))) . 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 = H1(f) holds
(liftPath (L,xt)) . (s + (1 / 2)) = ((liftPath (L,xt)) . s) + (ITs / 2) by A1, A2, A13, Lm17;
A19: (liftPath (L1,xt)) . (j0 + (1 / 2)) = ((liftPath (L1,xt)) . j0) + (ITj0 / 2) by A11;
A20: (liftPath (L1,xt)) . (s + (1 / 2)) = ((liftPath (L1,xt)) . s) + (ITs / 2) by A18;
A21: W . 0 = 2 * ((((liftPath (L1,xt)) * ((AffineMap (1,(1 / 2))) | [.0,(1 / 2).])) - (liftPath (L1,xt))) . 0) by VALUED_1:6
.= 2 * ((((liftPath (L1,xt)) * ((AffineMap (1,(1 / 2))) | [.0,(1 / 2).])) . 0) - ((liftPath (L1,xt)) . 0)) by A9, A15, VALUED_1:13
.= 2 * (((liftPath (L1,xt)) . (1 / 2)) - ((liftPath (L1,xt)) . 0)) by A16, A3, A15, FUNCT_1:13
.= 2 * (ITj0 / 2) by A19 ;
A22: W . s = 2 * ((((liftPath (L1,xt)) * ((AffineMap (1,(1 / 2))) | [.0,(1 / 2).])) - (liftPath (L1,xt))) . s) by VALUED_1:6
.= 2 * ((((liftPath (L1,xt)) * ((AffineMap (1,(1 / 2))) | [.0,(1 / 2).])) . s) - ((liftPath (L1,xt)) . s)) by A9, A14, VALUED_1:13
.= 2 * (((liftPath (L1,xt)) . (s + (1 / 2))) - ((liftPath (L1,xt)) . s)) by A17, A3, A14, FUNCT_1:13
.= 2 * (ITs / 2) by A20 ;
A23: rng W c= INT
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng W or y in INT )
assume y in rng W ; :: thesis: y in INT
then consider s being object such that
A24: s in dom W and
A25: W . s = y by FUNCT_1:def 3;
reconsider s = s as Real by A24;
A26: ((AffineMap (1,(1 / 2))) | [.0,(1 / 2).]) . s = (AffineMap (1,(1 / 2))) . 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 = H1(f) holds
(liftPath (L,xt)) . (s + (1 / 2)) = ((liftPath (L,xt)) . s) + (ITs / 2) by A1, A2, Lm17;
A28: (liftPath (L1,xt)) . (s + (1 / 2)) = ((liftPath (L1,xt)) . s) + (ITs / 2) by A27;
W . s = 2 * ((((liftPath (L1,xt)) * ((AffineMap (1,(1 / 2))) | [.0,(1 / 2).])) - (liftPath (L1,xt))) . s) by VALUED_1:6
.= 2 * ((((liftPath (L1,xt)) * ((AffineMap (1,(1 / 2))) | [.0,(1 / 2).])) . s) - ((liftPath (L1,xt)) . s)) by A10, A24, VALUED_1:13
.= 2 * (((liftPath (L1,xt)) . (s + (1 / 2))) - ((liftPath (L1,xt)) . s)) by A26, A3, A9, A10, A24, FUNCT_1:13
.= 2 * (ITs / 2) by A28 ;
hence y in INT by A25, INT_1:def 2; :: thesis: verum
end;
set T = Closed-Interval-TSpace (0,(1 / 2));
A29: the carrier of (Closed-Interval-TSpace (0,(1 / 2))) = [.0,(1 / 2).] 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 (Closed-Interval-TSpace (0,(1 / 2))),(R^1 | SR) by A10, A9, Lm8, A29, A23, FUNCT_2:2, NUMBERS:14, XBOOLE_1:1;
A31: Closed-Interval-TSpace (0,(1 / 2)) is connected by TREAL_1:20;
A32: R^1 | (R^1 (dom W)) = Closed-Interval-TSpace (0,(1 / 2)) by A10, A9, A29, PRE_TOPC:8, TSEP_1:5;
reconsider f1 = R^1 ((AffineMap (1,(1 / 2))) | [.0,(1 / 2).]) as Function of (Closed-Interval-TSpace (0,(1 / 2))),I[01] by A5, A3, A29, FUNCT_2:2;
rng (liftPath (L1,xt)) c= REAL by TOPMETR:17;
then reconsider ll1 = liftPath (L1,xt) as PartFunc of REAL,REAL by A4, BORSUK_1:40, RELSET_1:4;
liftPath (L1,xt) is continuous by A2, Def10;
then A33: ll1 is continuous by Th29, TOPMETR:20;
(ll1 * ((AffineMap (1,(1 / 2))) | [.0,(1 / 2).])) - ll1 is continuous by A33;
then reconsider W = 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 R^1 | (R^1 QQ) 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 (liftPath (L,xt)) . (s + (1 / 2)) = ((liftPath (L,xt)) . s) + (ITj0 / 2) by A20, A12, A21, A22, A9, A10, A15, A14; :: thesis: verum
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 = H1(f) holds
for I being Integer st S2[f,xt,I] holds
(liftPath (L,xt)) . 1 = ((liftPath (L,xt)) . 0) + I

proof end;

Lm20: for f being Function of (Tcircle ((0. (TOP-REAL (2 + 1))),1)),(TOP-REAL 2) st f is without_antipodals & f is continuous holds
not H1(f) is nullhomotopic Loop of (Sn1->Sn f) . c100a

proof end;

Lm21: for f being continuous Function of (Tcircle ((0. (TOP-REAL (2 + 1))),1)),(TOP-REAL 2) holds f is with_antipodals
proof end;

registration
let n be non zero Nat;
let r be negative Real;
let p be Point of (TOP-REAL (n + 1));
cluster Function-like quasi_total -> without_antipodals for Element of bool [: the carrier of (Tcircle (p,r)), the carrier of (TOP-REAL n):];
coherence
for b1 being Function of (Tcircle (p,r)),(TOP-REAL n) holds b1 is without_antipodals
proof end;
end;

:: WP: Borsuk-Ulam Theorem
registration
let r be non negative Real;
let p be Point of (TOP-REAL 3);
cluster Function-like quasi_total continuous -> with_antipodals for Element of bool [: the carrier of (Tcircle (p,r)), the carrier of (TOP-REAL 2):];
coherence
for b1 being Function of (Tcircle (p,r)),(TOP-REAL 2) st b1 is continuous holds
b1 is with_antipodals
proof end;
end;