reconsider f1 = proj1 , f2 = proj2 as Function of (TOP-REAL 2),R^1 by TOPMETR:17;
let f be Function of [:R^1,R^1:],(TOP-REAL 2); ( ( 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*>
; f is being_homeomorphism
thus
dom f = [#] [:R^1,R^1:]
by FUNCT_2:def 1; TOPS_2:def 5 ( rng f = [#] (TOP-REAL 2) & f is one-to-one & f is continuous & f " is continuous )
A2:
the carrier of [:R^1,R^1:] = [: the carrier of R^1, the carrier of R^1:]
by BORSUK_1:def 2;
then A3:
dom f = [: the carrier of R^1, the carrier of R^1:]
by FUNCT_2:def 1;
thus A4:
rng f = [#] (TOP-REAL 2)
( f is one-to-one & f is continuous & f " is continuous )proof
thus
rng f c= [#] (TOP-REAL 2)
;
XBOOLE_0:def 10 [#] (TOP-REAL 2) c= rng f
let y be
object ;
TARSKI:def 3 ( not y in [#] (TOP-REAL 2) or y in rng f )
assume
y in [#] (TOP-REAL 2)
;
y in rng f
then consider a,
b being
Element of
REAL such that A5:
y = <*a,b*>
by EUCLID:51;
A6:
f . [a,b] = <*a,b*>
by A1;
reconsider a =
a,
b =
b as
Element of
REAL ;
[a,b] in dom f
by A3, TOPMETR:17, ZFMISC_1:87;
hence
y in rng f
by A5, A6, FUNCT_1:def 3;
verum
end;
thus A7:
f is one-to-one
( f is continuous & f " is continuous )proof
let x,
y be
object ;
FUNCT_1:def 4 ( not x in dom f or not y in dom f or not f . x = f . y or x = y )
assume
x in dom f
;
( not y in dom f or not f . x = f . y or x = y )
then consider x1,
x2 being
object such that A8:
x1 in REAL
and A9:
x2 in REAL
and A10:
x = [x1,x2]
by A2, TOPMETR:17, ZFMISC_1:def 2;
assume
y in dom f
;
( not f . x = f . y or x = y )
then consider y1,
y2 being
object such that A11:
y1 in REAL
and A12:
y2 in REAL
and A13:
y = [y1,y2]
by A2, TOPMETR:17, ZFMISC_1:def 2;
reconsider x1 =
x1,
x2 =
x2,
y1 =
y1,
y2 =
y2 as
Real by A8, A9, A11, A12;
assume A14:
f . x = f . y
;
x = y
A15:
f . [y1,y2] = <*y1,y2*>
by A1;
A16:
f . [x1,x2] = <*x1,x2*>
by A1;
then
x1 = y1
by A10, A13, A15, A14, FINSEQ_1:77;
hence
x = y
by A10, A13, A16, A15, A14, FINSEQ_1:77;
verum
end;
A17:
now for x being object st x in dom (f ") holds
(f ") . x = <:f1,f2:> . xA18:
dom f2 = the
carrier of
(TOP-REAL 2)
by FUNCT_2:def 1;
let x be
object ;
( x in dom (f ") implies (f ") . x = <:f1,f2:> . x )A19:
dom f1 = the
carrier of
(TOP-REAL 2)
by FUNCT_2:def 1;
assume A20:
x in dom (f ")
;
(f ") . x = <:f1,f2:> . xthen consider a,
b being
Element of
REAL such that A21:
x = <*a,b*>
by EUCLID:51;
reconsider a =
a,
b =
b as
Element of
REAL ;
reconsider p =
x as
Point of
(TOP-REAL 2) by A20;
A22:
[a,b] in dom f
by A3, TOPMETR:17, ZFMISC_1:87;
A23:
f . [a,b] = <*a,b*>
by A1;
f is
onto
by A4, FUNCT_2:def 3;
hence (f ") . x =
(f ") . x
by A7, TOPS_2:def 4
.=
[a,b]
by A7, A21, A22, A23, FUNCT_1:32
.=
[(p `1),b]
by A21, EUCLID:52
.=
[(p `1),(p `2)]
by A21, EUCLID:52
.=
[(f1 . x),(p `2)]
by PSCOMP_1:def 5
.=
[(f1 . x),(f2 . x)]
by PSCOMP_1:def 6
.=
<:f1,f2:> . x
by A20, A19, A18, FUNCT_3:49
;
verum end;
thus
f is continuous
f " is continuous proof
let w be
Point of
[:R^1,R^1:];
BORSUK_1:def 1 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;
ex b1 being a_neighborhood of w st f .: b1 c= G
reconsider fw =
f . w as
Point of
(Euclid 2) by TOPREAL3:8;
consider x,
y being
object such that A24:
x in the
carrier of
R^1
and A25:
y in the
carrier of
R^1
and A26:
w = [x,y]
by A2, ZFMISC_1:def 2;
reconsider x =
x,
y =
y as
Real by A24, A25;
fw in Int G
by CONNSP_2:def 1;
then consider r being
Real such that A27:
r > 0
and A28:
Ball (
fw,
r)
c= G
by GOBOARD6:5;
reconsider r =
r as
Real ;
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:17;
A29:
f . [x,y] = <*x,y*>
by A1;
then
y = (f . w) `2
by A26, EUCLID:52;
then A30:
y in B
by A27, Th14, SQUARE_1:19, XREAL_1:139;
x = (f . w) `1
by A26, A29, EUCLID:52;
then
x in A
by A27, Th14, SQUARE_1:19, XREAL_1:139;
then A31:
w in [:A,B:]
by A26, A30, ZFMISC_1:87;
take
[:A,B:]
;
( [:A,B:] is a_neighborhood of w & f .: [:A,B:] c= G )
A32:
B is
open
by JORDAN6:35;
A is
open
by JORDAN6:35;
then
[:A,B:] in Base-Appr [:A,B:]
by A32;
then
w in union (Base-Appr [:A,B:])
by A31, TARSKI:def 4;
then
w in Int [:A,B:]
by BORSUK_1:14;
hence
[:A,B:] is
a_neighborhood of
w
by CONNSP_2:def 1;
f .: [:A,B:] c= G
product ((1,2) --> (A,B)) c= Ball (
fw,
r)
by Th39;
then
f .: [:A,B:] c= Ball (
fw,
r)
by A1, Th68;
hence
f .: [:A,B:] c= G
by A28;
verum
end;
A33:
f1 is continuous
by JORDAN5A:27;
A34:
f2 is continuous
by JORDAN5A:27;
dom <:f1,f2:> = the carrier of (TOP-REAL 2)
by FUNCT_2:def 1;
then
f " = <:f1,f2:>
by A4, A7, A17, TOPS_2:49;
hence
f " is continuous
by A33, A34, YELLOW12:41; verum