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_a_retract_of XX holds
space D is_a_retract_of space (TrivExt D)
let X be non empty closed SubSpace of XX; :: thesis: for D being DECOMPOSITION of X st X is_a_retract_of XX holds
space D is_a_retract_of space (TrivExt D)
let D be DECOMPOSITION of X; :: thesis: ( X is_a_retract_of XX implies space D is_a_retract_of space (TrivExt D) )
thus ( X is_a_retract_of XX implies space D is_a_retract_of space (TrivExt D) ) :: thesis: verum
proof
given R being continuous Function of XX,X such that A1: R is being_a_retraction ; :: according to BORSUK_1:def 17 :: thesis: space D is_a_retract_of space (TrivExt D)
now :: thesis: for xx, xx9 being Point of XX holds
( not (Proj (TrivExt D)) . xx = (Proj (TrivExt D)) . xx9 or not ((Proj D) * R) . xx <> ((Proj D) * R) . xx9 )
given xx, xx9 being Point of XX such that A2: ( (Proj (TrivExt D)) . xx = (Proj (TrivExt D)) . xx9 & ((Proj D) * R) . xx <> ((Proj D) * R) . xx9 ) ; :: thesis: contradiction
xx in the carrier of X by A2, Th35;
then R . xx = xx by A1;
then A3: (Proj D) . xx = ((Proj D) * R) . xx by FUNCT_2:15;
xx9 in the carrier of X by A2, Th35;
then A4: R . xx9 = xx9 by A1;
( (Proj (TrivExt D)) . xx = (Proj D) . xx & (Proj (TrivExt D)) . xx9 = (Proj D) . xx9 ) by A2, Th33, Th35;
hence contradiction by A2, A4, A3, FUNCT_2:15; :: thesis: verum
end;
then consider F being Function of the carrier of (space (TrivExt D)), the carrier of (space D) such that
A5: F * (Proj (TrivExt D)) = (Proj D) * R by EQREL_1:56;
reconsider F = F as Function of (space (TrivExt D)),(space D) ;
F is continuous
proof
let W be Point of (space (TrivExt D)); :: according to BORSUK_1:def 1 :: thesis: for G being a_neighborhood of F . W ex H being a_neighborhood of W st F .: H c= G
let G be a_neighborhood of F . W; :: thesis: ex H being a_neighborhood of W st F .: H c= G
reconsider GG = ((Proj D) * R) " G as a_neighborhood of (Proj (TrivExt D)) " {W} by A5, Th4, EQREL_1:57;
reconsider V9 = (Proj (TrivExt D)) .: GG as a_neighborhood of W by Th38;
take V = V9; :: thesis: F .: V c= G
F .: V = ((Proj D) * R) .: GG by A5, RELAT_1:126;
hence F .: V c= G by FUNCT_1:75; :: thesis: verum
end;
then reconsider F9 = F as continuous Function of (space (TrivExt D)),(space D) ;
take F9 ; :: according to BORSUK_1:def 17 :: thesis: F9 is being_a_retraction
let W be Point of (space (TrivExt D)); :: according to BORSUK_1:def 16 :: thesis: ( W in the carrier of (space D) implies F9 . W = W )
consider W9 being Point of XX such that
A6: (Proj (TrivExt D)) . W9 = W by Th29;
assume A7: W in the carrier of (space D) ; :: thesis: F9 . W = W
then W9 in the carrier of X by A6, Th36;
then A8: W9 = R . W9 by A1;
A9: F9 . W = (F * (Proj (TrivExt D))) . W9 by A6, FUNCT_2:15;
(Proj D) . W9 = (Proj (TrivExt D)) . W9 by A6, A7, Th33, Th36;
hence F9 . W = W by A5, A6, A8, A9, FUNCT_2:15; :: thesis: verum
end;