let XX be non empty TopSpace; for X being non empty closed SubSpace of XX
for D being DECOMPOSITION of X st X is_an_SDR_of XX holds
space D is_an_SDR_of space (TrivExt D)
let X be non empty closed SubSpace of XX; for D being DECOMPOSITION of X st X is_an_SDR_of XX holds
space D is_an_SDR_of space (TrivExt D)
let D be DECOMPOSITION of X; ( X is_an_SDR_of XX implies space D is_an_SDR_of space (TrivExt D) )
given CH1 being continuous Function of [:XX,I[01] :],XX such that A1:
for A being Point of XX holds
( CH1 . [A,0[01] ] = A & CH1 . [A,1[01] ] in the carrier of X & ( A in the carrier of X implies for T being Point of I[01] holds CH1 . [A,T] = A ) )
; BORSUK_1:def 21 space D is_an_SDR_of space (TrivExt D)
the carrier of [:XX,I[01] :] = [:the carrier of XX,the carrier of I[01] :]
by Def5;
then reconsider II = [:(Proj (TrivExt D)),(id the carrier of I[01] ):] as Function of the carrier of [:XX,I[01] :],the carrier of [:(space (TrivExt D)),I[01] :] by Def5;
now given xx,
xx9 being
Point of
[:XX,I[01] :] such that A2:
II . xx = II . xx9
and A3:
((Proj (TrivExt D)) * CH1) . xx <> ((Proj (TrivExt D)) * CH1) . xx9
;
contradictionA4:
(
((Proj (TrivExt D)) * CH1) . xx = (Proj (TrivExt D)) . (CH1 . xx) &
((Proj (TrivExt D)) * CH1) . xx9 = (Proj (TrivExt D)) . (CH1 . xx9) )
by FUNCT_2:21;
consider x being
Point of
XX,
t being
Point of
I[01] such that A5:
xx = [x,t]
by Th50;
consider x9 being
Point of
XX,
t9 being
Point of
I[01] such that A6:
xx9 = [x9,t9]
by Th50;
A7:
(
II . x,
t = [((Proj (TrivExt D)) . x),t] &
II . x9,
t9 = [((Proj (TrivExt D)) . x9),t9] )
by EQREL_1:67;
then
(
t = t9 &
(Proj (TrivExt D)) . x = (Proj (TrivExt D)) . x9 )
by A2, A5, A6, ZFMISC_1:33;
then
(
CH1 . xx = x &
CH1 . xx9 = x9 )
by A1, A3, A5, A6, Th78;
hence
contradiction
by A2, A3, A5, A6, A7, A4, ZFMISC_1:33;
verum end;
then consider THETA being Function of the carrier of [:(space (TrivExt D)),I[01] :],the carrier of (space (TrivExt D)) such that
A8:
(Proj (TrivExt D)) * CH1 = THETA * II
by EQREL_1:65;
reconsider THETA = THETA as Function of [:(space (TrivExt D)),I[01] :],(space (TrivExt D)) ;
THETA is continuous
proof
let WT be
Point of
[:(space (TrivExt D)),I[01] :];
BORSUK_1:def 3 for G being a_neighborhood of THETA . WT ex H being a_neighborhood of WT st THETA .: H c= G
reconsider xt9 =
WT as
Element of
[:the carrier of (space (TrivExt D)),the carrier of I[01] :] by Def5;
let G be
a_neighborhood of
THETA . WT;
ex H being a_neighborhood of WT st THETA .: H c= G
reconsider FF =
(Proj (TrivExt D)) * CH1 as
continuous Function of
[:XX,I[01] :],
(space (TrivExt D)) ;
consider W being
Point of
(space (TrivExt D)),
T being
Point of
I[01] such that A9:
WT = [W,T]
by Th50;
II " {xt9} = [:((Proj (TrivExt D)) " {W}),{T}:]
by A9, EQREL_1:69;
then reconsider GG =
FF " G as
a_neighborhood of
[:((Proj (TrivExt D)) " {W}),{T}:] by A8, EQREL_1:66, Th39;
W in the
carrier of
(space (TrivExt D))
;
then A10:
W in TrivExt D
by Def10;
then
(Proj (TrivExt D)) " {W} = W
by EQREL_1:75;
then
(Proj (TrivExt D)) " {W} is
compact
by A10, Def15;
then consider U being
a_neighborhood of
(Proj (TrivExt D)) " {W},
V being
a_neighborhood of
T such that A11:
[:U,V:] c= GG
by Th67;
reconsider H9 =
(Proj (TrivExt D)) .: U as
a_neighborhood of
W by Th81;
reconsider H99 =
[:H9,V:] as
a_neighborhood of
WT by A9;
take H =
H99;
THETA .: H c= G
II .: [:U,V:] = [:((Proj (TrivExt D)) .: U),V:]
by EQREL_1:68;
then A12:
(
((Proj (TrivExt D)) * CH1) .: GG c= G &
THETA .: H = ((Proj (TrivExt D)) * CH1) .: [:U,V:] )
by A8, FUNCT_1:145, RELAT_1:159;
((Proj (TrivExt D)) * CH1) .: [:U,V:] c= ((Proj (TrivExt D)) * CH1) .: GG
by A11, RELAT_1:156;
hence
THETA .: H c= G
by A12, XBOOLE_1:1;
verum
end;
then reconsider THETA9 = THETA as continuous Function of [:(space (TrivExt D)),I[01] :],(space (TrivExt D)) ;
take THETA99 = THETA9; BORSUK_1:def 21 for A being Point of (space (TrivExt D)) holds
( THETA99 . [A,0[01] ] = A & THETA99 . [A,1[01] ] in the carrier of (space D) & ( A in the carrier of (space D) implies for T being Point of I[01] holds THETA99 . [A,T] = A ) )
let W be Point of (space (TrivExt D)); ( THETA99 . [W,0[01] ] = W & THETA99 . [W,1[01] ] in the carrier of (space D) & ( W in the carrier of (space D) implies for T being Point of I[01] holds THETA99 . [W,T] = W ) )
consider W9 being Point of XX such that
A13:
(Proj (TrivExt D)) . W9 = W
by Th71;
II . W9,0[01] = [W,0[01] ]
by A13, EQREL_1:67;
then A14:
(THETA9 * II) . [W9,0[01] ] = THETA9 . [W,0[01] ]
by FUNCT_2:21;
CH1 . W9,0[01] = W9
by A1;
hence
THETA99 . [W,0[01] ] = W
by A8, A13, A14, FUNCT_2:21; ( THETA99 . [W,1[01] ] in the carrier of (space D) & ( W in the carrier of (space D) implies for T being Point of I[01] holds THETA99 . [W,T] = W ) )
A15:
CH1 . [W9,1[01] ] in the carrier of X
by A1;
II . W9,1[01] = [W,1[01] ]
by A13, EQREL_1:67;
then A16:
(THETA9 * II) . [W9,1[01] ] = THETA9 . [W,1[01] ]
by FUNCT_2:21;
(THETA9 * II) . [W9,1[01] ] = (Proj (TrivExt D)) . (CH1 . [W9,1[01] ])
by A8, FUNCT_2:21;
hence
THETA99 . [W,1[01] ] in the carrier of (space D)
by A16, A15, Th80; ( W in the carrier of (space D) implies for T being Point of I[01] holds THETA99 . [W,T] = W )
assume A17:
W in the carrier of (space D)
; for T being Point of I[01] holds THETA99 . [W,T] = W
let T be Point of I[01] ; THETA99 . [W,T] = W
II . W9,T = [W,T]
by A13, EQREL_1:67;
then A18:
(THETA9 * II) . [W9,T] = THETA9 . [W,T]
by FUNCT_2:21;
CH1 . W9,T = W9
by A1, A13, A17, Th79;
hence
THETA99 . [W,T] = W
by A8, A13, A18, FUNCT_2:21; verum