:: 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]

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;
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

Lm4: now :: thesis: for s being Real st 0 <= s & s <= 1 / 2 holds

s + (1 / 2) in the carrier of I[01]

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;
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

registration
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 ) )

( 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))/]) )

( 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))/]) )

( 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;

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)

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;
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

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) )

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) )

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)

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

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;

coherence

f + c is one-to-one

end;
let c be Complex;

coherence

f + c is one-to-one

proof end;

registration
end;

::$CT

Lm6: 1,2,3 are_mutually_distinct

;

canceled;

::$CD

::$CT 9

::$CT 9

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))}

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))

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))

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;

:: 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 );

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
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;

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)

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)

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 )

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

end;
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

{ q where q is Element of RAT : ( q in rng f & q > r ) } c= rng f

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 )

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)

Q2 = G2 /\ the carrier of (Image f)

thus Q1 \/ Q2 = [#] (Image f) :: thesis: verum

end;
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

then reconsider Q1 = { q where q is Element of RAT : ( q in rng f & q < r ) } as Subset of (Image f) by WAYBEL18:9;
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;
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

{ q where q is Element of RAT : ( q in rng f & q > r ) } c= rng f

proof

then reconsider Q2 = { q where q is Element of RAT : ( q in rng f & q > r ) } as Subset of (Image f) by WAYBEL18:9;
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;
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

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

( f . x in Q1 & f . y in Q2 )
by A2, A3, Lm8;
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;
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

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

hence
Q1 is open
by TSP_1:def 1; :: thesis: ( Q2 is open & [#] (Image f) = Q1 \/ Q2 )
thus
Q1 c= G1 /\ the carrier of (Image f)
:: according to XBOOLE_0:def 10 :: thesis: G1 /\ the carrier of (Image f) c= 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;
proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in G1 /\ the carrier of (Image f) or x in Q1 )
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;
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

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

Q2 = G2 /\ the carrier of (Image f)

proof

hence
Q2 is open
by TSP_1:def 1; :: thesis: [#] (Image f) = Q1 \/ Q2
thus
Q2 c= G2 /\ the carrier of (Image f)
:: according to XBOOLE_0:def 10 :: thesis: G2 /\ the carrier of (Image f) c= 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;
proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in G2 /\ the carrier of (Image f) or x in Q2 )
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;
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

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

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;
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

registration

let X be non empty connected TopSpace;

let Y be non empty TopSpace;

let f be continuous Function of X,Y;

coherence

Image f is connected

end;
let Y be non empty TopSpace;

let f be continuous Function of X,Y;

coherence

Image f is connected

proof 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

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

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;
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;

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;
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;

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

end;
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;

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

end;
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;

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

redefine func f - r -> Path of s - r,t - r;

coherence

f - r is Path of s - r,t - r

end;
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;

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

reconsider c100a = c[100] as Point of (Tunit_circle (2 + 1)) ;

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

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)) )

( 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

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)

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))

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)

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)))

for c being Complex

for s being Real holds Rotate (c,s) = Rotate (c,(s + ((2 * PI) * i)))

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))

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)

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 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)

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 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) )

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)

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;

(Rotate s) | (Tcircle ((0. (TOP-REAL 2)),r)) is Function of (Tcircle ((0. (TOP-REAL 2)),r)),(Tcircle ((0. (TOP-REAL 2)),r))

end;
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));

(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;

:: 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));

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;

coherence

RotateCircle (r,s) is being_homeomorphism

end;
let s be Real;

coherence

RotateCircle (r,s) is being_homeomorphism

proof 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)

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;

ex b_{1} 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

b_{1} . a = (r * b) + p

for b_{1}, b_{2} 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

b_{1} . a = (r * b) + p ) & ( for a being Point of (Tunit_circle n)

for b being Point of (TOP-REAL n) st a = b holds

b_{2} . a = (r * b) + p ) holds

b_{1} = b_{2}

end;
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 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;

ex b

for a being Point of (Tunit_circle n)

for b being Point of (TOP-REAL n) st a = b holds

b

proof end;

uniqueness for b

for b being Point of (TOP-REAL n) st a = b holds

b

for b being Point of (TOP-REAL n) st a = b holds

b

b

proof 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 b_{4} being Function of (Tunit_circle n),(Tcircle (p,r)) holds

( b_{4} = CircleIso (p,r) iff for a being Point of (Tunit_circle n)

for b being Point of (TOP-REAL n) st a = b holds

b_{4} . a = (r * b) + p );

for n being non zero Nat

for p being Point of (TOP-REAL n)

for r being non negative Real

for b

