let T be non empty TopSpace; for a, b being Point of T
for P being Path of a,b st a,b are_connected holds
P,P are_homotopic
let a, b be Point of T; for P being Path of a,b st a,b are_connected holds
P,P are_homotopic
let P be Path of a,b; ( a,b are_connected implies P,P are_homotopic )
defpred S1[ set , set ] means $2 = P . ($1 `1 );
A1:
for x being set st x in [:the carrier of I[01] ,the carrier of I[01] :] holds
ex y being set st
( y in the carrier of T & S1[x,y] )
consider f being Function of [:the carrier of I[01] ,the carrier of I[01] :],the carrier of T such that
A2:
for x being set st x in [:the carrier of I[01] ,the carrier of I[01] :] holds
S1[x,f . x]
from FUNCT_2:sch 1(A1);
the carrier of [:I[01] ,I[01] :] = [:the carrier of I[01] ,the carrier of I[01] :]
by BORSUK_1:def 5;
then reconsider f = f as Function of the carrier of [:I[01] ,I[01] :],the carrier of T ;
reconsider f = f as Function of [:I[01] ,I[01] :],T ;
assume A3:
a,b are_connected
; P,P are_homotopic
A4:
for t being Point of I[01] holds
( f . 0 ,t = a & f . 1,t = b )
proof
let t be
Point of
I[01] ;
( f . 0 ,t = a & f . 1,t = b )
set t0 =
[0 ,t];
set t1 =
[1,t];
0 in the
carrier of
I[01]
by Lm1;
then
[0 ,t] in [:the carrier of I[01] ,the carrier of I[01] :]
by ZFMISC_1:106;
then A5:
f . [0 ,t] = P . ([0 ,t] `1 )
by A2;
1
in the
carrier of
I[01]
by Lm1;
then
[1,t] in [:the carrier of I[01] ,the carrier of I[01] :]
by ZFMISC_1:106;
then A6:
f . [1,t] = P . ([1,t] `1 )
by A2;
(
P . 0 = a &
P . 1
= b )
by A3, Def2;
hence
(
f . 0 ,
t = a &
f . 1,
t = b )
by A5, A6, MCART_1:7;
verum
end;
A7:
for W being Point of [:I[01] ,I[01] :]
for G being a_neighborhood of f . W ex H being a_neighborhood of W st f .: H c= G
proof
let W be
Point of
[:I[01] ,I[01] :];
for G being a_neighborhood of f . W ex H being a_neighborhood of W st f .: H c= Glet G be
a_neighborhood of
f . W;
ex H being a_neighborhood of W st f .: H c= G
W in the
carrier of
[:I[01] ,I[01] :]
;
then A8:
W in [:the carrier of I[01] ,the carrier of I[01] :]
by BORSUK_1:def 5;
then reconsider W1 =
W `1 as
Point of
I[01] by MCART_1:10;
A9:
ex
x,
y being
set st
[x,y] = W
by A8, RELAT_1:def 1;
reconsider G9 =
G as
a_neighborhood of
P . W1 by A2, A8;
the
carrier of
I[01] c= the
carrier of
I[01]
;
then reconsider AI = the
carrier of
I[01] as
Subset of
I[01] ;
AI = [#] I[01]
;
then
Int AI = the
carrier of
I[01]
by TOPS_1:43;
then A10:
W `2 in Int AI
by A8, MCART_1:10;
P is
continuous
by A3, Def2;
then consider H being
a_neighborhood of
W1 such that A11:
P .: H c= G9
by BORSUK_1:def 3;
set HH =
[:H,the carrier of I[01] :];
[:H,the carrier of I[01] :] c= [:the carrier of I[01] ,the carrier of I[01] :]
by ZFMISC_1:118;
then reconsider HH =
[:H,the carrier of I[01] :] as
Subset of
[:I[01] ,I[01] :] by BORSUK_1:def 5;
(
W1 in Int H &
Int HH = [:(Int H),(Int AI):] )
by BORSUK_1:47, CONNSP_2:def 1;
then
W in Int HH
by A9, A10, MCART_1:11;
then reconsider HH =
HH as
a_neighborhood of
W by CONNSP_2:def 1;
take
HH
;
f .: HH c= G
f .: HH c= G
hence
f .: HH c= G
;
verum
end;
take
f
; BORSUK_2:def 7 ( f is continuous & ( for t being Point of I[01] holds
( f . t,0 = P . t & f . t,1 = P . t & f . 0 ,t = a & f . 1,t = b ) ) )
for s being Point of I[01] holds
( f . s,0 = P . s & f . s,1 = P . s )
proof
let s be
Point of
I[01] ;
( f . s,0 = P . s & f . s,1 = P . s )
reconsider s0 =
[s,0 ],
s1 =
[s,1] as
set ;
1
in the
carrier of
I[01]
by Lm1;
then
s1 in [:the carrier of I[01] ,the carrier of I[01] :]
by ZFMISC_1:106;
then A16:
S1[
s1,
f . s1]
by A2;
0 in the
carrier of
I[01]
by Lm1;
then
s0 in [:the carrier of I[01] ,the carrier of I[01] :]
by ZFMISC_1:106;
then
S1[
s0,
f . s0]
by A2;
hence
(
f . s,
0 = P . s &
f . s,1
= P . s )
by A16, MCART_1:7;
verum
end;
hence
( f is continuous & ( for t being Point of I[01] holds
( f . t,0 = P . t & f . t,1 = P . t & f . 0 ,t = a & f . 1,t = b ) ) )
by A7, A4, BORSUK_1:def 3; verum