let X, Y be non empty TopSpace; :: thesis: for f being Function of X,Y
for P being non empty Subset of Y st X is compact & Y is T_2 & f is continuous & f is one-to-one & P = rng f holds
ex f1 being Function of X,(Y | P) st
( f = f1 & f1 is being_homeomorphism )
let f be Function of X,Y; :: thesis: for P being non empty Subset of Y st X is compact & Y is T_2 & f is continuous & f is one-to-one & P = rng f holds
ex f1 being Function of X,(Y | P) st
( f = f1 & f1 is being_homeomorphism )
let P be non empty Subset of Y; :: thesis: ( X is compact & Y is T_2 & f is continuous & f is one-to-one & P = rng f implies ex f1 being Function of X,(Y | P) st
( f = f1 & f1 is being_homeomorphism ) )
assume that
A1: X is compact and
A2: Y is T_2 and
A3: ( f is continuous & f is one-to-one ) and
A4: P = rng f ; :: thesis: ex f1 being Function of X,(Y | P) st
( f = f1 & f1 is being_homeomorphism )
A5: the carrier of (Y | P) = P by PRE_TOPC:29;
A6: dom f = the carrier of X by FUNCT_2:def 1;
then reconsider f2 = f as Function of X,(Y | P) by A4, A5, FUNCT_2:3;
A7: dom f2 = [#] X by A6;
A8: rng f2 = [#] (Y | P) by A4, PRE_TOPC:def 10;
A9: Y | P is T_2 by A2, TOPMETR:3;
f2 is continuous by A3, Th63;
hence ex f1 being Function of X,(Y | P) st
( f = f1 & f1 is being_homeomorphism ) by A1, A3, A7, A8, A9, COMPTS_1:26; :: thesis: verum