let P be non empty compact Subset of (TOP-REAL 2); :: thesis: ( P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } implies ex f being Function of I[01] ,((TOP-REAL 2) | (Upper_Arc P)) st
( f is being_homeomorphism & ( for q1, q2 being Point of (TOP-REAL 2)
for r1, r2 being Real st f . r1 = q1 & f . r2 = q2 & r1 in [.0 ,1.] & r2 in [.0 ,1.] holds
( r1 < r2 iff q1 `1 < q2 `1 ) ) & f . 0 = W-min P & f . 1 = E-max P ) )
assume A1:
P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 }
; :: thesis: ex f being Function of I[01] ,((TOP-REAL 2) | (Upper_Arc P)) st
( f is being_homeomorphism & ( for q1, q2 being Point of (TOP-REAL 2)
for r1, r2 being Real st f . r1 = q1 & f . r2 = q2 & r1 in [.0 ,1.] & r2 in [.0 ,1.] holds
( r1 < r2 iff q1 `1 < q2 `1 ) ) & f . 0 = W-min P & f . 1 = E-max P )
then consider f1 being Function of (Closed-Interval-TSpace (- 1),1),((TOP-REAL 2) | (Upper_Arc P)) such that
A2:
( f1 is being_homeomorphism & ( for q being Point of (TOP-REAL 2) st q in Upper_Arc P holds
f1 . (q `1 ) = q ) & f1 . (- 1) = W-min P & f1 . 1 = E-max P )
by Th44;
consider g being Function of I[01] ,(Closed-Interval-TSpace (- 1),1) such that
A3:
( g is being_homeomorphism & ( for r being Real st r in [.0 ,1.] holds
g . r = (2 * r) - 1 ) & g . 0 = - 1 & g . 1 = 1 )
by Th42;
reconsider T = (TOP-REAL 2) | (Upper_Arc P) as non empty TopSpace ;
reconsider f2 = f1 as Function of (Closed-Interval-TSpace (- 1),1),T ;
A4:
f2 * g is being_homeomorphism
by A2, A3, TOPS_2:71;
reconsider h = f1 * g as Function of I[01] ,((TOP-REAL 2) | (Upper_Arc P)) ;
A5:
for q1, q2 being Point of (TOP-REAL 2)
for r1, r2 being Real st h . r1 = q1 & h . r2 = q2 & r1 in [.0 ,1.] & r2 in [.0 ,1.] holds
( r1 < r2 iff q1 `1 < q2 `1 )
proof
let q1,
q2 be
Point of
(TOP-REAL 2);
:: thesis: for r1, r2 being Real st h . r1 = q1 & h . r2 = q2 & r1 in [.0 ,1.] & r2 in [.0 ,1.] holds
( r1 < r2 iff q1 `1 < q2 `1 )let r1,
r2 be
Real;
:: thesis: ( h . r1 = q1 & h . r2 = q2 & r1 in [.0 ,1.] & r2 in [.0 ,1.] implies ( r1 < r2 iff q1 `1 < q2 `1 ) )
assume A6:
(
h . r1 = q1 &
h . r2 = q2 &
r1 in [.0 ,1.] &
r2 in [.0 ,1.] )
;
:: thesis: ( r1 < r2 iff q1 `1 < q2 `1 )
A7:
now assume A8:
r1 > r2
;
:: thesis: q1 `1 > q2 `1 set s1 =
(2 * r1) - 1;
set s2 =
(2 * r2) - 1;
set p1 =
|[((2 * r1) - 1),(sqrt (1 - (((2 * r1) - 1) ^2 )))]|;
set p2 =
|[((2 * r2) - 1),(sqrt (1 - (((2 * r2) - 1) ^2 )))]|;
A9:
g . r1 = (2 * r1) - 1
by A3, A6;
A10:
g . r2 = (2 * r2) - 1
by A3, A6;
A11:
2
* r1 > 2
* r2
by A8, XREAL_1:70;
r1 <= 1
by A6, XXREAL_1:1;
then
2
* r1 <= 2
* 1
by XREAL_1:66;
then A12:
(2 * r1) - 1
<= (2 * 1) - 1
by XREAL_1:11;
r1 >= 0
by A6, XXREAL_1:1;
then
2
* r1 >= 2
* 0
;
then A13:
(2 * r1) - 1
>= (2 * 0 ) - 1
by XREAL_1:11;
(2 * 0 ) - 1
= - 1
;
then
((2 * r1) - 1) ^2 <= 1
^2
by A12, A13, SQUARE_1:119;
then A14:
1
- (((2 * r1) - 1) ^2 ) >= 0
by XREAL_1:50;
A15:
|[((2 * r1) - 1),(sqrt (1 - (((2 * r1) - 1) ^2 )))]| `1 = (2 * r1) - 1
by EUCLID:56;
A16:
|[((2 * r1) - 1),(sqrt (1 - (((2 * r1) - 1) ^2 )))]| `2 = sqrt (1 - (((2 * r1) - 1) ^2 ))
by EUCLID:56;
A17:
sqrt (1 - (((2 * r1) - 1) ^2 )) >= 0
by A14, SQUARE_1:def 4;
|.|[((2 * r1) - 1),(sqrt (1 - (((2 * r1) - 1) ^2 )))]|.| =
sqrt ((((2 * r1) - 1) ^2 ) + ((sqrt (1 - (((2 * r1) - 1) ^2 ))) ^2 ))
by A15, A16, JGRAPH_3:10
.=
sqrt ((((2 * r1) - 1) ^2 ) + (1 - (((2 * r1) - 1) ^2 )))
by A14, SQUARE_1:def 4
.=
1
by SQUARE_1:83
;
then
|[((2 * r1) - 1),(sqrt (1 - (((2 * r1) - 1) ^2 )))]| in P
by A1;
then
|[((2 * r1) - 1),(sqrt (1 - (((2 * r1) - 1) ^2 )))]| in { p3 where p3 is Point of (TOP-REAL 2) : ( p3 in P & p3 `2 >= 0 ) }
by A16, A17;
then A18:
|[((2 * r1) - 1),(sqrt (1 - (((2 * r1) - 1) ^2 )))]| in Upper_Arc P
by A1, Th37;
dom h = [.0 ,1.]
by BORSUK_1:83, FUNCT_2:def 1;
then h . r1 =
f1 . ((2 * r1) - 1)
by A6, A9, FUNCT_1:22
.=
|[((2 * r1) - 1),(sqrt (1 - (((2 * r1) - 1) ^2 )))]|
by A2, A15, A18
;
then A19:
q1 `1 = (2 * r1) - 1
by A6, EUCLID:56;
r2 <= 1
by A6, XXREAL_1:1;
then
2
* r2 <= 2
* 1
by XREAL_1:66;
then A20:
(2 * r2) - 1
<= (2 * 1) - 1
by XREAL_1:11;
r2 >= 0
by A6, XXREAL_1:1;
then
2
* r2 >= 2
* 0
;
then A21:
(2 * r2) - 1
>= (2 * 0 ) - 1
by XREAL_1:11;
(2 * 0 ) - 1
= - 1
;
then
((2 * r2) - 1) ^2 <= 1
^2
by A20, A21, SQUARE_1:119;
then A22:
1
- (((2 * r2) - 1) ^2 ) >= 0
by XREAL_1:50;
A23:
|[((2 * r2) - 1),(sqrt (1 - (((2 * r2) - 1) ^2 )))]| `1 = (2 * r2) - 1
by EUCLID:56;
A24:
|[((2 * r2) - 1),(sqrt (1 - (((2 * r2) - 1) ^2 )))]| `2 = sqrt (1 - (((2 * r2) - 1) ^2 ))
by EUCLID:56;
A25:
sqrt (1 - (((2 * r2) - 1) ^2 )) >= 0
by A22, SQUARE_1:def 4;
|.|[((2 * r2) - 1),(sqrt (1 - (((2 * r2) - 1) ^2 )))]|.| =
sqrt ((((2 * r2) - 1) ^2 ) + ((sqrt (1 - (((2 * r2) - 1) ^2 ))) ^2 ))
by A23, A24, JGRAPH_3:10
.=
sqrt ((((2 * r2) - 1) ^2 ) + (1 - (((2 * r2) - 1) ^2 )))
by A22, SQUARE_1:def 4
.=
1
by SQUARE_1:83
;
then
|[((2 * r2) - 1),(sqrt (1 - (((2 * r2) - 1) ^2 )))]| in P
by A1;
then
|[((2 * r2) - 1),(sqrt (1 - (((2 * r2) - 1) ^2 )))]| in { p3 where p3 is Point of (TOP-REAL 2) : ( p3 in P & p3 `2 >= 0 ) }
by A24, A25;
then A26:
|[((2 * r2) - 1),(sqrt (1 - (((2 * r2) - 1) ^2 )))]| in Upper_Arc P
by A1, Th37;
dom h = [.0 ,1.]
by BORSUK_1:83, FUNCT_2:def 1;
then h . r2 =
f1 . ((2 * r2) - 1)
by A6, A10, FUNCT_1:22
.=
|[((2 * r2) - 1),(sqrt (1 - (((2 * r2) - 1) ^2 )))]|
by A2, A23, A26
;
hence
q1 `1 > q2 `1
by A6, A11, A19, A23, XREAL_1:16;
:: thesis: verum end;
A27:
now assume A28:
r2 > r1
;
:: thesis: q2 `1 > q1 `1 set s1 =
(2 * r2) - 1;
set s2 =
(2 * r1) - 1;
set p1 =
|[((2 * r2) - 1),(sqrt (1 - (((2 * r2) - 1) ^2 )))]|;
set p2 =
|[((2 * r1) - 1),(sqrt (1 - (((2 * r1) - 1) ^2 )))]|;
A29:
g . r2 = (2 * r2) - 1
by A3, A6;
A30:
g . r1 = (2 * r1) - 1
by A3, A6;
A31:
2
* r2 > 2
* r1
by A28, XREAL_1:70;
r2 <= 1
by A6, XXREAL_1:1;
then
2
* r2 <= 2
* 1
by XREAL_1:66;
then A32:
(2 * r2) - 1
<= (2 * 1) - 1
by XREAL_1:11;
r2 >= 0
by A6, XXREAL_1:1;
then
2
* r2 >= 2
* 0
;
then
(2 * r2) - 1
>= (2 * 0 ) - 1
by XREAL_1:11;
then
- 1
<= (2 * r2) - 1
;
then
((2 * r2) - 1) ^2 <= 1
^2
by A32, SQUARE_1:119;
then A33:
1
- (((2 * r2) - 1) ^2 ) >= 0
by XREAL_1:50;
A34:
|[((2 * r2) - 1),(sqrt (1 - (((2 * r2) - 1) ^2 )))]| `1 = (2 * r2) - 1
by EUCLID:56;
A35:
|[((2 * r2) - 1),(sqrt (1 - (((2 * r2) - 1) ^2 )))]| `2 = sqrt (1 - (((2 * r2) - 1) ^2 ))
by EUCLID:56;
A36:
sqrt (1 - (((2 * r2) - 1) ^2 )) >= 0
by A33, SQUARE_1:def 4;
|.|[((2 * r2) - 1),(sqrt (1 - (((2 * r2) - 1) ^2 )))]|.| =
sqrt ((((2 * r2) - 1) ^2 ) + ((sqrt (1 - (((2 * r2) - 1) ^2 ))) ^2 ))
by A34, A35, JGRAPH_3:10
.=
sqrt ((((2 * r2) - 1) ^2 ) + (1 - (((2 * r2) - 1) ^2 )))
by A33, SQUARE_1:def 4
.=
1
by SQUARE_1:83
;
then
|[((2 * r2) - 1),(sqrt (1 - (((2 * r2) - 1) ^2 )))]| in P
by A1;
then
|[((2 * r2) - 1),(sqrt (1 - (((2 * r2) - 1) ^2 )))]| in { p3 where p3 is Point of (TOP-REAL 2) : ( p3 in P & p3 `2 >= 0 ) }
by A35, A36;
then A37:
|[((2 * r2) - 1),(sqrt (1 - (((2 * r2) - 1) ^2 )))]| in Upper_Arc P
by A1, Th37;
dom h = [.0 ,1.]
by BORSUK_1:83, FUNCT_2:def 1;
then h . r2 =
f1 . ((2 * r2) - 1)
by A6, A29, FUNCT_1:22
.=
|[((2 * r2) - 1),(sqrt (1 - (((2 * r2) - 1) ^2 )))]|
by A2, A34, A37
;
then A38:
q2 `1 = (2 * r2) - 1
by A6, EUCLID:56;
r1 <= 1
by A6, XXREAL_1:1;
then
2
* r1 <= 2
* 1
by XREAL_1:66;
then A39:
(2 * r1) - 1
<= (2 * 1) - 1
by XREAL_1:11;
r1 >= 0
by A6, XXREAL_1:1;
then
2
* r1 >= 2
* 0
;
then
(2 * r1) - 1
>= (2 * 0 ) - 1
by XREAL_1:11;
then
- 1
<= (2 * r1) - 1
;
then
((2 * r1) - 1) ^2 <= 1
^2
by A39, SQUARE_1:119;
then A40:
1
- (((2 * r1) - 1) ^2 ) >= 0
by XREAL_1:50;
A41:
|[((2 * r1) - 1),(sqrt (1 - (((2 * r1) - 1) ^2 )))]| `1 = (2 * r1) - 1
by EUCLID:56;
A42:
|[((2 * r1) - 1),(sqrt (1 - (((2 * r1) - 1) ^2 )))]| `2 = sqrt (1 - (((2 * r1) - 1) ^2 ))
by EUCLID:56;
A43:
sqrt (1 - (((2 * r1) - 1) ^2 )) >= 0
by A40, SQUARE_1:def 4;
|.|[((2 * r1) - 1),(sqrt (1 - (((2 * r1) - 1) ^2 )))]|.| =
sqrt ((((2 * r1) - 1) ^2 ) + ((sqrt (1 - (((2 * r1) - 1) ^2 ))) ^2 ))
by A41, A42, JGRAPH_3:10
.=
sqrt ((((2 * r1) - 1) ^2 ) + (1 - (((2 * r1) - 1) ^2 )))
by A40, SQUARE_1:def 4
.=
1
by SQUARE_1:83
;
then
|[((2 * r1) - 1),(sqrt (1 - (((2 * r1) - 1) ^2 )))]| in P
by A1;
then
|[((2 * r1) - 1),(sqrt (1 - (((2 * r1) - 1) ^2 )))]| in { p3 where p3 is Point of (TOP-REAL 2) : ( p3 in P & p3 `2 >= 0 ) }
by A42, A43;
then A44:
|[((2 * r1) - 1),(sqrt (1 - (((2 * r1) - 1) ^2 )))]| in Upper_Arc P
by A1, Th37;
dom h = [.0 ,1.]
by BORSUK_1:83, FUNCT_2:def 1;
then h . r1 =
f1 . ((2 * r1) - 1)
by A6, A30, FUNCT_1:22
.=
|[((2 * r1) - 1),(sqrt (1 - (((2 * r1) - 1) ^2 )))]|
by A2, A41, A44
;
hence
q2 `1 > q1 `1
by A6, A31, A38, A41, XREAL_1:16;
:: thesis: verum end;
hence
(
r1 < r2 iff
q1 `1 < q2 `1 )
by A27;
:: thesis: verum
end;
A47:
dom h = [.0 ,1.]
by BORSUK_1:83, FUNCT_2:def 1;
then
0 in dom h
by XXREAL_1:1;
then A48:
h . 0 = W-min P
by A2, A3, FUNCT_1:22;
1 in dom h
by A47, XXREAL_1:1;
then
h . 1 = E-max P
by A2, A3, FUNCT_1:22;
hence
ex f being Function of I[01] ,((TOP-REAL 2) | (Upper_Arc P)) st
( f is being_homeomorphism & ( for q1, q2 being Point of (TOP-REAL 2)
for r1, r2 being Real st f . r1 = q1 & f . r2 = q2 & r1 in [.0 ,1.] & r2 in [.0 ,1.] holds
( r1 < r2 iff q1 `1 < q2 `1 ) ) & f . 0 = W-min P & f . 1 = E-max P )
by A4, A5, A48; :: thesis: verum