let T, S be non empty TopSpace; ( 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
; for f being Function of T,S st corestr f is being_homeomorphism holds
T is_Retract_of S
let f be Function of T,S; ( corestr f is being_homeomorphism implies T is_Retract_of S )
consider g being Function of (Image f),T such that
A2:
g = (corestr f) "
;
assume A3:
corestr f is being_homeomorphism
; T is_Retract_of S
then
g is continuous
by A2, TOPS_2:def 5;
then consider h being Function of S,T such that
A4:
h is continuous
and
A5:
h | the carrier of (Image f) = g
by A1, Def5;
g is being_homeomorphism
by A3, A2, TOPS_2:56;
then A6:
g is one-to-one
by TOPS_2:def 5;
A7:
the carrier of (Image f) = rng f
by Th10;
A8:
for x being set st x in the carrier of T holds
(h * f) . x = x
proof
let x be
set ;
( x in the carrier of T implies (h * f) . x = x )
assume A10:
x in the
carrier of
T
;
(h * f) . x = x
then A11:
x in dom (corestr f)
by FUNCT_2:def 1;
A12:
x in dom f
by A10, FUNCT_2:def 1;
then A13:
f . x in rng f
by FUNCT_1:def 3;
A14:
corestr f is
one-to-one
by A3, TOPS_2:def 5;
thus (h * f) . x =
h . (f . x)
by A12, FUNCT_1:13
.=
((corestr f) ") . ((corestr f) . x)
by A2, A5, A7, A13, FUNCT_1:49
.=
((corestr f) ") . ((corestr f) . x)
by A14, TOPS_2:def 4
.=
x
by A11, A14, FUNCT_1:34
;
verum
end;
dom (h * f) = the carrier of T
by FUNCT_2:def 1;
then A15:
h * f = id the carrier of T
by A8, FUNCT_1:17;
take F = f * h; WAYBEL18:def 8 ( F is continuous & F * F = F & Image F,T are_homeomorphic )
set H = h * (incl (Image F));
A16:
dom (h * (incl (Image F))) = [#] (Image F)
by FUNCT_2:def 1;
rng h c= the carrier of T
;
then A17:
rng h c= dom f
by FUNCT_2:def 1;
A18:
rng F c= rng f
A23:
h * (incl (Image F)) is one-to-one
proof
let x,
y be
Element of
(Image F);
WAYBEL_1:def 1 ( not (h * (incl (Image F))) . x = (h * (incl (Image F))) . y or x = y )
assume A24:
(h * (incl (Image F))) . x = (h * (incl (Image F))) . y
;
x = y
A25:
x in the
carrier of
(Image F)
;
then A26:
x in dom (incl (Image F))
by FUNCT_2:def 1;
A27:
y in the
carrier of
(Image F)
;
then A28:
y in dom (incl (Image F))
by FUNCT_2:def 1;
A29:
y in rng F
by A27, Th10;
A30:
x in rng F
by A25, Th10;
then reconsider a =
x,
b =
y as
Point of
S by A29;
reconsider x9 =
x,
y9 =
y as
Element of
(Image f) by A18, A30, A29, Th10;
g . x9 =
h . x
by A5, FUNCT_1:49
.=
h . ((incl (Image F)) . a)
by TMAP_1:84
.=
(h * (incl (Image F))) . b
by A24, A26, FUNCT_1:13
.=
h . ((incl (Image F)) . b)
by A28, FUNCT_1:13
.=
h . y
by TMAP_1:84
.=
g . y9
by A5, FUNCT_1:49
;
hence
x = y
by A6, WAYBEL_1:def 1;
verum
end;
A31:
dom (incl (Image F)) = the carrier of (Image F)
by FUNCT_2:def 1;
A32:
rng (h * (incl (Image F))) = [#] T
proof
thus
rng (h * (incl (Image F))) c= [#] T
;
XBOOLE_0:def 10 [#] T c= rng (h * (incl (Image F)))
let y be
set ;
TARSKI:def 3 ( not y in [#] T or y in rng (h * (incl (Image F))) )
assume A33:
y in [#] T
;
y in rng (h * (incl (Image F)))
then A34:
y in dom f
by FUNCT_2:def 1;
then A35:
F . (f . y) =
((f * h) * f) . y
by FUNCT_1:13
.=
(f * (id T)) . y
by A15, RELAT_1:36
.=
f . y
by FUNCT_2:17
;
A36:
f . y in rng f
by A34, FUNCT_1:def 3;
then reconsider pp =
f . y as
Point of
S ;
f . y in the
carrier of
S
by A36;
then A37:
f . y in dom F
by FUNCT_2:def 1;
then
F . (f . y) in rng F
by FUNCT_1:def 3;
then A38:
f . y in the
carrier of
(Image F)
by A35, Th10;
then A39:
y in dom ((incl (Image F)) * f)
by A31, A34, FUNCT_1:11;
dom (h * (incl (Image F))) = rng F
by A16, Th10;
then A40:
f . y in dom (h * (incl (Image F)))
by A37, A35, FUNCT_1:def 3;
(h * (incl (Image F))) . (f . y) =
((h * (incl (Image F))) * f) . y
by A34, FUNCT_1:13
.=
(h * ((incl (Image F)) * f)) . y
by RELAT_1:36
.=
h . (((incl (Image F)) * f) . y)
by A39, FUNCT_1:13
.=
h . ((incl (Image F)) . pp)
by A34, FUNCT_1:13
.=
h . (f . y)
by A38, TMAP_1:84
.=
(id T) . y
by A15, A34, FUNCT_1:13
.=
y
by A33, FUNCT_1:18
;
hence
y in rng (h * (incl (Image F)))
by A40, FUNCT_1:def 3;
verum
end;
reconsider p = incl (Image f) as Function of (Image f),S ;
A41:
[#] S <> {}
;
A42: dom (p * (corestr f)) =
the carrier of T
by FUNCT_2:def 1
.=
dom f
by FUNCT_2:def 1
;
A43:
for P being Subset of S holds f " P = (p * (corestr f)) " P
A53:
corestr f is continuous
by A3, TOPS_2:def 5;
A54:
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);
( P is open implies ((h * (incl (Image F))) ") " P is open )
A55:
p is
continuous
by TMAP_1:87;
(incl (Image F)) .: P = P
then A61:
(h * (incl (Image F))) .: P = h .: P
by RELAT_1:126;
assume
P is
open
;
((h * (incl (Image F))) ") " P is open
then
P in the
topology of
(Image F)
by PRE_TOPC:def 2;
then consider Q being
Subset of
S such that A62:
Q in the
topology of
S
and A63:
P = Q /\ ([#] (Image F))
by PRE_TOPC:def 4;
reconsider Q =
Q as
Subset of
S ;
A64:
f " Q = h .: P
proof
hereby TARSKI:def 3,
XBOOLE_0:def 10 h .: P c= f " Q
let x be
set ;
( x in f " Q implies x in h .: P )assume A65:
x in f " Q
;
x in h .: Pthen A66:
x in dom f
by FUNCT_1:def 7;
then A67:
h . (f . x) =
(id T) . x
by A15, FUNCT_1:13
.=
x
by A65, FUNCT_1:18
;
f . x in rng f
by A66, FUNCT_1:def 3;
then A68:
f . x in the
carrier of
S
;
then A69:
f . x in dom h
by FUNCT_2:def 1;
A70:
f . x in dom F
by A68, FUNCT_2:def 1;
F . (f . x) =
f . (h . (f . x))
by A69, FUNCT_1:13
.=
f . ((id T) . x)
by A15, A66, FUNCT_1:13
.=
f . x
by A65, FUNCT_1:18
;
then
f . x in rng F
by A70, FUNCT_1:def 3;
then A71:
f . x in the
carrier of
(Image F)
by Th10;
f . x in Q
by A65, FUNCT_1:def 7;
then
f . x in P
by A63, A71, XBOOLE_0:def 4;
hence
x in h .: P
by A69, A67, FUNCT_1:def 6;
verum
end;
let x be
set ;
TARSKI:def 3 ( not x in h .: P or x in f " Q )
assume
x in h .: P
;
x in f " Q
then consider y being
set such that A72:
y in dom h
and A73:
y in P
and A74:
x = h . y
by FUNCT_1:def 6;
A75:
y in Q
by A63, A73, XBOOLE_0:def 4;
y in the
carrier of
(Image F)
by A73;
then A76:
y in rng F
by Th10;
A77:
x in rng h
by A72, A74, FUNCT_1:def 3;
then
f . x in rng f
by A17, FUNCT_1:def 3;
then reconsider a =
f . x,
b =
y as
Element of
(Image f) by A18, A76, Th10;
g . a =
h . (f . x)
by A5, FUNCT_1:49
.=
(id T) . x
by A17, A15, A77, FUNCT_1:13
.=
h . y
by A74, A77, FUNCT_1:18
.=
g . b
by A5, FUNCT_1:49
;
then
f . x in Q
by A6, A75, WAYBEL_1:def 1;
hence
x in f " Q
by A17, A77, FUNCT_1:def 7;
verum
end;
Q is
open
by A62, PRE_TOPC:def 2;
then
(p * (corestr f)) " Q is
open
by A41, A53, A55, TOPS_2:43;
then
f " Q is
open
by A43;
hence
((h * (incl (Image F))) ") " P is
open
by A32, A23, A64, A61, TOPS_2:54;
verum
end;
A78:
p is continuous
by TMAP_1:87;
A79:
[#] T <> {}
;
for P being Subset of S st P is open holds
F " P is open
hence
F is continuous
by A41, TOPS_2:43; ( F * F = F & Image F,T are_homeomorphic )
thus F * F =
((f * h) * f) * h
by RELAT_1:36
.=
(f * (id T)) * h
by A15, RELAT_1:36
.=
F
by FUNCT_2:17
; Image F,T are_homeomorphic
[#] (Image F) <> {}
;
then
( incl (Image F) is continuous & (h * (incl (Image F))) " is continuous )
by A54, TMAP_1:87, TOPS_2:43;
then
h * (incl (Image F)) is being_homeomorphism
by A4, A16, A32, A23, TOPS_2:def 5;
hence
Image F,T are_homeomorphic
by T_0TOPSP:def 1; verum