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 )
( the carrier of (Y | P) = P & dom f = the carrier of X ) by FUNCT_2:def 1, PRE_TOPC:8;
then reconsider f2 = f as Function of X,(Y | P) by A4, FUNCT_2:1;
A5: ( dom f2 = [#] X & f2 is continuous ) by A3, Th44, FUNCT_2:def 1;
( rng f2 = [#] (Y | P) & Y | P is T_2 ) by A2, A4, PRE_TOPC:def 5, TOPMETR:2;
hence ex f1 being Function of X,(Y | P) st
( f = f1 & f1 is being_homeomorphism ) by A1, A3, A5, COMPTS_1:17; :: thesis: verum