let n be Element of NAT ; :: thesis:
let T be non empty convex SubSpace of TOP-REAL n; :: thesis:
let a, b be Point of T; :: thesis:
let P, Q be Path of a,b; :: thesis:
set F = ConvexHomotopy P,Q;
let s be Point of I[01] ; :: thesis:
reconsider x0 = 0 , x1 = 1 as Point of I[01] by BORSUK_1:def 17, BORSUK_1:def 18;
reconsider a1 = P . s, b1 = Q . s as Point of (TOP-REAL n) by PRE_TOPC:55;
(ConvexHomotopy P,Q) . s,x0 = ((1 - x0) * a1) + (x0 * b1) by Def2;
hence (ConvexHomotopy P,Q) . s,0 = a1 + (0 * b1) by EUCLID:33
.= a1 + (0. (TOP-REAL n)) by EUCLID:33
.= P . s by EUCLID:31 ;
:: thesis:
(ConvexHomotopy P,Q) . s,x1 = ((1 - x1) * a1) + (x1 * b1) by Def2;
hence (ConvexHomotopy P,Q) . s,1 = (0. (TOP-REAL n)) + (1 * b1) by EUCLID:33
.= (0. (TOP-REAL n)) + b1 by EUCLID:33
.= Q . s by EUCLID:31 ;
:: thesis:
let t be Point of I[01] ; :: thesis:
reconsider a1 = P . x0, b1 = Q . x0 as Point of (TOP-REAL n) by PRE_TOPC:55;
A1: (ConvexHomotopy P,Q) . 0 ,t = ((1 - t) * a1) + (t * b1) by Def2;
A2: P . x0 = a by BORSUK_2:def 4;
A3: Q . x0 = a by BORSUK_2:def 4;
A4: P . x1 = b by BORSUK_2:def 4;
A5: Q . x1 = b by BORSUK_2:def 4;
thus (ConvexHomotopy P,Q) . 0 ,t = ((1 * a1) - (t * a1)) + (t * a1) by A1, A2, A3, EUCLID:54
.= 1 * a1 by EUCLID:52
.= a by A2, EUCLID:33 ; :: thesis:
reconsider a1 = P . x1, b1 = Q . x1 as Point of (TOP-REAL n) by PRE_TOPC:55;
(ConvexHomotopy P,Q) . 1,t = ((1 - t) * a1) + (t * b1) by Def2;
hence (ConvexHomotopy P,Q) . 1,t = ((1 * a1) - (t * b1)) + (t * a1) by A4, A5, EUCLID:54
.= 1 * b1 by A4, A5, EUCLID:52
.= b by A5, EUCLID:33 ;
:: thesis: