let n be Element of NAT ; :: thesis: for P, Q being continuous Function of I[01] ,(TOP-REAL n) holds RealHomotopy P,Q is continuous
let P, Q be continuous Function of I[01] ,(TOP-REAL n); :: thesis: RealHomotopy P,Q is continuous
set F = RealHomotopy P,Q;
set I = the carrier of I[01] ;
set T = the carrier of (TOP-REAL n);
set PI = [:P,(id I[01] ):];
set QI = [:Q,(id I[01] ):];
A1:
( [:P,(id I[01] ):] is continuous & [:Q,(id I[01] ):] is continuous )
by BORSUK_2:12;
deffunc H1( Element 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 (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
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 = 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
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 = 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 A2, A3, Th18, Th19;
then A4:
( Pa * [:P,(id I[01] ):] is continuous & Pb * [:Q,(id I[01] ):] is continuous )
by A1;
for p being Point of [:I[01] ,I[01] :] holds (RealHomotopy P,Q) . p = ((Pa * [:P,(id I[01] ):]) . p) + ((Pb * [:Q,(id I[01] ):]) . p)
proof
let p be
Point of
[:I[01] ,I[01] :];
:: thesis: (RealHomotopy P,Q) . p = ((Pa * [:P,(id I[01] ):]) . p) + ((Pb * [:Q,(id I[01] ):]) . p)
consider s,
t being
Point of
I[01] such that A5:
p = [s,t]
by BORSUK_1:50;
A6:
dom P = the
carrier of
I[01]
by FUNCT_2:def 1;
A7:
dom Q = the
carrier of
I[01]
by FUNCT_2:def 1;
A8:
dom (id I[01] ) = the
carrier of
I[01]
by FUNCT_2:def 1;
A9:
(id I[01] ) . t = t
by FUNCT_1:35;
A10:
(Pa * [:P,(id I[01] ):]) . p =
Pa . ([:P,(id I[01] ):] . s,t)
by A5, FUNCT_2:21
.=
Pa . (P . s),
t
by A6, A8, A9, FUNCT_3:def 9
.=
(1 - t) * (P . s)
by A2
;
A11:
(Pb * [:Q,(id I[01] ):]) . p =
Pb . ([:Q,(id I[01] ):] . s,t)
by A5, FUNCT_2:21
.=
Pb . (Q . s),
t
by A7, A8, A9, FUNCT_3:def 9
.=
t * (Q . s)
by A3
;
thus (RealHomotopy P,Q) . p =
(RealHomotopy P,Q) . s,
t
by A5
.=
((Pa * [:P,(id I[01] ):]) . p) + ((Pb * [:Q,(id I[01] ):]) . p)
by A10, A11, Def5
;
:: thesis: verum
end;
hence
RealHomotopy P,Q is continuous
by A4, Lm1; :: thesis: verum