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 18 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 Def2;
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 Def2;
now for xx, xx9 being Point of [:XX,I[01]:] holds
( not II . xx = II . xx9 or not ((Proj (TrivExt D)) * CH1) . xx <> ((Proj (TrivExt D)) * CH1) . xx9 )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:15;
consider x being
Point of
XX,
t being
Point of
I[01] such that A5:
xx = [x,t]
by Th10;
consider x9 being
Point of
XX,
t9 being
Point of
I[01] such that A6:
xx9 = [x9,t9]
by Th10;
A7:
(
II . (
x,
t)
= [((Proj (TrivExt D)) . x),t] &
II . (
x9,
t9)
= [((Proj (TrivExt D)) . x9),t9] )
by EQREL_1:58;
then
(
t = t9 &
(Proj (TrivExt D)) . x = (Proj (TrivExt D)) . x9 )
by A2, A5, A6, XTUPLE_0:1;
then
(
CH1 . xx = x &
CH1 . xx9 = x9 )
by A1, A3, A5, A6, Th35;
hence
contradiction
by A2, A3, A5, A6, A7, A4, XTUPLE_0:1;
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:56;
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 1 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 Def2;
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 Th10;
II " {xt9} = [:((Proj (TrivExt D)) " {W}),{T}:]
by A9, EQREL_1:60;
then reconsider GG =
FF " G as
a_neighborhood of
[:((Proj (TrivExt D)) " {W}),{T}:] by A8, Th4, EQREL_1:57;
W in the
carrier of
(space (TrivExt D))
;
then A10:
W in TrivExt D
by Def7;
then
(Proj (TrivExt D)) " {W} = W
by EQREL_1:66;
then
(Proj (TrivExt D)) " {W} is
compact
by A10, Def12;
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 Th25;
reconsider H9 =
(Proj (TrivExt D)) .: U as
a_neighborhood of
W by Th38;
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:59;
then A12:
(
((Proj (TrivExt D)) * CH1) .: GG c= G &
THETA .: H = ((Proj (TrivExt D)) * CH1) .: [:U,V:] )
by A8, FUNCT_1:75, RELAT_1:126;
((Proj (TrivExt D)) * CH1) .: [:U,V:] c= ((Proj (TrivExt D)) * CH1) .: GG
by A11, RELAT_1:123;
hence
THETA .: H c= G
by A12;
verum
end;
then reconsider THETA9 = THETA as continuous Function of [:(space (TrivExt D)),I[01]:],(space (TrivExt D)) ;
take THETA99 = THETA9; BORSUK_1:def 18 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 Th29;
II . (W9,0[01]) = [W,0[01]]
by A13, EQREL_1:58;
then A14:
(THETA9 * II) . [W9,0[01]] = THETA9 . [W,0[01]]
by FUNCT_2:15;
CH1 . (W9,0[01]) = W9
by A1;
hence
THETA99 . [W,0[01]] = W
by A8, A13, A14, FUNCT_2:15; ( 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:58;
then A16:
(THETA9 * II) . [W9,1[01]] = THETA9 . [W,1[01]]
by FUNCT_2:15;
(THETA9 * II) . [W9,1[01]] = (Proj (TrivExt D)) . (CH1 . [W9,1[01]])
by A8, FUNCT_2:15;
hence
THETA99 . [W,1[01]] in the carrier of (space D)
by A16, A15, Th37; ( 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:58;
then A18:
(THETA9 * II) . [W9,T] = THETA9 . [W,T]
by FUNCT_2:15;
CH1 . (W9,T) = W9
by A1, A13, A17, Th36;
hence
THETA99 . [W,T] = W
by A8, A13, A18, FUNCT_2:15; verum