let n be Nat; :: thesis: for P being non empty Subset of (TOP-REAL n)
for g being Function of I[01],(TOP-REAL n) st g is continuous & g is one-to-one & rng g = P holds
ex f being Function of I[01],((TOP-REAL n) | P) st
( f = g & f is being_homeomorphism )
let P be non empty Subset of (TOP-REAL n); :: thesis: for g being Function of I[01],(TOP-REAL n) st g is continuous & g is one-to-one & rng g = P holds
ex f being Function of I[01],((TOP-REAL n) | P) st
( f = g & f is being_homeomorphism )
let g be Function of I[01],(TOP-REAL n); :: thesis: ( g is continuous & g is one-to-one & rng g = P implies ex f being Function of I[01],((TOP-REAL n) | P) st
( f = g & f is being_homeomorphism ) )
assume that
A1: ( g is continuous & g is one-to-one ) and
A2: rng g = P ; :: thesis: ex f being Function of I[01],((TOP-REAL n) | P) st
( f = g & f is being_homeomorphism )
the carrier of ((TOP-REAL n) | P) = [#] ((TOP-REAL n) | P) ;
then A3: the carrier of ((TOP-REAL n) | P) = P by PRE_TOPC:def 5;
then reconsider f = g as Function of I[01],((TOP-REAL n) | P) by A2, FUNCT_2:6;
take f ; :: thesis: ( f = g & f is being_homeomorphism )
thus f = g ; :: thesis: f is being_homeomorphism
A4: [#] ((TOP-REAL n) | P) = P by PRE_TOPC:def 5;
A5: dom f = the carrier of I[01] by FUNCT_2:def 1
.= [#] I[01] ;
A6: [#] (TOP-REAL n) <> {} ;
for P2 being Subset of ((TOP-REAL n) | P) st P2 is open holds
f " P2 is open
proof
let P2 be Subset of ((TOP-REAL n) | P); :: thesis: ( P2 is open implies f " P2 is open )
assume P2 is open ; :: thesis: f " P2 is open
then consider C being Subset of (TOP-REAL n) such that
A7: C is open and
A8: C /\ ([#] ((TOP-REAL n) | P)) = P2 by TOPS_2:24;
g " P = [#] I[01] by A3, A5, RELSET_1:22;
then f " P2 = (f " C) /\ ([#] I[01]) by A4, A8, FUNCT_1:68
.= f " C by XBOOLE_1:28 ;
hence f " P2 is open by A1, A6, A7, TOPS_2:43; :: thesis: verum
end;
then A9: f is continuous by A4, TOPS_2:43;
rng f = [#] ((TOP-REAL n) | P) by A2, PRE_TOPC:def 5;
hence f is being_homeomorphism by A1, A9, COMPTS_1:17; :: thesis: verum