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 )
A2: incl (X,Y) = id X by A1, YELLOW_9:def 1;
set YY = Y | (rng (incl (X,Y)));
A3: [#] (Y | (rng (incl (X,Y)))) = rng (incl (X,Y)) by PRE_TOPC:def 5;
A4: ( [#] Y = {} implies [#] X = {} ) by A1;
then reconsider h = incl (X,Y) as Function of X,(Y | (rng (incl (X,Y)))) by A3, FUNCT_2:6;
set f = id X;
given Xy being Subset of Y such that A5: Xy = [#] X and
A6: the topology of (Y | Xy) = the topology of X ; :: thesis: incl (X,Y) is embedding
A7: 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 )
reconsider Q = P as Subset of (Y | (rng (incl (X,Y)))) by A2, A3;
assume P is open ; :: thesis: (h ") " P is open
then A8: P in the topology of X ;
(h ") " P = h .: Q by A2, A3, TOPS_2:54
.= Q by A2, FUNCT_1:92 ;
hence (h ") " P in the topology of (Y | (rng (incl (X,Y)))) by A5, A6, A2, A8; :: according to PRE_TOPC:def 2 :: thesis: verum
end;
A9: ( [#] X = {} implies [#] X = {} ) ;
A10: 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 )
reconsider Q = P as Subset of X by A2, A3;
assume P is open ; :: thesis: h " P is open
then P in the topology of (Y | (rng (incl (X,Y)))) ;
then Q in the topology of X by A5, A6, A2;
then Q is open ;
then (id X) " Q is open by A9, TOPS_2:43;
then (id X) " Q in the topology of X ;
hence h " P in the topology of X by A1, YELLOW_9:def 1; :: according to PRE_TOPC:def 2 :: thesis: verum
end;
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 A4, FUNCT_2:def 1, PRE_TOPC:def 5; :: 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 A2; :: thesis: ( h is continuous & h " is continuous )
( [#] (Y | (rng (incl (X,Y)))) = {} implies [#] X = {} ) by A2, A3;
hence h is continuous by A10, TOPS_2:43; :: thesis: h " is continuous
( [#] X = {} implies [#] (Y | (rng (incl (X,Y)))) = {} ) ;
hence h " is continuous by A7, TOPS_2:43; :: thesis: verum