let XX be non empty TopSpace; :: thesis: 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; :: thesis: 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; :: thesis: ( X is_an_SDR_of XX implies space D is_an_SDR_of space (TrivExt D) )
( the carrier of [:XX,I[01] :] = [:the carrier of XX,the carrier of I[01] :] & the carrier of [:(space (TrivExt D)),I[01] :] = [:the carrier of (space (TrivExt D)),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] :] ;
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 ) )
; :: according to BORSUK_1:def 21 :: thesis: space D is_an_SDR_of space (TrivExt D)
now given xx,
xx' being
Point of
[:XX,I[01] :] such that A2:
II . xx = II . xx'
and A3:
((Proj (TrivExt D)) * CH1) . xx <> ((Proj (TrivExt D)) * CH1) . xx'
;
:: thesis: contradictionconsider x being
Point of
XX,
t being
Point of
I[01] such that A4:
xx = [x,t]
by Th50;
consider x' being
Point of
XX,
t' being
Point of
I[01] such that A5:
xx' = [x',t']
by Th50;
A6:
(
II . x,
t = [((Proj (TrivExt D)) . x),t] &
II . x',
t' = [((Proj (TrivExt D)) . x'),t'] )
by Th21;
then
(
t = t' &
(Proj (TrivExt D)) . x = (Proj (TrivExt D)) . x' )
by A2, A4, A5, ZFMISC_1:33;
then A7:
(
CH1 . xx = x &
CH1 . xx' = x' )
by A1, A5, A3, A4, Th78;
(
((Proj (TrivExt D)) * CH1) . xx = (Proj (TrivExt D)) . (CH1 . xx) &
((Proj (TrivExt D)) * CH1) . xx' = (Proj (TrivExt D)) . (CH1 . xx') )
by FUNCT_2:21;
hence
contradiction
by A2, A3, A4, A5, A6, A7, ZFMISC_1:33;
:: thesis: 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 Th19;
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] :];
:: according to BORSUK_1:def 3 :: thesis: for G being a_neighborhood of THETA . WT ex H being a_neighborhood of WT st THETA .: H c= G
reconsider xt' =
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;
:: thesis: 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 " {xt'} = [:((Proj (TrivExt D)) " {W}),{T}:]
by A9, Th24;
then reconsider GG =
FF " G as
a_neighborhood of
[:((Proj (TrivExt D)) " {W}),{T}:] by A8, Th20, Th39;
W in the
carrier of
(space (TrivExt D))
;
then A10:
W in TrivExt D
by Def10;
then
(Proj (TrivExt D)) " {W} = W
by Th30;
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 H' =
(Proj (TrivExt D)) .: U as
a_neighborhood of
W by Th81;
reconsider H'' =
[:H',V:] as
a_neighborhood of
WT by A9;
take H =
H'';
:: thesis: THETA .: H c= G
A12:
((Proj (TrivExt D)) * CH1) .: GG c= G
by FUNCT_1:145;
II .: [:U,V:] = [:((Proj (TrivExt D)) .: U),V:]
by Th23;
then A13:
THETA .: H = ((Proj (TrivExt D)) * CH1) .: [:U,V:]
by A8, 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, A13, XBOOLE_1:1;
:: thesis: verum
end;
then reconsider THETA' = THETA as continuous Function of [:(space (TrivExt D)),I[01] :],(space (TrivExt D)) ;
take THETA'' = THETA'; :: according to BORSUK_1:def 21 :: thesis: for A being Point of (space (TrivExt D)) holds
( THETA'' . [A,0[01] ] = A & THETA'' . [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 THETA'' . [A,T] = A ) )
let W be Point of (space (TrivExt D)); :: thesis: ( THETA'' . [W,0[01] ] = W & THETA'' . [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 THETA'' . [W,T] = W ) )
consider W' being Point of XX such that
A14:
(Proj (TrivExt D)) . W' = W
by Th71;
( CH1 . W',0[01] = W' & II . W',0[01] = [W,0[01] ] )
by A1, A14, Th21;
then
( (THETA' * II) . [W',0[01] ] = THETA' . [W,0[01] ] & (THETA' * II) . [W',0[01] ] = W )
by A8, A14, FUNCT_2:21;
hence
THETA'' . [W,0[01] ] = W
; :: thesis: ( THETA'' . [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 THETA'' . [W,T] = W ) )
II . W',1[01] = [W,1[01] ]
by A14, Th21;
then A15:
( (THETA' * II) . [W',1[01] ] = THETA' . [W,1[01] ] & (THETA' * II) . [W',1[01] ] = (Proj (TrivExt D)) . (CH1 . [W',1[01] ]) )
by A8, FUNCT_2:21;
CH1 . [W',1[01] ] in the carrier of X
by A1;
hence
THETA'' . [W,1[01] ] in the carrier of (space D)
by A15, Th80; :: thesis: ( W in the carrier of (space D) implies for T being Point of I[01] holds THETA'' . [W,T] = W )
assume A16:
W in the carrier of (space D)
; :: thesis: for T being Point of I[01] holds THETA'' . [W,T] = W
let T be Point of I[01] ; :: thesis: THETA'' . [W,T] = W
W' in the carrier of X
by A14, A16, Th79;
then
( CH1 . W',T = W' & II . W',T = [W,T] )
by A1, A14, Th21;
then
( (THETA' * II) . [W',T] = THETA' . [W,T] & (THETA' * II) . [W',T] = W )
by A8, A14, FUNCT_2:21;
hence
THETA'' . [W,T] = W
; :: thesis: verum