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