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[ object , object ] means $2 = P . ($1 `1);
A1:
for x being object st x in [: the carrier of I[01], the carrier of I[01]:] holds
ex y being object 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 object 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 2;
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:87;
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:87;
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;
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 2;
then reconsider W1 =
W `1 as
Point of
I[01] by MCART_1:10;
A9:
ex
x,
y being
object 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:15;
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
;
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:95;
then reconsider HH =
[:H, the carrier of I[01]:] as
Subset of
[:I[01],I[01]:] by BORSUK_1:def 2;
(
W1 in Int H &
Int HH = [:(Int H),(Int AI):] )
by BORSUK_1:7, CONNSP_2:def 1;
then
W in Int HH
by A9, A10, ZFMISC_1:def 2;
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:87;
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:87;
then
S1[
s0,
f . s0]
by A2;
hence
(
f . (
s,
0)
= P . s &
f . (
s,1)
= P . s )
by A16;
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; verum