let T be non empty TopStruct ; for c1, c2 being with_endpoints Curve of T
for a, b being Point of T
for p1, p2 being Path of a,b st c1 = p1 & c2 = p2 & a,b are_connected holds
( c1,c2 are_homotopic iff p1,p2 are_homotopic )
let c1, c2 be with_endpoints Curve of T; for a, b being Point of T
for p1, p2 being Path of a,b st c1 = p1 & c2 = p2 & a,b are_connected holds
( c1,c2 are_homotopic iff p1,p2 are_homotopic )
let a, b be Point of T; for p1, p2 being Path of a,b st c1 = p1 & c2 = p2 & a,b are_connected holds
( c1,c2 are_homotopic iff p1,p2 are_homotopic )
let p1, p2 be Path of a,b; ( c1 = p1 & c2 = p2 & a,b are_connected implies ( c1,c2 are_homotopic iff p1,p2 are_homotopic ) )
assume A1:
( c1 = p1 & c2 = p2 )
; ( not a,b are_connected or ( c1,c2 are_homotopic iff p1,p2 are_homotopic ) )
assume A2:
a,b are_connected
; ( c1,c2 are_homotopic iff p1,p2 are_homotopic )
A3:
( 0 is Point of I[01] & 1 is Point of I[01] )
by BORSUK_1:40, XXREAL_1:1;
A4:
( inf (dom c1) = 0 & sup (dom c1) = 1 & inf (dom c2) = 0 & sup (dom c2) = 1 )
by A1, Th4;
A5:
( dom p1 = the carrier of I[01] & dom p2 = the carrier of I[01] )
by FUNCT_2:def 1;
thus
( c1,c2 are_homotopic implies p1,p2 are_homotopic )
( p1,p2 are_homotopic implies c1,c2 are_homotopic )proof
assume
c1,
c2 are_homotopic
;
p1,p2 are_homotopic
then consider aa,
bb being
Point of
T,
pp1,
pp2 being
Path of
aa,
bb such that A6:
(
pp1 = c1 * (L[01] (0,1,(inf (dom c1)),(sup (dom c1)))) &
pp2 = c2 * (L[01] (0,1,(inf (dom c2)),(sup (dom c2)))) &
pp1,
pp2 are_homotopic )
;
consider f being
Function of
[:I[01],I[01]:],
T such that A7:
(
f is
continuous & ( for
t being
Point of
I[01] holds
(
f . (
t,
0)
= pp1 . t &
f . (
t,1)
= pp2 . t &
f . (
0,
t)
= aa &
f . (1,
t)
= bb ) ) )
by A6;
A8:
(
pp1 = p1 &
pp2 = p2 )
by A1, A6, A4, A5, Th1, RELAT_1:52, TOPMETR:20;
A9:
(
f . (
0,
0)
= pp1 . 0 &
f . (
0,1)
= pp2 . 0 &
f . (
0,
0)
= aa &
f . (
0,1)
= aa )
by A7, A3;
A10:
(
f . (1,
0)
= pp1 . 1 &
f . (1,1)
= pp2 . 1 &
f . (1,
0)
= bb &
f . (1,1)
= bb )
by A7, A3;
(
aa = a &
bb = b )
by A8, A9, A10, A2, BORSUK_2:def 2;
hence
p1,
p2 are_homotopic
by A7, A8;
verum
end;
assume A11:
p1,p2 are_homotopic
; c1,c2 are_homotopic
( p1 = p1 * (L[01] (0,1,0,1)) & p2 = p2 * (L[01] (0,1,0,1)) )
by A5, Th1, RELAT_1:52, TOPMETR:20;
hence
c1,c2 are_homotopic
by A4, A1, A11; verum