let f be Function of [:R^1 ,R^1 :],(TOP-REAL 2); :: thesis: ( ( for x, y being Real holds f . [x,y] = <*x,y*> ) implies f is being_homeomorphism )
assume A1:
for x, y being Real holds f . [x,y] = <*x,y*>
; :: thesis: f is being_homeomorphism
A2:
the carrier of [:R^1 ,R^1 :] = [:the carrier of R^1 ,the carrier of R^1 :]
by BORSUK_1:def 5;
then A3:
dom f = [:the carrier of R^1 ,the carrier of R^1 :]
by FUNCT_2:def 1;
thus
dom f = [#] [:R^1 ,R^1 :]
by FUNCT_2:def 1; :: according to TOPS_2:def 5 :: thesis: ( rng f = [#] (TOP-REAL 2) & f is one-to-one & f is continuous & f /" is continuous )
thus A4:
rng f = [#] (TOP-REAL 2)
:: thesis: ( f is one-to-one & f is continuous & f /" is continuous )
thus A7:
f is one-to-one
:: thesis: ( f is continuous & f /" is continuous )proof
let x,
y be
set ;
:: according to FUNCT_1:def 8 :: thesis: ( not x in proj1 f or not y in proj1 f or not f . x = f . y or x = y )
assume
x in dom f
;
:: thesis: ( not y in proj1 f or not f . x = f . y or x = y )
then consider x1,
x2 being
set such that A8:
(
x1 in REAL &
x2 in REAL )
and A9:
x = [x1,x2]
by A2, TOPMETR:24, ZFMISC_1:def 2;
assume
y in dom f
;
:: thesis: ( not f . x = f . y or x = y )
then consider y1,
y2 being
set such that A10:
(
y1 in REAL &
y2 in REAL )
and A11:
y = [y1,y2]
by A2, TOPMETR:24, ZFMISC_1:def 2;
reconsider x1 =
x1,
x2 =
x2,
y1 =
y1,
y2 =
y2 as
Real by A8, A10;
A12:
(
f . [x1,x2] = <*x1,x2*> &
f . [y1,y2] = <*y1,y2*> )
by A1;
assume
f . x = f . y
;
:: thesis: x = y
then
(
x1 = y1 &
x2 = y2 )
by A9, A11, A12, GROUP_7:2;
hence
x = y
by A9, A11;
:: thesis: verum
end;
thus
f is continuous
:: thesis: f /" is continuous proof
let w be
Point of
[:R^1 ,R^1 :];
:: according to BORSUK_1:def 3 :: thesis: for b1 being a_neighborhood of f . w ex b2 being a_neighborhood of w st f .: b2 c= b1let G be
a_neighborhood of
f . w;
:: thesis: ex b1 being a_neighborhood of w st f .: b1 c= G
consider x,
y being
set such that A13:
(
x in the
carrier of
R^1 &
y in the
carrier of
R^1 )
and A14:
w = [x,y]
by A2, ZFMISC_1:def 2;
reconsider x =
x,
y =
y as
Real by A13, TOPMETR:24;
reconsider fw =
f . w as
Point of
(Euclid 2) by TOPREAL3:13;
fw in Int G
by CONNSP_2:def 1;
then consider r being
real number such that A15:
r > 0
and A16:
Ball fw,
r c= G
by GOBOARD6:8;
reconsider r =
r as
Real by XREAL_0:def 1;
set A =
].(((f . w) `1 ) - (r / (sqrt 2))),(((f . w) `1 ) + (r / (sqrt 2))).[;
set B =
].(((f . w) `2 ) - (r / (sqrt 2))),(((f . w) `2 ) + (r / (sqrt 2))).[;
reconsider A =
].(((f . w) `1 ) - (r / (sqrt 2))),(((f . w) `1 ) + (r / (sqrt 2))).[,
B =
].(((f . w) `2 ) - (r / (sqrt 2))),(((f . w) `2 ) + (r / (sqrt 2))).[ as
Subset of
R^1 by TOPMETR:24;
take
[:A,B:]
;
:: thesis: ( [:A,B:] is a_neighborhood of w & f .: [:A,B:] c= G )
thus
[:A,B:] is
a_neighborhood of
w
:: thesis: f .: [:A,B:] c= Gproof
(
A is
open &
B is
open )
by JORDAN6:46;
then A17:
[:A,B:] in Base-Appr [:A,B:]
;
A18:
r / (sqrt 2) > 0
by A15, SQUARE_1:84, XREAL_1:141;
f . [x,y] = <*x,y*>
by A1;
then
(
x = (f . w) `1 &
y = (f . w) `2 )
by A14, EUCLID:56;
then
(
x in A &
y in B )
by A18, Th20;
then
w in [:A,B:]
by A14, ZFMISC_1:106;
then
w in union (Base-Appr [:A,B:])
by A17, TARSKI:def 4;
hence
w in Int [:A,B:]
by BORSUK_1:55;
:: according to CONNSP_2:def 1 :: thesis: verum
end;
product (1,2 --> A,B) c= Ball fw,
r
by Th49;
then
f .: [:A,B:] c= Ball fw,
r
by A1, Th84;
hence
f .: [:A,B:] c= G
by A16, XBOOLE_1:1;
:: thesis: verum
end;
A19:
dom (f " ) = the carrier of (TOP-REAL 2)
by A4, A7, TOPS_2:62;
reconsider f1 = proj1 , f2 = proj2 as Function of (TOP-REAL 2),R^1 by TOPMETR:24;
A20:
dom <:f1,f2:> = the carrier of (TOP-REAL 2)
by FUNCT_2:def 1;
now let x be
set ;
:: thesis: ( x in dom (f " ) implies (f " ) . x = <:f1,f2:> . x )assume A21:
x in dom (f " )
;
:: thesis: (f " ) . x = <:f1,f2:> . xthen consider a,
b being
Real such that A22:
x = <*a,b*>
by EUCLID:55;
A23:
(
dom f1 = the
carrier of
(TOP-REAL 2) &
dom f2 = the
carrier of
(TOP-REAL 2) )
by FUNCT_2:def 1;
A24:
[a,b] in dom f
by A3, TOPMETR:24, ZFMISC_1:106;
A25:
f . [a,b] = <*a,b*>
by A1;
reconsider p =
x as
Point of
(TOP-REAL 2) by A21;
thus (f " ) . x =
(f " ) . x
by A4, A7, TOPS_2:def 4
.=
[a,b]
by A7, A22, A24, A25, FUNCT_1:54
.=
[(p `1 ),b]
by A22, EUCLID:56
.=
[(p `1 ),(p `2 )]
by A22, EUCLID:56
.=
[(f1 . x),(p `2 )]
by PSCOMP_1:def 28
.=
[(f1 . x),(f2 . x)]
by PSCOMP_1:def 29
.=
<:f1,f2:> . x
by A21, A23, FUNCT_3:69
;
:: thesis: verum end;
then A26:
f " = <:f1,f2:>
by A19, A20, FUNCT_1:9;
( f1 is continuous & f2 is continuous )
by Th83;
hence
f /" is continuous
by A26, YELLOW12:41; :: thesis: verum