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 )
( 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
;
WAYBEL18:def 8 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
;
ex r being continuous Function of Y,X st r * c = id X
take
r
;
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
;
verum
end;
given c being continuous Function of X,Y, r being continuous Function of Y,X such that A8:
r * c = id X
; X is_Retract_of Y
take f = c * r; WAYBEL18:def 8 ( 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
A18:
r * (cf * (cf ")) = (id X) * (cf ")
by A8, RELAT_1:36;
thus
f is continuous
; ( 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
; Image f,X are_homeomorphic
take h = cf " ; T_0TOPSP:def 1 h is being_homeomorphism
thus
dom h = [#] (Image f)
by FUNCT_2:def 1; TOPS_2:def 5 ( 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; ( 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; ( 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; h " is continuous
corestr c is continuous
by WAYBEL18:10;
hence
h " is continuous
by A10, A19, A20, TOPS_2:51; verum