( b

for b being Point of (TOP-REAL n) st a = b holds

b

registration

let n be non zero Nat;

let p be Point of (TOP-REAL n);

let r be positive Real;

coherence

CircleIso (p,r) is being_homeomorphism

end;
let p be Point of (TOP-REAL n);

let r be positive Real;

coherence

CircleIso (p,r) is being_homeomorphism

proof end;

definition

ex b_{1} being Function of R^1,(Tunit_circle 3) st

for x being Real holds b_{1} . x = |[(cos ((2 * PI) * x)),(sin ((2 * PI) * x)),0]|

for b_{1}, b_{2} being Function of R^1,(Tunit_circle 3) st ( for x being Real holds b_{1} . x = |[(cos ((2 * PI) * x)),(sin ((2 * PI) * x)),0]| ) & ( for x being Real holds b_{2} . x = |[(cos ((2 * PI) * x)),(sin ((2 * PI) * x)),0]| ) holds

b_{1} = b_{2}
end;

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 for x being Real holds it . x = |[(cos ((2 * PI) * x)),(sin ((2 * PI) * x)),0]|;

ex b

for x being Real holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def6 defines SphereMap BORSUK_7:def 6 :

for b_{1} being Function of R^1,(Tunit_circle 3) holds

( b_{1} = SphereMap iff for x being Real holds b_{1} . x = |[(cos ((2 * PI) * x)),(sin ((2 * PI) * x)),0]| );

for b

( b

set SM = SphereMap ;

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;

definition

let r be Real;

ex b_{1} being Function of I[01],(Tunit_circle 3) st

for x being Point of I[01] holds b_{1} . x = |[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x)),0]|

for b_{1}, b_{2} being Function of I[01],(Tunit_circle 3) st ( for x being Point of I[01] holds b_{1} . x = |[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x)),0]| ) & ( for x being Point of I[01] holds b_{2} . x = |[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x)),0]| ) holds

b_{1} = b_{2}

end;
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 for x being Point of I[01] holds it . x = |[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x)),0]|;

ex b

for x being Point of I[01] holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def7 defines eLoop BORSUK_7:def 7 :

for r being Real

for b_{2} being Function of I[01],(Tunit_circle 3) holds

( b_{2} = eLoop r iff for x being Point of I[01] holds b_{2} . x = |[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x)),0]| );

for r being Real

for b

( b

definition

let i be Integer;

:: original: eLoop

redefine func eLoop i -> Loop of c[100] ;

coherence

eLoop i is Loop of c[100]

end;
:: original: eLoop

redefine func eLoop i -> Loop of c[100] ;

coherence

eLoop i is Loop of c[100]

proof end;

registration

let i be Integer;

coherence

for b_{1} being Loop of c[100] st b_{1} = eLoop i holds

b_{1} is nullhomotopic

end;
coherence

for b

b

proof 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

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) ;

p (/) |.p.| is Point of (Tcircle ((0. (TOP-REAL n)),1))

end;
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.|;

p (/) |.p.| is Point of (Tcircle ((0. (TOP-REAL n)),1))

proof 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.|;

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;

ex b_{1} 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

b_{1} . x = Rn->S1 ((f . x) - (f . y))

for b_{1}, b_{2} 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

b_{1} . x = Rn->S1 ((f . x) - (f . y)) ) & ( for x, y being Point of (Tcircle ((0. (TOP-REAL (n + 1))),1)) st y = - x holds

b_{2} . x = Rn->S1 ((f . x) - (f . y)) ) holds

b_{1} = b_{2}

end;
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 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));

ex b

for x, y being Point of (Tcircle ((0. (TOP-REAL (n + 1))),1)) st y = - x holds

b

proof end;

uniqueness for b

b

b

b

proof 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 b_{3} being Function of (Tunit_circle (n + 1)),(Tunit_circle n) holds

( b_{3} = Sn1->Sn f iff for x, y being Point of (Tcircle ((0. (TOP-REAL (n + 1))),1)) st y = - x holds

b_{3} . x = Rn->S1 ((f . x) - (f . y)) );

for n being non zero Nat

for f being Function of (Tcircle ((0. (TOP-REAL (n + 1))),1)),(TOP-REAL n)

for b

( b

b

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} ;

ex b_{1} being Function of I[01],R^1 st

( b_{1} . 0 = xt & f = CircleMap * b_{1} & b_{1} is continuous & ( for f1 being Function of I[01],R^1 st f1 is continuous & f = CircleMap * f1 & f1 . 0 = xt holds

b_{1} = f1 ) )
by A1, TOPALG_5:23;

uniqueness

for b_{1}, b_{2} being Function of I[01],R^1 st b_{1} . 0 = xt & f = CircleMap * b_{1} & b_{1} is continuous & ( for f1 being Function of I[01],R^1 st f1 is continuous & f = CircleMap * f1 & f1 . 0 = xt holds

b_{1} = f1 ) & b_{2} . 0 = xt & f = CircleMap * b_{2} & b_{2} is continuous & ( for f1 being Function of I[01],R^1 st f1 is continuous & f = CircleMap * f1 & f1 . 0 = xt holds

b_{2} = f1 ) holds

b_{1} = b_{2}
;

end;
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 ( 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 ) );

ex b

