let T, S be non empty TopSpace; :: thesis: ( T is injective implies for f being Function of T,S st corestr f is being_homeomorphism holds
T is_Retract_of S )
assume A1:
T is injective
; :: thesis: for f being Function of T,S st corestr f is being_homeomorphism holds
T is_Retract_of S
A2:
( [#] S <> {} & [#] T <> {} )
;
let f be Function of T,S; :: thesis: ( corestr f is being_homeomorphism implies T is_Retract_of S )
assume A3:
corestr f is being_homeomorphism
; :: thesis: T is_Retract_of S
then A4:
corestr f is continuous
by TOPS_2:def 5;
consider g being Function of (Image f),T such that
A5:
g = (corestr f) "
;
g is continuous
by A3, A5, TOPS_2:def 5;
then consider h being Function of S,T such that
A6:
h is continuous
and
A7:
h | the carrier of (Image f) = g
by A1, Def5;
g is being_homeomorphism
by A3, A5, TOPS_2:70;
then A8:
g is one-to-one
by TOPS_2:def 5;
reconsider p = incl (Image f) as Function of (Image f),S ;
p is continuous
by TMAP_1:98;
then A9:
p * (corestr f) is continuous
by A4;
A10: dom (p * (corestr f)) =
the carrier of T
by FUNCT_2:def 1
.=
dom f
by FUNCT_2:def 1
;
take F = f * h; :: according to WAYBEL18:def 8 :: thesis: ( F is continuous & F * F = F & Image F,T are_homeomorphic )
A11:
the carrier of (Image f) = rng f
by Th10;
( dom h = the carrier of S & rng h c= the carrier of T )
by FUNCT_2:def 1;
then A12:
rng h c= dom f
by FUNCT_2:def 1;
A13:
for P being Subset of S holds f " P = (p * (corestr f)) " P
for P being Subset of S st P is open holds
F " P is open
hence
F is continuous
by A2, TOPS_2:55; :: thesis: ( F * F = F & Image F,T are_homeomorphic )
A19:
dom (h * f) = the carrier of T
by FUNCT_2:def 1;
for x being set st x in the carrier of T holds
(h * f) . x = x
proof
let x be
set ;
:: thesis: ( x in the carrier of T implies (h * f) . x = x )
assume A20:
x in the
carrier of
T
;
:: thesis: (h * f) . x = x
then A21:
x in dom f
by FUNCT_2:def 1;
A22:
x in dom (corestr f)
by A20, FUNCT_2:def 1;
A23:
corestr f is
one-to-one
by A3, TOPS_2:def 5;
A24:
rng (corestr f) = [#] (Image f)
by FUNCT_2:def 3;
A25:
f . x in rng f
by A21, FUNCT_1:def 5;
thus (h * f) . x =
h . (f . x)
by A21, FUNCT_1:23
.=
((corestr f) " ) . ((corestr f) . x)
by A5, A7, A11, A25, FUNCT_1:72
.=
((corestr f) " ) . ((corestr f) . x)
by A23, A24, TOPS_2:def 4
.=
x
by A22, A23, FUNCT_1:56
;
:: thesis: verum
end;
then A26:
h * f = id the carrier of T
by A19, FUNCT_1:34;
thus F * F =
((f * h) * f) * h
by RELAT_1:55
.=
(f * (id T)) * h
by A26, RELAT_1:55
.=
F
by FUNCT_2:23
; :: thesis: Image F,T are_homeomorphic
A27:
rng F c= rng f
set H = h * (incl (Image F));
A32:
dom (incl (Image F)) = the carrier of (Image F)
by FUNCT_2:def 1;
A33:
dom (h * (incl (Image F))) = [#] (Image F)
by FUNCT_2:def 1;
A34:
[#] (Image F) <> {}
;
A35:
rng (h * (incl (Image F))) = [#] T
proof
thus
rng (h * (incl (Image F))) c= [#] T
;
:: according to XBOOLE_0:def 10 :: thesis: [#] T c= rng (h * (incl (Image F)))
let y be
set ;
:: according to TARSKI:def 3 :: thesis: ( not y in [#] T or y in rng (h * (incl (Image F))) )
assume A36:
y in [#] T
;
:: thesis: y in rng (h * (incl (Image F)))
A37:
dom (h * (incl (Image F))) = rng F
by A33, Th10;
A38:
y in dom f
by A36, FUNCT_2:def 1;
then A39:
f . y in rng f
by FUNCT_1:def 5;
then
f . y in the
carrier of
S
;
then A40:
f . y in dom F
by FUNCT_2:def 1;
A41:
F . (f . y) =
((f * h) * f) . y
by A38, FUNCT_1:23
.=
(f * (id T)) . y
by A26, RELAT_1:55
.=
f . y
by FUNCT_2:23
;
then A42:
f . y in dom (h * (incl (Image F)))
by A37, A40, FUNCT_1:def 5;
reconsider pp =
f . y as
Point of
S by A39;
F . (f . y) in rng F
by A40, FUNCT_1:def 5;
then A43:
f . y in the
carrier of
(Image F)
by A41, Th10;
then A44:
y in dom ((incl (Image F)) * f)
by A32, A38, FUNCT_1:21;
(h * (incl (Image F))) . (f . y) =
((h * (incl (Image F))) * f) . y
by A38, FUNCT_1:23
.=
(h * ((incl (Image F)) * f)) . y
by RELAT_1:55
.=
h . (((incl (Image F)) * f) . y)
by A44, FUNCT_1:23
.=
h . ((incl (Image F)) . pp)
by A38, FUNCT_1:23
.=
h . (f . y)
by A43, TMAP_1:95
.=
(id T) . y
by A26, A38, FUNCT_1:23
.=
y
by A36, FUNCT_1:35
;
hence
y in rng (h * (incl (Image F)))
by A42, FUNCT_1:def 5;
:: thesis: verum
end;
A45:
h * (incl (Image F)) is one-to-one
proof
let x,
y be
Element of
(Image F);
:: according to WAYBEL_1:def 1 :: thesis: ( not (h * (incl (Image F))) . x = (h * (incl (Image F))) . y or x = y )
assume A46:
(h * (incl (Image F))) . x = (h * (incl (Image F))) . y
;
:: thesis: x = y
A47:
x in the
carrier of
(Image F)
;
then A48:
x in rng F
by Th10;
A49:
x in dom (incl (Image F))
by A47, FUNCT_2:def 1;
A50:
y in the
carrier of
(Image F)
;
then A51:
y in rng F
by Th10;
A52:
y in dom (incl (Image F))
by A50, FUNCT_2:def 1;
reconsider a =
x,
b =
y as
Point of
S by A48, A51;
reconsider x' =
x,
y' =
y as
Element of
(Image f) by A27, A48, A51, Th10;
g . x' =
h . x
by A7, FUNCT_1:72
.=
h . ((incl (Image F)) . a)
by TMAP_1:95
.=
(h * (incl (Image F))) . b
by A46, A49, FUNCT_1:23
.=
h . ((incl (Image F)) . b)
by A52, FUNCT_1:23
.=
h . y
by TMAP_1:95
.=
g . y'
by A7, FUNCT_1:72
;
hence
x = y
by A8, WAYBEL_1:def 1;
:: thesis: verum
end;
incl (Image F) is continuous
by TMAP_1:98;
then A53:
h * (incl (Image F)) is continuous
by A6;
for P being Subset of (Image F) st P is open holds
((h * (incl (Image F))) " ) " P is open
proof
let P be
Subset of
(Image F);
:: thesis: ( P is open implies ((h * (incl (Image F))) " ) " P is open )
assume
P is
open
;
:: thesis: ((h * (incl (Image F))) " ) " P is open
then
P in the
topology of
(Image F)
by PRE_TOPC:def 5;
then consider Q being
Subset of
S such that A54:
Q in the
topology of
S
and A55:
P = Q /\ ([#] (Image F))
by PRE_TOPC:def 9;
reconsider Q =
Q as
Subset of
S ;
A56:
Q is
open
by A54, PRE_TOPC:def 5;
p is
continuous
by TMAP_1:98;
then
p * (corestr f) is
continuous
by A4;
then
(p * (corestr f)) " Q is
open
by A2, A56, TOPS_2:55;
then A57:
f " Q is
open
by A13;
A58:
(incl (Image F)) .: P = P
A65:
f " Q = h .: P
proof
hereby :: according to TARSKI:def 3,
XBOOLE_0:def 10 :: thesis: h .: P c= f " Q
let x be
set ;
:: thesis: ( x in f " Q implies x in h .: P )assume A66:
x in f " Q
;
:: thesis: x in h .: Pthen A67:
x in dom f
by FUNCT_1:def 13;
A68:
f . x in Q
by A66, FUNCT_1:def 13;
f . x in rng f
by A67, FUNCT_1:def 5;
then A69:
f . x in the
carrier of
S
;
then A70:
f . x in dom h
by FUNCT_2:def 1;
A71:
f . x in dom F
by A69, FUNCT_2:def 1;
F . (f . x) =
f . (h . (f . x))
by A70, FUNCT_1:23
.=
f . ((id T) . x)
by A26, A67, FUNCT_1:23
.=
f . x
by A66, FUNCT_1:35
;
then
f . x in rng F
by A71, FUNCT_1:def 5;
then
f . x in the
carrier of
(Image F)
by Th10;
then A72:
f . x in P
by A55, A68, XBOOLE_0:def 4;
h . (f . x) =
(id T) . x
by A26, A67, FUNCT_1:23
.=
x
by A66, FUNCT_1:35
;
hence
x in h .: P
by A70, A72, FUNCT_1:def 12;
:: thesis: verum
end;
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in h .: P or x in f " Q )
assume
x in h .: P
;
:: thesis: x in f " Q
then consider y being
set such that A73:
y in dom h
and A74:
y in P
and A75:
x = h . y
by FUNCT_1:def 12;
A76:
x in rng h
by A73, A75, FUNCT_1:def 5;
A77:
y in Q
by A55, A74, XBOOLE_0:def 4;
y in the
carrier of
(Image F)
by A74;
then A78:
y in rng F
by Th10;
f . x in rng f
by A12, A76, FUNCT_1:def 5;
then reconsider a =
f . x,
b =
y as
Element of
(Image f) by A27, A78, Th10;
g . a =
h . (f . x)
by A7, FUNCT_1:72
.=
(id T) . x
by A12, A26, A76, FUNCT_1:23
.=
h . y
by A75, A76, FUNCT_1:35
.=
g . b
by A7, FUNCT_1:72
;
then
f . x in Q
by A8, A77, WAYBEL_1:def 1;
hence
x in f " Q
by A12, A76, FUNCT_1:def 13;
:: thesis: verum
end;
(h * (incl (Image F))) .: P = h .: P
by A58, RELAT_1:159;
hence
((h * (incl (Image F))) " ) " P is
open
by A35, A45, A57, A65, TOPS_2:67;
:: thesis: verum
end;
then
(h * (incl (Image F))) " is continuous
by A34, TOPS_2:55;
then
h * (incl (Image F)) is being_homeomorphism
by A33, A35, A45, A53, TOPS_2:def 5;
hence
Image F,T are_homeomorphic
by T_0TOPSP:def 1; :: thesis: verum