begin
set I = the carrier of I[01];
Lm1:
the carrier of [:I[01],I[01]:] = [: the carrier of I[01], the carrier of I[01]:]
by BORSUK_1:def 2;
Lm2:
the carrier of [:(TOP-REAL 1),I[01]:] = [: the carrier of (TOP-REAL 1), the carrier of I[01]:]
by BORSUK_1:def 2;
Lm3:
the carrier of [:R^1,I[01]:] = [: the carrier of R^1, the carrier of I[01]:]
by BORSUK_1:def 2;
Lm4:
dom (id I[01]) = the carrier of I[01]
by FUNCT_2:def 1;
definition
let n be
Element of
NAT ;
let T be non
empty convex SubSpace of
TOP-REAL n;
let P,
Q be
Function of
I[01],
T;
existence
ex b1 being Function of [:I[01],I[01]:],T st
for s, t being Element of I[01]
for a1, b1 being Point of (TOP-REAL n) st a1 = P . s & b1 = Q . s holds
b1 . (s,t) = ((1 - t) * a1) + (t * b1)
uniqueness
for b1, b2 being Function of [:I[01],I[01]:],T st ( for s, t being Element of I[01]
for a1, b1 being Point of (TOP-REAL n) st a1 = P . s & b1 = Q . s holds
b1 . (s,t) = ((1 - t) * a1) + (t * b1) ) & ( for s, t being Element of I[01]
for a1, b1 being Point of (TOP-REAL n) st a1 = P . s & b1 = Q . s holds
b2 . (s,t) = ((1 - t) * a1) + (t * b1) ) holds
b1 = b2
end;
Lm5:
for n being Element of NAT
for T being non empty convex SubSpace of TOP-REAL n
for P, Q being continuous Function of I[01],T holds ConvexHomotopy (P,Q) is continuous
Lm6:
for n being Element of NAT
for T being non empty convex SubSpace of TOP-REAL n
for a, b being Point of T
for P, Q being Path of a,b
for s being Point of I[01] holds
( (ConvexHomotopy (P,Q)) . (s,0) = P . s & (ConvexHomotopy (P,Q)) . (s,1) = Q . s & ( for t being Point of I[01] holds
( (ConvexHomotopy (P,Q)) . (0,t) = a & (ConvexHomotopy (P,Q)) . (1,t) = b ) ) )
begin
Lm7:
for T being SubSpace of R^1 st T = R^1 holds
T is interval
definition
let T be non
empty interval SubSpace of
R^1 ;
let P,
Q be
Function of
I[01],
T;
existence
ex b1 being Function of [:I[01],I[01]:],T st
for s, t being Element of I[01] holds b1 . (s,t) = ((1 - t) * (P . s)) + (t * (Q . s))
uniqueness
for b1, b2 being Function of [:I[01],I[01]:],T st ( for s, t being Element of I[01] holds b1 . (s,t) = ((1 - t) * (P . s)) + (t * (Q . s)) ) & ( for s, t being Element of I[01] holds b2 . (s,t) = ((1 - t) * (P . s)) + (t * (Q . s)) ) holds
b1 = b2
end;
Lm8:
for T being non empty interval SubSpace of R^1
for P, Q being continuous Function of I[01],T holds R1Homotopy (P,Q) is continuous
Lm9:
for T being non empty interval SubSpace of R^1
for a, b being Point of T
for P, Q being Path of a,b
for s being Point of I[01] holds
( (R1Homotopy (P,Q)) . (s,0) = P . s & (R1Homotopy (P,Q)) . (s,1) = Q . s & ( for t being Point of I[01] holds
( (R1Homotopy (P,Q)) . (0,t) = a & (R1Homotopy (P,Q)) . (1,t) = b ) ) )