( b

b

uniqueness

for b

b

b

b

:: 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 b_{5} being Function of I[01],R^1 holds

( b_{5} = liftPath (f,xt) iff ( b_{5} . 0 = xt & f = CircleMap * b_{5} & b_{5} is continuous & ( for f1 being Function of I[01],R^1 st f1 is continuous & f = CircleMap * f1 & f1 . 0 = xt holds

b_{5} = f1 ) ) );

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 b

( b

b

definition

let n be Nat;

let p, x, y be Point of (TOP-REAL n);

let r be Real;

end;
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) );

( x is Point of (Tcircle (p,r)) & y is Point of (Tcircle (p,r)) & p in LSeg (x,y) );

:: 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) ) );

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;

end;
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 );

( x,y are_antipodals_of p,r & x in dom f & y in dom f & f . x = f . y );

:: 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 ) );

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);

end;
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;

ex x, y being Point of (TOP-REAL m) st x,y are_antipodals_of p,r,f;

:: 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 );

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;
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 ;

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

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

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)

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

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)

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 H

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

H

proof end;

defpred S

Lm15: now :: thesis: for a, b being Point of R^1 st CircleMap . a = - (CircleMap . b) holds

ex I being odd Integer st S_{1}[a,b,I]

ex I being odd Integer st S

let a, b be Point of R^1; :: thesis: ( CircleMap . a = - (CircleMap . b) implies ex I being odd Integer st S_{1}[a,b,I] )

assume A1: CircleMap . a = - (CircleMap . b) ; :: thesis: ex I being odd Integer st S_{1}[a,b,I]

thus ex I being odd Integer st S_{1}[a,b,I]
:: thesis: verum

end;
assume A1: CircleMap . a = - (CircleMap . b) ; :: thesis: ex I being odd Integer st S

thus ex I being odd Integer st S

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: S_{1}[a,b,I]

thus S_{1}[a,b,I]
by A6; :: thesis: verum

end;
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: S

thus S

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

H

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 = H_{1}(f) holds

(liftPath (L,xt)) . (s + (1 / 2)) = ((liftPath (L,xt)) . s) + (IT / 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 = H

(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 = H_{1}(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 = H_{1}(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 = H_{1}(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 = H_{1}(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 = H_{1}(f) holds

(liftPath (L,xt)) . (s + (1 / 2)) = ((liftPath (L,xt)) . s) + (IT / 2) :: thesis: verum

end;
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 = H

(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 = H

(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 = H

(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 = H

(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 = H

(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 = H_{1}(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: H_{1}(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: S_{1}[(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 = H_{1}(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 = H_{1}(f) holds

(liftPath (L,xt)) . (s + (1 / 2)) = ((liftPath (L,xt)) . s) + (I / 2) by A5; :: thesis: verum

end;
reconsider L = H

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: H

( (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: S

take I ; :: thesis: for L being Loop of (Sn1->Sn f) . c100a st L = H

(liftPath (L,xt)) . (s + (1 / 2)) = ((liftPath (L,xt)) . s) + (I / 2)

thus for L being Loop of (Sn1->Sn f) . c100a st L = H

(liftPath (L,xt)) . (s + (1 / 2)) = ((liftPath (L,xt)) . s) + (I / 2) by A5; :: thesis: verum

defpred S

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 S_{2}[f,xt,I]

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 S

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 S_{2}[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 S_{2}[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 S_{2}[f,xt,I]

reconsider L1 = H_{1}(f) as Loop of (Sn1->Sn f) . c100a by A1, Lm16;

thus ex I being odd Integer st S_{2}[f,xt,I]
:: thesis: verum

end;
ex I being odd Integer st S

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 S

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 S

reconsider L1 = H

thus ex I being odd Integer st S

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]

.= (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 = H_{1}(f) holds

(liftPath (L,xt)) . (j0 + (1 / 2)) = ((liftPath (L,xt)) . j0) + (ITj0 / 2) by A1, A2, Lm17;

take ITj0 ; :: thesis: S_{2}[f,xt,ITj0]

let L be Loop of (Sn1->Sn f) . c100a; :: thesis: ( L = H_{1}(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 = H_{1}(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 = H_{1}(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

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;
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

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
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;
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

.= (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 = H

(liftPath (L,xt)) . (j0 + (1 / 2)) = ((liftPath (L,xt)) . j0) + (ITj0 / 2) by A1, A2, Lm17;

take ITj0 ; :: thesis: S

let L be Loop of (Sn1->Sn f) . c100a; :: thesis: ( L = H

(liftPath (L,xt)) . (s + (1 / 2)) = ((liftPath (L,xt)) . s) + (ITj0 / 2) )

assume A12: L = H

(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 = H

(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

set T = Closed-Interval-TSpace (0,(1 / 2));
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 = H_{1}(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;
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 = H

(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

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

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 = H

for I being Integer st S

(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 H

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));

for b_{1} being Function of (Tcircle (p,r)),(TOP-REAL n) holds b_{1} is without_antipodals

end;
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 b

proof end;

registration

let r be non negative Real;

let p be Point of (TOP-REAL 3);

for b_{1} being Function of (Tcircle (p,r)),(TOP-REAL 2) st b_{1} is continuous holds

b_{1} is with_antipodals

end;
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 b

b

proof end;