let S, T be non empty TopSpace; :: thesis: ( S is injective & S,T are_homeomorphic implies T is injective )
assume that
A1: S is injective and
A2: S,T are_homeomorphic ; :: thesis: T is injective
consider p being Function of S,T such that
A3: p is being_homeomorphism by A2;
let X be non empty TopSpace; :: according to WAYBEL18:def 5 :: thesis: for b1 being Element of bool [: the carrier of X, the carrier of T:] holds
( not b1 is continuous or for b2 being TopStruct holds
( not X is SubSpace of b2 or ex b3 being Element of bool [: the carrier of b2, the carrier of T:] st
( b3 is continuous & b3 | the carrier of X = b1 ) ) )
let f be Function of X,T; :: thesis: ( not f is continuous or for b1 being TopStruct holds
( not X is SubSpace of b1 or ex b2 being Element of bool [: the carrier of b1, the carrier of T:] st
( b2 is continuous & b2 | the carrier of X = f ) ) )
assume A4: f is continuous ; :: thesis: for b1 being TopStruct holds
( not X is SubSpace of b1 or ex b2 being Element of bool [: the carrier of b1, the carrier of T:] st
( b2 is continuous & b2 | the carrier of X = f ) )
let Y be non empty TopSpace; :: thesis: ( not X is SubSpace of Y or ex b1 being Element of bool [: the carrier of Y, the carrier of T:] st
( b1 is continuous & b1 | the carrier of X = f ) )
assume A5: X is SubSpace of Y ; :: thesis: ex b1 being Element of bool [: the carrier of Y, the carrier of T:] st
( b1 is continuous & b1 | the carrier of X = f )
then A6: [#] X c= [#] Y by PRE_TOPC:def 4;
A7: p is V7() by A3;
set F = (p ") * f;
p " is continuous by A3;
then consider G being Function of Y,S such that
A8: G is continuous and
A9: G | the carrier of X = (p ") * f by A1, A4, A5;
take g = p * G; :: thesis: ( g is continuous & g | the carrier of X = f )
A10: rng p = [#] T by A3;
A11: for x being object st x in dom f holds
g . x = f . x
proof
let x be object ; :: thesis: ( x in dom f implies g . x = f . x )
assume A12: x in dom f ; :: thesis: g . x = f . x
then A13: f . x in rng f by FUNCT_1:def 3;
then f . x in the carrier of T ;
then A14: f . x in dom (p ") by FUNCT_2:def 1;
x in the carrier of X by A12;
then x in the carrier of Y by A6;
then x in dom G by FUNCT_2:def 1;
hence g . x = p . (G . x) by FUNCT_1:13
.= p . (((p ") * f) . x) by A9, A12, FUNCT_1:49
.= p . ((p ") . (f . x)) by A12, FUNCT_1:13
.= (p * (p ")) . (f . x) by A14, FUNCT_1:13
.= (id the carrier of T) . (f . x) by A10, A7, TOPS_2:52
.= f . x by A13, FUNCT_1:17 ;
:: thesis: verum
end;
p is continuous by A3;
hence g is continuous by A8; :: thesis: g | the carrier of X = f
dom f = the carrier of X by FUNCT_2:def 1
.= the carrier of Y /\ the carrier of X by A6, XBOOLE_1:28
.= (dom g) /\ the carrier of X by FUNCT_2:def 1 ;
hence g | the carrier of X = f by A11, FUNCT_1:46; :: thesis: verum