environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, XBOOLE_0, CONVEX1, EUCLID, PRE_TOPC, RLTOPSP1, BORSUK_2, STRUCT_0, RELAT_1, TARSKI, TOPREAL1, FUNCT_1, BORSUK_1, TOPS_2, CARD_1, ORDINAL2, GRAPH_1, ZFMISC_1, TOPMETR, ARYTM_1, ARYTM_3, XXREAL_0, REAL_1, SUPINF_2, BORSUK_6, ALGSTR_1, TOPALG_1, EQREL_1, WAYBEL20, PARTFUN1, FINSEQ_1, MEMBERED, XXREAL_1, VALUED_1, TREAL_1, TOPALG_2, MEASURE5, FUNCT_2, NAT_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, EQREL_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, BINOP_1, NUMBERS, XXREAL_2, XCMPLX_0, XREAL_0, REAL_1, STRUCT_0, PRE_TOPC, BORSUK_1, TOPS_2, TOPREAL1, TREAL_1, TOPMETR, RLVECT_1, RLTOPSP1, EUCLID, JORDAN2B, BORSUK_2, BORSUK_6, TOPALG_1, XXREAL_0, FINSEQ_1, RCOMP_1;
definitions TARSKI, XBOOLE_0, BORSUK_2, BORSUK_6, XXREAL_2;
theorems XREAL_0, TARSKI, FUNCT_2, TSEP_1, PRE_TOPC, EUCLID, TOPS_2, BORSUK_1, TOPALG_1, EQREL_1, BORSUK_2, BINOP_1, TOPMETR, JORDAN1, TOPREAL1, FUNCT_3, BORSUK_6, JGRAPH_2, FUNCT_1, JORDAN2B, FINSEQ_4, RVSUM_1, TREAL_1, XCMPLX_1, XREAL_1, JGRAPH_6, XXREAL_0, XXREAL_1, FINSEQ_1, XXREAL_2, RLVECT_1, RLVECT_4;
schemes BINOP_1;
registrations FUNCT_2, NUMBERS, XREAL_0, STRUCT_0, PRE_TOPC, BORSUK_1, EUCLID, TOPMETR, BORSUK_2, TOPALG_1, ZFMISC_1, RLTOPSP1, JORDAN2B, MONOID_0, MEMBERED, XXREAL_2, RELSET_1, JORDAN2C;
constructors HIDDEN, REAL_1, RCOMP_1, BINARITH, TOPS_2, T_0TOPSP, TOPREAL1, TREAL_1, JORDAN2B, BORSUK_6, TOPALG_1, CONVEX1, MONOID_0, XXREAL_2, BINOP_1;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, ARITHM, REAL;
equalities XBOOLE_0, BINOP_1, STRUCT_0, BORSUK_1, RLTOPSP1, TOPALG_1;
expansions XBOOLE_0, BORSUK_2;
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 ) ) )
Lm7:
for T being SubSpace of R^1 st T = R^1 holds
T is interval
by TOPMETR:17;
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 ) ) )