let X, Y be non empty TopSpace; 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; 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; ( 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
; 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; verum