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