begin
Lm1:
for r being real number holds
( ( 0 <= r & r <= 1 ) iff r in the carrier of I[01] )
theorem
theorem
canceled;
theorem
begin
theorem Th4:
:: deftheorem Def1 defines are_connected BORSUK_2:def 1 :
:: deftheorem Def2 defines Path BORSUK_2:def 2 :
:: deftheorem Def3 defines arcwise_connected BORSUK_2:def 3 :
:: deftheorem Def4 defines Path BORSUK_2:def 4 :
Lm2:
( 0 in [.0 ,1.] & 1 in [.0 ,1.] )
theorem Th5:
begin
Lm3:
for G being non empty TopSpace
for w1, w2, w3 being Point of
for h1, h2 being Function of I[01] ,G st h1 is continuous & w1 = h1 . 0 & w2 = h1 . 1 & h2 is continuous & w2 = h2 . 0 & w3 = h2 . 1 holds
ex h3 being Function of I[01] ,G st
( h3 is continuous & w1 = h3 . 0 & w3 = h3 . 1 & rng h3 c= (rng h1) \/ (rng h2) )
definition
let T be non
empty TopSpace;
let a,
b,
c be
Point of ;
let P be
Path of
a,
b;
let Q be
Path of
b,
c;
assume that A1:
a,
b are_connected
and A2:
b,
c are_connected
;
func P + Q -> Path of
a,
c means :
Def5:
for
t being
Point of holds
( (
t <= 1
/ 2 implies
it . t = P . (2 * t) ) & ( 1
/ 2
<= t implies
it . t = Q . ((2 * t) - 1) ) );
existence
ex b1 being Path of a,c st
for t being Point of holds
( ( t <= 1 / 2 implies b1 . t = P . (2 * t) ) & ( 1 / 2 <= t implies b1 . t = Q . ((2 * t) - 1) ) )
uniqueness
for b1, b2 being Path of a,c st ( for t being Point of holds
( ( t <= 1 / 2 implies b1 . t = P . (2 * t) ) & ( 1 / 2 <= t implies b1 . t = Q . ((2 * t) - 1) ) ) ) & ( for t being Point of holds
( ( t <= 1 / 2 implies b2 . t = P . (2 * t) ) & ( 1 / 2 <= t implies b2 . t = Q . ((2 * t) - 1) ) ) ) holds
b1 = b2
end;
:: deftheorem Def5 defines + BORSUK_2:def 5 :
theorem
theorem Th7:
:: deftheorem Def6 defines - BORSUK_2:def 6 :
Lm4:
for r being Real st 0 <= r & r <= 1 holds
( 0 <= 1 - r & 1 - r <= 1 )
Lm5:
for r being Real st r in the carrier of I[01] holds
1 - r in the carrier of I[01]
theorem Th8:
begin
theorem Th9:
definition
let S1,
S2,
T1,
T2 be non
empty TopSpace;
let f be
Function of
S1,
S2;
let g be
Function of
T1,
T2;
[:redefine func [:f,g:] -> Function of
[:S1,T1:],
[:S2,T2:];
coherence
[:f,g:] is Function of [:S1,T1:],[:S2,T2:]
end;
theorem Th10:
theorem Th11:
theorem Th12:
theorem
canceled;
theorem Th14:
Lm6:
for T1, T2 being non empty TopSpace st T1 is T_2 & T2 is T_2 holds
[:T1,T2:] is T_2
definition
let T be non
empty TopStruct ;
let a,
b be
Point of ;
let P,
Q be
Path of
a,
b;
pred P,
Q are_homotopic means
ex
f being
Function of
[:I[01] ,I[01] :],
T st
(
f is
continuous & ( for
t being
Point of holds
(
f . t,
0 = P . t &
f . t,1
= Q . t &
f . 0 ,
t = a &
f . 1,
t = b ) ) );
symmetry
for P, Q being Path of a,b st ex f being Function of [:I[01] ,I[01] :],T st
( f is continuous & ( for t being Point of holds
( f . t,0 = P . t & f . t,1 = Q . t & f . 0 ,t = a & f . 1,t = b ) ) ) holds
ex f being Function of [:I[01] ,I[01] :],T st
( f is continuous & ( for t being Point of holds
( f . t,0 = Q . t & f . t,1 = P . t & f . 0 ,t = a & f . 1,t = b ) ) )
end;
:: deftheorem defines are_homotopic BORSUK_2:def 7 :
for
T being non
empty TopStruct for
a,
b being
Point of
for
P,
Q being
Path of
a,
b holds
(
P,
Q are_homotopic iff ex
f being
Function of
[:I[01] ,I[01] :],
T st
(
f is
continuous & ( for
t being
Point of holds
(
f . t,
0 = P . t &
f . t,1
= Q . t &
f . 0 ,
t = a &
f . 1,
t = b ) ) ) );
theorem Th15:
theorem
theorem
theorem Th18: