begin
:: deftheorem Def1 defines convex TOPALG_2:def 1 :
theorem
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 5;
Lm2:
the carrier of [:(TOP-REAL 1),I[01] :] = [:the carrier of (TOP-REAL 1),the carrier of I[01] :]
by BORSUK_1:def 5;
Lm3:
the carrier of [:R^1 ,I[01] :] = [:the carrier of R^1 ,the carrier of I[01] :]
by BORSUK_1:def 5;
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;
func ConvexHomotopy P,
Q -> Function of
[:I[01] ,I[01] :],
T means :
Def2:
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
it . s,
t = ((1 - t) * a1) + (t * b1);
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;
:: deftheorem Def2 defines ConvexHomotopy TOPALG_2:def 2 :
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 ) ) )
theorem Th2:
theorem Th3:
begin
theorem Th4:
theorem
theorem Th6:
theorem Th7:
:: deftheorem Def3 defines convex TOPALG_2:def 3 :
theorem Th8:
theorem
theorem
theorem
:: deftheorem Def4 defines convex TOPALG_2:def 4 :
Lm7:
for T being SubSpace of R^1 st T = R^1 holds
T is convex
theorem Th12:
theorem Th13:
theorem Th14:
theorem
definition
let T be non
empty convex SubSpace of
R^1 ;
let P,
Q be
Function of
I[01] ,
T;
func R1Homotopy P,
Q -> Function of
[:I[01] ,I[01] :],
T means :
Def5:
for
s,
t being
Element of
I[01] holds
it . s,
t = ((1 - t) * (P . s)) + (t * (Q . s));
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;
:: deftheorem Def5 defines R1Homotopy TOPALG_2:def 5 :
Lm8:
for T being non empty convex 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 convex 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 ) ) )
theorem Th16:
theorem Th17:
theorem
theorem
theorem
theorem
theorem
theorem