let n be Element of NAT ; :: thesis: 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

let T be non empty convex SubSpace of TOP-REAL n; :: thesis: for P, Q being continuous Function of I[01],T holds ConvexHomotopy (P,Q) is continuous

let P, Q be continuous Function of I[01],T; :: thesis: ConvexHomotopy (P,Q) is continuous

set F = ConvexHomotopy (P,Q);

A1: the carrier of T is Subset of (TOP-REAL n) by TSEP_1:1;

then reconsider G = ConvexHomotopy (P,Q) as Function of [:I[01],I[01]:],(TOP-REAL n) by FUNCT_2:7;

reconsider P1 = P, Q1 = Q as Function of I[01],(TOP-REAL n) by A1, FUNCT_2:7;

set E = the carrier of (TOP-REAL n);

set PI = [:P,(id I[01]):];

set QI = [:Q,(id I[01]):];

reconsider P1 = P1, Q1 = Q1 as continuous Function of I[01],(TOP-REAL n) by PRE_TOPC:26;

set P1I = [:P1,(id I[01]):];

set Q1I = [:Q1,(id I[01]):];

deffunc H_{1}( Element of the carrier of (TOP-REAL n), Element of the carrier of I[01]) -> Element of the carrier of (TOP-REAL n) = $2 * $1;

deffunc H_{2}( Element of the carrier of (TOP-REAL n), Element of the carrier of I[01]) -> Element of the carrier of (TOP-REAL n) = (1 - $2) * $1;

consider Pa being Function of [: the carrier of (TOP-REAL n), the carrier of I[01]:], the carrier of (TOP-REAL n) such that

A2: for x being Element of the carrier of (TOP-REAL n)

for i being Element of the carrier of I[01] holds Pa . (x,i) = H_{2}(x,i)
from BINOP_1:sch 4();

consider Pb being Function of [: the carrier of (TOP-REAL n), the carrier of I[01]:], the carrier of (TOP-REAL n) such that

A3: for x being Element of the carrier of (TOP-REAL n)

for i being Element of the carrier of I[01] holds Pb . (x,i) = H_{1}(x,i)
from BINOP_1:sch 4();

the carrier of [:(TOP-REAL n),I[01]:] = [: the carrier of (TOP-REAL n), the carrier of I[01]:] by BORSUK_1:def 2;

then reconsider Pa = Pa, Pb = Pb as Function of [:(TOP-REAL n),I[01]:],(TOP-REAL n) ;

A4: Pb is continuous by A3, TOPALG_1:18;

Pa is continuous by A2, TOPALG_1:17;

then consider g being Function of [:I[01],I[01]:],(TOP-REAL n) such that

A5: for r being Point of [:I[01],I[01]:] holds g . r = ((Pa * [:P1,(id I[01]):]) . r) + ((Pb * [:Q1,(id I[01]):]) . r) and

A6: g is continuous by A4, JGRAPH_6:12;

A7: for p being Point of [:I[01],I[01]:] holds G . p = ((Pa * [:P1,(id I[01]):]) . p) + ((Pb * [:Q1,(id I[01]):]) . p)

for P, Q being continuous Function of I[01],T holds ConvexHomotopy (P,Q) is continuous

let T be non empty convex SubSpace of TOP-REAL n; :: thesis: for P, Q being continuous Function of I[01],T holds ConvexHomotopy (P,Q) is continuous

let P, Q be continuous Function of I[01],T; :: thesis: ConvexHomotopy (P,Q) is continuous

set F = ConvexHomotopy (P,Q);

A1: the carrier of T is Subset of (TOP-REAL n) by TSEP_1:1;

then reconsider G = ConvexHomotopy (P,Q) as Function of [:I[01],I[01]:],(TOP-REAL n) by FUNCT_2:7;

reconsider P1 = P, Q1 = Q as Function of I[01],(TOP-REAL n) by A1, FUNCT_2:7;

set E = the carrier of (TOP-REAL n);

set PI = [:P,(id I[01]):];

set QI = [:Q,(id I[01]):];

reconsider P1 = P1, Q1 = Q1 as continuous Function of I[01],(TOP-REAL n) by PRE_TOPC:26;

set P1I = [:P1,(id I[01]):];

set Q1I = [:Q1,(id I[01]):];

deffunc H

deffunc H

consider Pa being Function of [: the carrier of (TOP-REAL n), the carrier of I[01]:], the carrier of (TOP-REAL n) such that

A2: for x being Element of the carrier of (TOP-REAL n)

for i being Element of the carrier of I[01] holds Pa . (x,i) = H

consider Pb being Function of [: the carrier of (TOP-REAL n), the carrier of I[01]:], the carrier of (TOP-REAL n) such that

A3: for x being Element of the carrier of (TOP-REAL n)

