let n be Nat; 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); 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); ( 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
; 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
; ( f = g & f is being_homeomorphism )
thus
f = g
; 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
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; verum