thus ( X is_Retract_of Y implies ex c being continuous Function of X,Y ex r being continuous Function of Y,X st r * c = id X ) :: thesis: ( ex c being continuous Function of X,Y ex r being continuous Function of Y,X st r * c = id X implies X is_Retract_of Y )
proof
given f being Function of Y,Y such that A1: f is continuous and
A2: f * f = f and
A3: Image f,X are_homeomorphic ; :: according to WAYBEL18:def 8 :: thesis: ex c being continuous Function of X,Y ex r being continuous Function of Y,X st r * c = id X
consider h being Function of (Image f),X such that
A4: h is being_homeomorphism by A3;
A5: corestr f is continuous by A1, WAYBEL18:10;
h " is continuous by A4;
then reconsider c = (incl (Image f)) * (h ") as continuous Function of X,Y ;
h is continuous by A4;
then reconsider r = h * (corestr f) as continuous Function of Y,X by A5;
take c ; :: thesis: ex r being continuous Function of Y,X st r * c = id X
take r ; :: thesis: r * c = id X
A6: rng h = [#] X by A4;
A7: h is V7() by A4;
thus r * c = h * ((corestr f) * ((incl (Image f)) * (h "))) by RELAT_1:36
.= h * (((corestr f) * (incl (Image f))) * (h ")) by RELAT_1:36
.= h * ((id (Image f)) * (h ")) by A2, YELLOW14:35
.= h * (h ") by FUNCT_2:17
.= id X by A6, A7, TOPS_2:52 ; :: thesis: verum
end;
given c being continuous Function of X,Y, r being continuous Function of Y,X such that A8: r * c = id X ; :: thesis: X is_Retract_of Y
take f = c * r; :: according to WAYBEL18:def 8 :: thesis: ( f is continuous & f * f = f & Image f,X are_homeomorphic )
A9: dom c = the carrier of X by FUNCT_2:def 1
.= rng r by A8, FUNCT_2:18 ;
then reconsider cf = corestr c as Function of X,(Image f) by RELAT_1:28;
A10: Image f = Image c by A9, RELAT_1:28;
the carrier of (Image c) c= the carrier of Y by BORSUK_1:1;
then id (Image c) is Function of the carrier of (Image c), the carrier of Y by FUNCT_2:7;
then reconsider q = r * (id (Image c)) as Function of (Image f),X by A10;
A11: [#] X <> {} ;
A12: for P being Subset of X st P is open holds
q " P is open
proof
let P be Subset of X; :: thesis: ( P is open implies q " P is open )
A13: dom (id (Image c)) = [#] (Image c) ;
A14: (id (Image c)) " (r " P) = (r " P) /\ ([#] (Image c))
proof
thus (id (Image c)) " (r " P) c= (r " P) /\ ([#] (Image c)) :: according to XBOOLE_0:def 10 :: thesis: (r " P) /\ ([#] (Image c)) c= (id (Image c)) " (r " P)
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in (id (Image c)) " (r " P) or a in (r " P) /\ ([#] (Image c)) )
assume A15: a in (id (Image c)) " (r " P) ; :: thesis: a in (r " P) /\ ([#] (Image c))
then (id (Image c)) . a in r " P by FUNCT_1:def 7;
then a in r " P by A15, FUNCT_1:18;
hence a in (r " P) /\ ([#] (Image c)) by A15, XBOOLE_0:def 4; :: thesis: verum
end;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in (r " P) /\ ([#] (Image c)) or a in (id (Image c)) " (r " P) )
assume A16: a in (r " P) /\ ([#] (Image c)) ; :: thesis: a in (id (Image c)) " (r " P)
then a in r " P by XBOOLE_0:def 4;
then (id (Image c)) . a in r " P by A16, FUNCT_1:18;
hence a in (id (Image c)) " (r " P) by A13, A16, FUNCT_1:def 7; :: thesis: verum
end;
assume P is open ; :: thesis: q " P is open
then r " P is open by A11, TOPS_2:43;
then A17: r " P in the topology of Y ;
q " P = (id (Image c)) " (r " P) by RELAT_1:146;
hence q " P in the topology of (Image f) by A10, A17, A14, PRE_TOPC:def 4; :: according to PRE_TOPC:def 2 :: thesis: verum
end;
A18: r * (cf * (cf ")) = (id X) * (cf ") by A8, RELAT_1:36;
thus f is continuous ; :: thesis: ( f * f = f & Image f,X are_homeomorphic )
thus f * f = c * (r * (c * r)) by RELAT_1:36
.= c * ((id X) * r) by A8, RELAT_1:36
.= f by FUNCT_2:17 ; :: thesis: Image f,X are_homeomorphic
take h = cf " ; :: according to T_0TOPSP:def 1 :: thesis: h is being_homeomorphism
thus dom h = [#] (Image f) by FUNCT_2:def 1; :: according to TOPS_2:def 5 :: thesis: ( rng h = [#] X & h is one-to-one & h is continuous & h " is continuous )
A19: rng (corestr c) = [#] (Image c) by FUNCT_2:def 3;
A20: c is V7() by A8, FUNCT_2:23;
hence rng h = [#] X by A10, A19, TOPS_2:49; :: thesis: ( h is one-to-one & h is continuous & h " is continuous )
(corestr c) " is one-to-one by A20;
hence h is V7() by A10, A20, TOPS_2:def 4; :: thesis: ( h is continuous & h " is continuous )
corestr c is V7() by A8, FUNCT_2:23;
then r * (id the carrier of (Image c)) = (id X) * (cf ") by A10, A19, A18, TOPS_2:52;
then r * (id (Image c)) = cf " by FUNCT_2:17;
hence h is continuous by A11, A12, TOPS_2:43; :: thesis: h " is continuous
corestr c is continuous by WAYBEL18:10;
hence h " is continuous by A10, A19, A20, TOPS_2:51; :: thesis: verum