let X, Y be TopSpace; :: thesis: ( [#] X c= [#] Y & ex Xy being Subset of Y st
( Xy = [#] X & the topology of (Y | Xy) = the topology of X ) implies incl X,Y is embedding )
assume A1:
[#] X c= [#] Y
; :: thesis: ( for Xy being Subset of Y holds
( not Xy = [#] X or not the topology of (Y | Xy) = the topology of X ) or incl X,Y is embedding )
given Xy being Subset of Y such that A2:
Xy = [#] X
and
A3:
the topology of (Y | Xy) = the topology of X
; :: thesis: incl X,Y is embedding
A4:
incl X,Y = id X
by A1, YELLOW_9:def 1;
A5:
( [#] Y = {} implies [#] X = {} )
by A1, XBOOLE_1:3;
set YY = Y | (rng (incl X,Y));
A6:
[#] (Y | (rng (incl X,Y))) = rng (incl X,Y)
by PRE_TOPC:def 10;
then reconsider h = incl X,Y as Function of X,(Y | (rng (incl X,Y))) by A5, FUNCT_2:8;
take
h
; :: according to COMPACT1:def 7 :: thesis: ( h = incl X,Y & h is being_homeomorphism )
thus
h = incl X,Y
; :: thesis: h is being_homeomorphism
thus
( dom h = [#] X & rng h = [#] (Y | (rng (incl X,Y))) )
by A5, FUNCT_2:def 1, PRE_TOPC:def 10; :: according to TOPS_2:def 5 :: thesis: ( h is one-to-one & h is continuous & h " is continuous )
thus
h is one-to-one
by A4; :: thesis: ( h is continuous & h " is continuous )
A7:
( [#] (Y | (rng (incl X,Y))) = {} implies [#] X = {} )
by A4, A6, RELAT_1:71;
set f = id X;
A8:
( [#] X = {} implies [#] X = {} )
;
for P being Subset of (Y | (rng (incl X,Y))) st P is open holds
h " P is open
proof
let P be
Subset of
(Y | (rng (incl X,Y)));
:: thesis: ( P is open implies h " P is open )
assume
P is
open
;
:: thesis: h " P is open
then A9:
P in the
topology of
(Y | (rng (incl X,Y)))
by PRE_TOPC:def 5;
reconsider Q =
P as
Subset of
X by A4, A6, RELAT_1:71;
Q in the
topology of
X
by A2, A3, A4, A9, RELAT_1:71;
then
Q is
open
by PRE_TOPC:def 5;
then
(id X) " Q is
open
by A8, TOPS_2:55;
then
(id X) " Q in the
topology of
X
by PRE_TOPC:def 5;
hence
h " P in the
topology of
X
by A1, YELLOW_9:def 1;
:: according to PRE_TOPC:def 5 :: thesis: verum
end;
hence
h is continuous
by A7, TOPS_2:55; :: thesis: h " is continuous
A10:
( [#] X = {} implies [#] (Y | (rng (incl X,Y))) = {} )
by A4, A6, RELAT_1:71;
for P being Subset of X st P is open holds
(h " ) " P is open
proof
let P be
Subset of
X;
:: thesis: ( P is open implies (h " ) " P is open )
assume
P is
open
;
:: thesis: (h " ) " P is open
then A11:
P in the
topology of
X
by PRE_TOPC:def 5;
reconsider Q =
P as
Subset of
(Y | (rng (incl X,Y))) by A4, A6, RELAT_1:71;
(h " ) " P =
h .: Q
by A4, A6, TOPS_2:67
.=
Q
by A4, FUNCT_1:162
;
hence
(h " ) " P in the
topology of
(Y | (rng (incl X,Y)))
by A2, A3, A4, A11, RELAT_1:71;
:: according to PRE_TOPC:def 5 :: thesis: verum
end;
hence
h " is continuous
by A10, TOPS_2:55; :: thesis: verum