:: deftheorem defines Homotopy BORSUK_6:def 11 :
for T being non empty TopSpace
for a, b being Point of T
for P, Q being Path of a,b st P,Q are_homotopic holds
for b₆ being Function of [:I[01],I[01]:],T holds
( b₆ is Homotopy of P,Q iff ( b₆ is continuous & ( for t being Point of I[01] holds
( b₆ . (t,0) = P . t & b₆ . (t,1) = Q . t & b₆ . (0,t) = a & b₆ . (1,t) = b ) ) ) );