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;
set E = the carrier of (TOP-REAL n);
set PI = [:P,(id I[01] ):];
set QI = [:Q,(id I[01] ):];
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:9;
reconsider P1 = P, Q1 = Q as Function of I[01] ,(TOP-REAL n) by A1, FUNCT_2:9;
reconsider P1 = P1, Q1 = Q1 as continuous Function of I[01] ,(TOP-REAL n) by PRE_TOPC:56;
set P1I = [:P1,(id I[01] ):];
set Q1I = [:Q1,(id I[01] ):];
A2:
( [:P1,(id I[01] ):] is continuous & [:Q1,(id I[01] ):] is continuous )
by BORSUK_2:12;
deffunc H1( 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;
deffunc H2( 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;
consider Pa 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 Pa . x,i = H1(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
A4:
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 = H2(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 5;
then reconsider Pa = Pa, Pb = Pb as Function of [:(TOP-REAL n),I[01] :],(TOP-REAL n) ;
( Pa is continuous & Pb is continuous )
by A3, A4, TOPALG_1:18, TOPALG_1:19;
then A5:
( Pa * [:P1,(id I[01] ):] is continuous & Pb * [:Q1,(id I[01] ):] is continuous )
by A2;
A6:
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
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 A7:
p = [s,t]
by BORSUK_1:50;
A8:
dom P = the
carrier of
I[01]
by FUNCT_2:def 1;
A9:
dom Q = the
carrier of
I[01]
by FUNCT_2:def 1;
A10:
(id I[01] ) . t = t
by FUNCT_1:35;
A11:
(Pa * [:P,(id I[01] ):]) . p =
Pa . ([:P,(id I[01] ):] . s,t)
by A7, FUNCT_2:21
.=
Pa . (P . s),
t
by A8, A10, Lm4, FUNCT_3:def 9
.=
(1 - t) * (P1 . s)
by A3
;
A12:
(Pb * [:Q,(id I[01] ):]) . p =
Pb . ([:Q,(id I[01] ):] . s,t)
by A7, FUNCT_2:21
.=
Pb . (Q . s),
t
by A9, A10, Lm4, FUNCT_3:def 9
.=
t * (Q1 . s)
by A4
;
reconsider a1 =
P . s,
b1 =
Q . s as
Point of
(TOP-REAL n) by PRE_TOPC:55;
(ConvexHomotopy P,Q) . s,
t = ((1 - t) * a1) + (t * b1)
by Def2;
hence
G . p = ((Pa * [:P1,(id I[01] ):]) . p) + ((Pb * [:Q1,(id I[01] ):]) . p)
by A7, A11, A12;
:: thesis: verum
end;
consider g being Function of [:I[01] ,I[01] :],(TOP-REAL n) such that
A13:
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
A14:
g is continuous
by A5, JGRAPH_6:20;
for p being Point of [:I[01] ,I[01] :] holds G . p = g . p
then
G = g
by FUNCT_2:113;
hence
ConvexHomotopy P,Q is continuous
by A14, PRE_TOPC:57; :: thesis: verum