let f be Function of (TOP-REAL 2),(TOP-REAL 2); ( f is continuous & f is one-to-one & rng f = [#] (TOP-REAL 2) & ( for p2 being Point of (TOP-REAL 2) ex K being non empty compact Subset of (TOP-REAL 2) st
( K = f .: K & ex V2 being Subset of (TOP-REAL 2) st
( p2 in V2 & V2 is open & V2 c= K & f . p2 in V2 ) ) ) implies f is being_homeomorphism )
assume that
A1:
( f is continuous & f is one-to-one )
and
A2:
rng f = [#] (TOP-REAL 2)
and
A3:
for p2 being Point of (TOP-REAL 2) ex K being non empty compact Subset of (TOP-REAL 2) st
( K = f .: K & ex V2 being Subset of (TOP-REAL 2) st
( p2 in V2 & V2 is open & V2 c= K & f . p2 in V2 ) )
; f is being_homeomorphism
reconsider g = f " as Function of (TOP-REAL 2),(TOP-REAL 2) by A1, A2, FUNCT_2:31;
A4:
dom f = the carrier of (TOP-REAL 2)
by FUNCT_2:def 1;
for p being Point of (TOP-REAL 2)
for V being Subset of (TOP-REAL 2) st g . p in V & V is open holds
ex W being Subset of (TOP-REAL 2) st
( p in W & W is open & g .: W c= V )
proof
let p be
Point of
(TOP-REAL 2);
for V being Subset of (TOP-REAL 2) st g . p in V & V is open holds
ex W being Subset of (TOP-REAL 2) st
( p in W & W is open & g .: W c= V )let V be
Subset of
(TOP-REAL 2);
( g . p in V & V is open implies ex W being Subset of (TOP-REAL 2) st
( p in W & W is open & g .: W c= V ) )
assume that A5:
g . p in V
and A6:
V is
open
;
ex W being Subset of (TOP-REAL 2) st
( p in W & W is open & g .: W c= V )
consider K being non
empty compact Subset of
(TOP-REAL 2) such that A7:
K = f .: K
and A8:
ex
V2 being
Subset of
(TOP-REAL 2) st
(
g . p in V2 &
V2 is
open &
V2 c= K &
f . (g . p) in V2 )
by A3;
consider V2 being
Subset of
(TOP-REAL 2) such that A9:
g . p in V2
and A10:
V2 is
open
and A11:
V2 c= K
and A12:
f . (g . p) in V2
by A8;
A13:
dom (f | K) =
(dom f) /\ K
by RELAT_1:90
.=
K
by A4, XBOOLE_1:28
;
A14:
g . p in V /\ V2
by A5, A9, XBOOLE_0:def 4;
the
carrier of
((TOP-REAL 2) | K) = K
by PRE_TOPC:29;
then reconsider R =
(V /\ V2) /\ K as
Subset of
((TOP-REAL 2) | K) by XBOOLE_1:17;
A15:
R = (V /\ V2) /\ ([#] ((TOP-REAL 2) | K))
by PRE_TOPC:def 10;
V /\ V2 is
open
by A6, A10, TOPS_1:38;
then A16:
R is
open
by A15, TOPS_2:32;
A17:
p in V2
by A1, A2, A12, FUNCT_1:57;
then reconsider q =
p as
Point of
((TOP-REAL 2) | K) by A11, PRE_TOPC:29;
A18:
rng (f | K) c= the
carrier of
(TOP-REAL 2)
;
dom (f | K) =
(dom f) /\ K
by RELAT_1:90
.=
the
carrier of
(TOP-REAL 2) /\ K
by FUNCT_2:def 1
.=
K
by XBOOLE_1:28
.=
the
carrier of
((TOP-REAL 2) | K)
by PRE_TOPC:29
;
then reconsider h =
f | K as
Function of
((TOP-REAL 2) | K),
(TOP-REAL 2) by A18, FUNCT_2:4;
A19:
h is
one-to-one
by A1, FUNCT_1:84;
A20:
K =
(f | K) .: K
by A7, RELAT_1:162
.=
rng (f | K)
by A13, RELAT_1:146
;
then consider f1 being
Function of
((TOP-REAL 2) | K),
((TOP-REAL 2) | K) such that A21:
h = f1
and A22:
f1 is
being_homeomorphism
by A1, A19, JGRAPH_1:64, TOPMETR:10;
A23:
rng f1 = [#] ((TOP-REAL 2) | K)
by A22, TOPS_2:def 5;
(
dom (f1 " ) = rng f1 &
rng (f1 " ) = dom f1 )
by A19, A21, FUNCT_1:55;
then reconsider g1 =
f1 " as
Function of
((TOP-REAL 2) | K),
((TOP-REAL 2) | K) by A23, FUNCT_2:4;
g1 = f1 "
by A19, A21, A23, TOPS_2:def 4;
then A24:
g1 is
continuous
by A22, TOPS_2:def 5;
A25:
f1 . (g . p) =
f . (g . p)
by A9, A11, A21, FUNCT_1:72
.=
p
by A1, A2, FUNCT_1:57
;
A26:
dom f1 =
(dom f) /\ K
by A21, RELAT_1:90
.=
K
by A4, XBOOLE_1:28
;
rng f1 = dom (f1 " )
by A19, A21, FUNCT_1:55;
then A27:
(f1 " ) . p in rng (f1 " )
by A11, A17, A20, A21, FUNCT_1:12;
A28:
rng (f1 " ) = dom f1
by A19, A21, FUNCT_1:55;
f1 . ((f1 " ) . p) = p
by A11, A17, A19, A20, A21, FUNCT_1:57;
then
(f1 " ) . p = g . p
by A8, A19, A21, A25, A26, A28, A27, FUNCT_1:def 8;
then
(f1 " ) . p in R
by A9, A11, A14, XBOOLE_0:def 4;
then consider W3 being
Subset of
((TOP-REAL 2) | K) such that A29:
q in W3
and A30:
W3 is
open
and A31:
(f1 " ) .: W3 c= R
by A16, A24, JGRAPH_2:20;
R = V /\ (V2 /\ K)
by XBOOLE_1:16;
then A32:
R c= V
by XBOOLE_1:17;
consider W5 being
Subset of
(TOP-REAL 2) such that A33:
W5 is
open
and A34:
W3 = W5 /\ ([#] ((TOP-REAL 2) | K))
by A30, TOPS_2:32;
reconsider W4 =
W5 /\ V2 as
Subset of
(TOP-REAL 2) ;
p in W5
by A29, A34, XBOOLE_0:def 4;
then A35:
p in W4
by A17, XBOOLE_0:def 4;
A36:
dom f1 = the
carrier of
((TOP-REAL 2) | K)
by FUNCT_2:def 1;
A37:
(f " ) .: W3 c= R
proof
let y be
set ;
TARSKI:def 3 ( not y in (f " ) .: W3 or y in R )
assume
y in (f " ) .: W3
;
y in R
then consider x being
set such that A38:
x in dom (f " )
and A39:
x in W3
and A40:
y = (f " ) . x
by FUNCT_1:def 12;
A41:
x in rng f
by A1, A38, FUNCT_1:55;
then A42:
y in dom f
by A1, A40, FUNCT_1:54;
A43:
f . y = x
by A1, A40, A41, FUNCT_1:54;
the
carrier of
((TOP-REAL 2) | K) = K
by PRE_TOPC:29;
then
ex
z2 being
set st
(
z2 in dom f &
z2 in K &
f . y = f . z2 )
by A7, A39, A43, FUNCT_1:def 12;
then A44:
y in K
by A1, A42, FUNCT_1:def 8;
then A45:
y in the
carrier of
((TOP-REAL 2) | K)
by PRE_TOPC:29;
A46:
dom (f1 " ) = the
carrier of
((TOP-REAL 2) | K)
by A19, A21, A23, FUNCT_1:55;
f1 . y = x
by A21, A43, A44, FUNCT_1:72;
then
y = (f1 " ) . x
by A19, A21, A36, A45, FUNCT_1:54;
then
y in (f1 " ) .: W3
by A39, A46, FUNCT_1:def 12;
hence
y in R
by A31;
verum
end;
W4 =
W5 /\ (V2 /\ K)
by A11, XBOOLE_1:28
.=
(W5 /\ K) /\ V2
by XBOOLE_1:16
.=
W3 /\ V2
by A34, PRE_TOPC:def 10
;
then A47:
g .: W4 c= (g .: W3) /\ (g .: V2)
by RELAT_1:154;
(g .: W3) /\ (g .: V2) c= g .: W3
by XBOOLE_1:17;
then
g .: W4 c= g .: W3
by A47, XBOOLE_1:1;
then A48:
g .: W4 c= R
by A37, XBOOLE_1:1;
W4 is
open
by A10, A33, TOPS_1:38;
hence
ex
W being
Subset of
(TOP-REAL 2) st
(
p in W &
W is
open &
g .: W c= V )
by A35, A48, A32, XBOOLE_1:1;
verum
end;
then A49:
g is continuous
by JGRAPH_2:20;
g = f "
by A1, A2, TOPS_2:def 4;
hence
f is being_homeomorphism
by A1, A2, A4, A49, TOPS_2:def 5; verum