for i being Element of the carrier of I[01] holds Pb . (x,i) = H

the carrier of [:(TOP-REAL n),I[01]:] = [: the carrier of (TOP-REAL n), the carrier of I[01]:] by BORSUK_1:def 2;

then reconsider Pa = Pa, Pb = Pb as Function of [:(TOP-REAL n),I[01]:],(TOP-REAL n) ;

A4: Pb is continuous by A3, TOPALG_1:18;

Pa is continuous by A2, TOPALG_1:17;

then consider g being Function of [:I[01],I[01]:],(TOP-REAL n) such that

A5: for r being Point of [:I[01],I[01]:] holds g . r = ((Pa * [:P1,(id I[01]):]) . r) + ((Pb * [:Q1,(id I[01]):]) . r) and

A6: g is continuous by A4, JGRAPH_6:12;

A7: for p being Point of [:I[01],I[01]:] holds G . p = ((Pa * [:P1,(id I[01]):]) . p) + ((Pb * [:Q1,(id I[01]):]) . p)

proof

for p being Point of [:I[01],I[01]:] holds G . p = g . p
A8:
dom Q = the carrier of I[01]
by FUNCT_2:def 1;

A9: dom P = the carrier of I[01] by FUNCT_2:def 1;

let p be Point of [:I[01],I[01]:]; :: thesis: G . p = ((Pa * [:P1,(id I[01]):]) . p) + ((Pb * [:Q1,(id I[01]):]) . p)

consider s, t being Point of I[01] such that

A10: p = [s,t] by BORSUK_1:10;

reconsider a1 = P . s, b1 = Q . s as Point of (TOP-REAL n) by PRE_TOPC:25;

A11: (ConvexHomotopy (P,Q)) . (s,t) = ((1 - t) * a1) + (t * b1) by Def2;

A12: (id I[01]) . t = t by FUNCT_1:18;

A13: (Pb * [:Q,(id I[01]):]) . p = Pb . ([:Q,(id I[01]):] . (s,t)) by A10, FUNCT_2:15

.= Pb . ((Q . s),t) by A8, A12, Lm4, FUNCT_3:def 8

.= t * (Q1 . s) by A3 ;

(Pa * [:P,(id I[01]):]) . p = Pa . ([:P,(id I[01]):] . (s,t)) by A10, FUNCT_2:15

.= Pa . ((P . s),t) by A9, A12, Lm4, FUNCT_3:def 8

.= (1 - t) * (P1 . s) by A2 ;

hence G . p = ((Pa * [:P1,(id I[01]):]) . p) + ((Pb * [:Q1,(id I[01]):]) . p) by A10, A13, A11; :: thesis: verum

end;A9: dom P = the carrier of I[01] by FUNCT_2:def 1;

let p be Point of [:I[01],I[01]:]; :: thesis: G . p = ((Pa * [:P1,(id I[01]):]) . p) + ((Pb * [:Q1,(id I[01]):]) . p)

consider s, t being Point of I[01] such that

A10: p = [s,t] by BORSUK_1:10;

reconsider a1 = P . s, b1 = Q . s as Point of (TOP-REAL n) by PRE_TOPC:25;

A11: (ConvexHomotopy (P,Q)) . (s,t) = ((1 - t) * a1) + (t * b1) by Def2;

A12: (id I[01]) . t = t by FUNCT_1:18;

A13: (Pb * [:Q,(id I[01]):]) . p = Pb . ([:Q,(id I[01]):] . (s,t)) by A10, FUNCT_2:15

.= Pb . ((Q . s),t) by A8, A12, Lm4, FUNCT_3:def 8

.= t * (Q1 . s) by A3 ;

(Pa * [:P,(id I[01]):]) . p = Pa . ([:P,(id I[01]):] . (s,t)) by A10, FUNCT_2:15

.= Pa . ((P . s),t) by A9, A12, Lm4, FUNCT_3:def 8

.= (1 - t) * (P1 . s) by A2 ;

hence G . p = ((Pa * [:P1,(id I[01]):]) . p) + ((Pb * [:Q1,(id I[01]):]) . p) by A10, A13, A11; :: thesis: verum

proof

hence
ConvexHomotopy (P,Q) is continuous
by A6, FUNCT_2:63, PRE_TOPC:27; :: thesis: verum
let p be Point of [:I[01],I[01]:]; :: thesis: G . p = g . p

thus G . p = ((Pa * [:P1,(id I[01]):]) . p) + ((Pb * [:Q1,(id I[01]):]) . p) by A7

.= g . p by A5 ; :: thesis: verum

end;thus G . p = ((Pa * [:P1,(id I[01]):]) . p) + ((Pb * [:Q1,(id I[01]):]) . p) by A7

.= g . p by A5 ; :: thesis: verum