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:25;
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:61
.=
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:8;
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 5;
V /\ V2 is
open
by A6, A10, TOPS_1:11;
then A16:
R is
open
by A15, TOPS_2:24;
A17:
p in V2
by A1, A2, A12, FUNCT_1:35;
then reconsider q =
p as
Point of
((TOP-REAL 2) | K) by A11, PRE_TOPC:8;
A18:
rng (f | K) c= the
carrier of
(TOP-REAL 2)
;
dom (f | K) =
(dom f) /\ K
by RELAT_1:61
.=
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:8
;
then reconsider h =
f | K as
Function of
((TOP-REAL 2) | K),
(TOP-REAL 2) by A18, FUNCT_2:2;
A19:
h is
one-to-one
by A1, FUNCT_1:52;
A20:
K =
(f | K) .: K
by A7, RELAT_1:129
.=
rng (f | K)
by A13, RELAT_1:113
;
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:46, TOPMETR:7;
A23:
rng f1 = [#] ((TOP-REAL 2) | K)
by A22, TOPS_2:def 5;
A24:
f1 is
onto
by A23, FUNCT_2:def 3;
(
dom (f1 ") = rng f1 &
rng (f1 ") = dom f1 )
by A19, A21, FUNCT_1:33;
then reconsider g1 =
f1 " as
Function of
((TOP-REAL 2) | K),
((TOP-REAL 2) | K) by A23, FUNCT_2:2;
g1 = f1 "
by A19, A21, A24, TOPS_2:def 4;
then A25:
g1 is
continuous
by A22, TOPS_2:def 5;
A26:
f1 . (g . p) =
f . (g . p)
by A9, A11, A21, FUNCT_1:49
.=
p
by A1, A2, FUNCT_1:35
;
A27:
dom f1 =
(dom f) /\ K
by A21, RELAT_1:61
.=
K
by A4, XBOOLE_1:28
;
rng f1 = dom (f1 ")
by A19, A21, FUNCT_1:33;
then A28:
(f1 ") . p in rng (f1 ")
by A11, A17, A20, A21, FUNCT_1:3;
A29:
rng (f1 ") = dom f1
by A19, A21, FUNCT_1:33;
f1 . ((f1 ") . p) = p
by A11, A17, A19, A20, A21, FUNCT_1:35;
then
(f1 ") . p = g . p
by A8, A19, A21, A26, A27, A29, A28, FUNCT_1:def 4;
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 A30:
q in W3
and A31:
W3 is
open
and A32:
(f1 ") .: W3 c= R
by A16, A25, JGRAPH_2:10;
R = V /\ (V2 /\ K)
by XBOOLE_1:16;
then A33:
R c= V
by XBOOLE_1:17;
consider W5 being
Subset of
(TOP-REAL 2) such that A34:
W5 is
open
and A35:
W3 = W5 /\ ([#] ((TOP-REAL 2) | K))
by A31, TOPS_2:24;
reconsider W4 =
W5 /\ V2 as
Subset of
(TOP-REAL 2) ;
p in W5
by A30, A35, XBOOLE_0:def 4;
then A36:
p in W4
by A17, XBOOLE_0:def 4;
A37:
dom f1 = the
carrier of
((TOP-REAL 2) | K)
by FUNCT_2:def 1;
A38:
(f ") .: W3 c= R
proof
let y be
object ;
TARSKI:def 3 ( not y in (f ") .: W3 or y in R )
assume
y in (f ") .: W3
;
y in R
then consider x being
object such that A39:
x in dom (f ")
and A40:
x in W3
and A41:
y = (f ") . x
by FUNCT_1:def 6;
A42:
x in rng f
by A1, A39, FUNCT_1:33;
then A43:
y in dom f
by A1, A41, FUNCT_1:32;
A44:
f . y = x
by A1, A41, A42, FUNCT_1:32;
the
carrier of
((TOP-REAL 2) | K) = K
by PRE_TOPC:8;
then
ex
z2 being
object st
(
z2 in dom f &
z2 in K &
f . y = f . z2 )
by A7, A40, A44, FUNCT_1:def 6;
then A45:
y in K
by A1, A43, FUNCT_1:def 4;
then A46:
y in the
carrier of
((TOP-REAL 2) | K)
by PRE_TOPC:8;
A47:
dom (f1 ") = the
carrier of
((TOP-REAL 2) | K)
by A19, A21, A23, FUNCT_1:33;
f1 . y = x
by A21, A44, A45, FUNCT_1:49;
then
y = (f1 ") . x
by A19, A21, A37, A46, FUNCT_1:32;
then
y in (f1 ") .: W3
by A40, A47, FUNCT_1:def 6;
hence
y in R
by A32;
verum
end;
W4 =
W5 /\ (V2 /\ K)
by A11, XBOOLE_1:28
.=
(W5 /\ K) /\ V2
by XBOOLE_1:16
.=
W3 /\ V2
by A35, PRE_TOPC:def 5
;
then A48:
g .: W4 c= (g .: W3) /\ (g .: V2)
by RELAT_1:121;
(g .: W3) /\ (g .: V2) c= g .: W3
by XBOOLE_1:17;
then
g .: W4 c= g .: W3
by A48;
then A49:
g .: W4 c= R
by A38;
W4 is
open
by A10, A34, TOPS_1:11;
hence
ex
W being
Subset of
(TOP-REAL 2) st
(
p in W &
W is
open &
g .: W c= V )
by A36, A49, A33, XBOOLE_1:1;
verum
end;
then A50:
g is continuous
by JGRAPH_2:10;
f is onto
by A2, FUNCT_2:def 3;
then
g = f "
by A1, TOPS_2:def 4;
hence
f is being_homeomorphism
by A1, A2, A4, A50, TOPS_2:def 5; verum