let f be Function of (TOP-REAL 1),R^1 ; :: thesis: ( ( for p being Element of (TOP-REAL 1) holds f . p = Proj p,1 ) implies f is being_homeomorphism )
assume A1:
for p being Element of (TOP-REAL 1) holds f . p = Proj p,1
; :: thesis: f is being_homeomorphism
1 in Seg 1
by FINSEQ_1:3;
then A2:
f is continuous
by A1, Th22;
A3:
[#] (TOP-REAL 1) = the carrier of (TOP-REAL 1)
;
A4:
dom f = the carrier of (TOP-REAL 1)
by FUNCT_2:def 1;
REAL c= rng f
then A6:
rng f = [#] R^1
by TOPMETR:24, XBOOLE_0:def 10;
A7:
f is one-to-one
proof
for
x1,
x2 being
set st
x1 in dom f &
x2 in dom f &
f . x1 = f . x2 holds
x1 = x2
proof
let x1,
x2 be
set ;
:: thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )
assume A8:
(
x1 in dom f &
x2 in dom f &
f . x1 = f . x2 )
;
:: thesis: x1 = x2
then reconsider p1 =
x1,
p2 =
x2 as
Element of
(TOP-REAL 1) ;
consider r1 being
Real such that A9:
p1 = <*r1*>
by Th24;
consider r2 being
Real such that A10:
p2 = <*r2*>
by Th24;
A11:
( 1
<= 1 & 1
<= len <*r1*> )
by FINSEQ_1:57;
A12:
( 1
<= 1 & 1
<= len <*r2*> )
by FINSEQ_1:57;
A13:
f . p1 =
Proj p1,1
by A1
.=
<*r1*> /. 1
by A9, Def1
.=
<*r1*> . 1
by A11, FINSEQ_4:24
.=
r1
by FINSEQ_1:57
;
f . p2 =
Proj p2,1
by A1
.=
<*r2*> /. 1
by A10, Def1
.=
<*r2*> . 1
by A12, FINSEQ_4:24
.=
r2
by FINSEQ_1:57
;
hence
x1 = x2
by A8, A9, A10, A13;
:: thesis: verum
end;
hence
f is
one-to-one
by FUNCT_1:def 8;
:: thesis: verum
end;
XX:
TopStruct(# the carrier of (TOP-REAL 1),the topology of (TOP-REAL 1) #) = TopSpaceMetr (Euclid 1)
by EUCLID:def 8;
then reconsider ff = f /" as Function of R^1 ,(TopSpaceMetr (Euclid 1)) ;
f /" is continuous
proof
the
carrier of
R^1 c= rng f
then A14:
rng f = the
carrier of
R^1
by XBOOLE_0:def 10;
TopStruct(# the
carrier of
(TOP-REAL 1),the
topology of
(TOP-REAL 1) #)
= TopSpaceMetr (Euclid 1)
by EUCLID:def 8;
then reconsider g =
f /" as
Function of
R^1 ,
(TopSpaceMetr (Euclid 1)) ;
reconsider g1 =
g as
Function of the
carrier of
R^1 ,the
carrier of
(TOP-REAL 1) ;
for
r being
real number for
u being
Element of the
carrier of
(Euclid 1) for
P being
Subset of the
carrier of
(TopSpaceMetr (Euclid 1)) st
r > 0 &
P = Ball u,
r holds
g " P is
open
proof
let r be
real number ;
:: thesis: for u being Element of the carrier of (Euclid 1)
for P being Subset of the carrier of (TopSpaceMetr (Euclid 1)) st r > 0 & P = Ball u,r holds
g " P is open let u be
Element of the
carrier of
(Euclid 1);
:: thesis: for P being Subset of the carrier of (TopSpaceMetr (Euclid 1)) st r > 0 & P = Ball u,r holds
g " P is open let P be
Subset of the
carrier of
(TopSpaceMetr (Euclid 1));
:: thesis: ( r > 0 & P = Ball u,r implies g " P is open )
assume A15:
(
r > 0 &
P = Ball u,
r )
;
:: thesis: g " P is open
consider s1 being
Real such that A16:
u = <*s1*>
by FINSEQ_2:117;
reconsider f1 =
f as
Function of the
carrier of
(TOP-REAL 1),the
carrier of
R^1 ;
dom f1 = the
carrier of
(TOP-REAL 1)
by FUNCT_2:def 1;
then A17:
dom f1 = REAL 1
by EUCLID:25;
A18:
g1 = f1 "
by A7, A14, TOPS_2:def 4;
A19:
Ball u,
r = { <*s*> where s is Real : ( s1 - r < s & s < s1 + r ) }
by A15, A16, Th33;
f1 .: (Ball u,r) = { w1 where w1 is Real : ( s1 - r < w1 & w1 < s1 + r ) }
proof
A20:
f1 .: (Ball u,r) c= { w1 where w1 is Real : ( s1 - r < w1 & w1 < s1 + r ) }
{ w1 where w1 is Real : ( s1 - r < w1 & w1 < s1 + r ) } c= f1 .: (Ball u,r)
proof
let z be
set ;
:: according to TARSKI:def 3 :: thesis: ( not z in { w1 where w1 is Real : ( s1 - r < w1 & w1 < s1 + r ) } or z in f1 .: (Ball u,r) )
assume
z in { w1 where w1 is Real : ( s1 - r < w1 & w1 < s1 + r ) }
;
:: thesis: z in f1 .: (Ball u,r)
then consider r1 being
Real such that A24:
(
z = r1 &
s1 - r < r1 &
r1 < s1 + r )
;
<*r1*> in 1
-tuples_on REAL
by FINSEQ_2:118;
then
<*r1*> in REAL 1
by FINSEQ_2:118;
then reconsider q =
<*r1*> as
Element of
(TOP-REAL 1) by EUCLID:25;
Ball u,
r = { <*s*> where s is Real : ( s1 - r < s & s < s1 + r ) }
by A15, A16, Th33;
then A25:
<*r1*> in Ball u,
r
by A24;
z =
<*r1*> /. 1
by A24, FINSEQ_4:25
.=
Proj q,1
by Def1
.=
f1 . <*r1*>
by A1
;
hence
z in f1 .: (Ball u,r)
by A17, A25, FUNCT_1:def 12;
:: thesis: verum
end;
hence
f1 .: (Ball u,r) = { w1 where w1 is Real : ( s1 - r < w1 & w1 < s1 + r ) }
by A20, XBOOLE_0:def 10;
:: thesis: verum
end;
then
g1 " (Ball u,r) = { w1 where w1 is Real : ( s1 - r < w1 & w1 < s1 + r ) }
by A7, A18, FUNCT_1:154;
hence
g " P is
open
by A15, Th32;
:: thesis: verum
end;
then
ff is
continuous
by Th20;
hence
f /" is
continuous
by XX, PRE_TOPC:63;
:: thesis: verum
end;
hence
f is being_homeomorphism
by A2, A3, A4, A6, A7, TOPS_2:def 5; :: thesis: verum