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) | (Lower_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 = E-max P & f . 1 = W-min 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) | (Lower_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 = E-max P & f . 1 = W-min P )
then consider f1 being Function of (Closed-Interval-TSpace (- 1),1),((TOP-REAL 2) | (Lower_Arc P)) such that
A2:
( f1 is being_homeomorphism & ( for q being Point of (TOP-REAL 2) st q in Lower_Arc P holds
f1 . (q `1 ) = q ) & f1 . (- 1) = W-min P & f1 . 1 = E-max P )
by Th43;
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 Th41;
reconsider T = (TOP-REAL 2) | (Lower_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) | (Lower_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;
(- 2) * r1 > (- 2) * r2
by A8, XREAL_1:71;
then A11:
((- 2) * r1) + 1
> ((- 2) * r2) + 1
by XREAL_1:10;
r1 <= 1
by A6, XXREAL_1:1;
then
(- 2) * r1 >= (- 2) * 1
by XREAL_1:67;
then
((- 2) * r1) + 1
>= ((- 2) * 1) + 1
by XREAL_1:9;
then A12:
- 1
<= ((- 2) * r1) + 1
;
r1 >= 0
by A6, XXREAL_1:1;
then
(- 2) * r1 <= (- 2) * 0
;
then
((- 2) * r1) + 1
<= ((- 2) * 0 ) + 1
by XREAL_1:9;
then
(((- 2) * r1) + 1) ^2 <= 1
^2
by A12, SQUARE_1:119;
then A13:
1
- ((((- 2) * r1) + 1) ^2 ) >= 0
by XREAL_1:50;
A14:
|[(((- 2) * r1) + 1),(- (sqrt (1 - ((((- 2) * r1) + 1) ^2 ))))]| `1 = ((- 2) * r1) + 1
by EUCLID:56;
A15:
|[(((- 2) * r1) + 1),(- (sqrt (1 - ((((- 2) * r1) + 1) ^2 ))))]| `2 = - (sqrt (1 - ((((- 2) * r1) + 1) ^2 )))
by EUCLID:56;
sqrt (1 - ((((- 2) * r1) + 1) ^2 )) >= 0
by A13, SQUARE_1:def 4;
then A16:
- (sqrt (1 - ((((- 2) * r1) + 1) ^2 ))) <= 0
;
|.|[(((- 2) * r1) + 1),(- (sqrt (1 - ((((- 2) * r1) + 1) ^2 ))))]|.| =
sqrt (((|[(((- 2) * r1) + 1),(- (sqrt (1 - ((((- 2) * r1) + 1) ^2 ))))]| `1 ) ^2 ) + ((|[(((- 2) * r1) + 1),(- (sqrt (1 - ((((- 2) * r1) + 1) ^2 ))))]| `2 ) ^2 ))
by JGRAPH_3:10
.=
sqrt (((((- 2) * r1) + 1) ^2 ) + ((sqrt (1 - ((((- 2) * r1) + 1) ^2 ))) ^2 ))
by A15, EUCLID:56
.=
sqrt (((((- 2) * r1) + 1) ^2 ) + (1 - ((((- 2) * r1) + 1) ^2 )))
by A13, 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 A15, A16;
then A17:
|[(((- 2) * r1) + 1),(- (sqrt (1 - ((((- 2) * r1) + 1) ^2 ))))]| in Lower_Arc P
by A1, Th38;
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, A14, A17
;
then A18:
q1 `1 = ((- 2) * r1) + 1
by A6, EUCLID:56;
r2 <= 1
by A6, XXREAL_1:1;
then
(- 2) * r2 >= (- 2) * 1
by XREAL_1:67;
then
((- 2) * r2) + 1
>= ((- 2) * 1) + 1
by XREAL_1:9;
then A19:
- 1
<= ((- 2) * r2) + 1
;
r2 >= 0
by A6, XXREAL_1:1;
then
(- 2) * r2 <= (- 2) * 0
;
then
((- 2) * r2) + 1
<= ((- 2) * 0 ) + 1
by XREAL_1:9;
then
(((- 2) * r2) + 1) ^2 <= 1
^2
by A19, SQUARE_1:119;
then A20:
1
- ((((- 2) * r2) + 1) ^2 ) >= 0
by XREAL_1:50;
A21:
|[(((- 2) * r2) + 1),(- (sqrt (1 - ((((- 2) * r2) + 1) ^2 ))))]| `1 = ((- 2) * r2) + 1
by EUCLID:56;
A22:
|[(((- 2) * r2) + 1),(- (sqrt (1 - ((((- 2) * r2) + 1) ^2 ))))]| `2 = - (sqrt (1 - ((((- 2) * r2) + 1) ^2 )))
by EUCLID:56;
sqrt (1 - ((((- 2) * r2) + 1) ^2 )) >= 0
by A20, SQUARE_1:def 4;
then A23:
- (sqrt (1 - ((((- 2) * r2) + 1) ^2 ))) <= 0
;
|.|[(((- 2) * r2) + 1),(- (sqrt (1 - ((((- 2) * r2) + 1) ^2 ))))]|.| =
sqrt (((|[(((- 2) * r2) + 1),(- (sqrt (1 - ((((- 2) * r2) + 1) ^2 ))))]| `1 ) ^2 ) + ((|[(((- 2) * r2) + 1),(- (sqrt (1 - ((((- 2) * r2) + 1) ^2 ))))]| `2 ) ^2 ))
by JGRAPH_3:10
.=
sqrt (((((- 2) * r2) + 1) ^2 ) + ((sqrt (1 - ((((- 2) * r2) + 1) ^2 ))) ^2 ))
by A22, EUCLID:56
.=
sqrt (((((- 2) * r2) + 1) ^2 ) + (1 - ((((- 2) * r2) + 1) ^2 )))
by A20, 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 A22, A23;
then A24:
|[(((- 2) * r2) + 1),(- (sqrt (1 - ((((- 2) * r2) + 1) ^2 ))))]| in Lower_Arc P
by A1, Th38;
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, A21, A24
;
hence
q1 `1 > q2 `1
by A6, A11, A18, EUCLID:56;
:: thesis: verum end;
A25:
now assume A26:
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 ))))]|;
A27:
g . r2 = ((- 2) * r2) + 1
by A3, A6;
A28:
g . r1 = ((- 2) * r1) + 1
by A3, A6;
A29:
(- 2) * r2 > (- 2) * r1
by A26, XREAL_1:71;
r2 <= 1
by A6, XXREAL_1:1;
then
(- 2) * r2 >= (- 2) * 1
by XREAL_1:67;
then
((- 2) * r2) + 1
>= ((- 2) * 1) + 1
by XREAL_1:9;
then A30:
- 1
<= ((- 2) * r2) + 1
;
r2 >= 0
by A6, XXREAL_1:1;
then
(- 2) * r2 <= (- 2) * 0
;
then
((- 2) * r2) + 1
<= ((- 2) * 0 ) + 1
by XREAL_1:9;
then
(((- 2) * r2) + 1) ^2 <= 1
^2
by A30, SQUARE_1:119;
then A31:
1
- ((((- 2) * r2) + 1) ^2 ) >= 0
by XREAL_1:50;
A32:
|[(((- 2) * r2) + 1),(- (sqrt (1 - ((((- 2) * r2) + 1) ^2 ))))]| `1 = ((- 2) * r2) + 1
by EUCLID:56;
A33:
|[(((- 2) * r2) + 1),(- (sqrt (1 - ((((- 2) * r2) + 1) ^2 ))))]| `2 = - (sqrt (1 - ((((- 2) * r2) + 1) ^2 )))
by EUCLID:56;
sqrt (1 - ((((- 2) * r2) + 1) ^2 )) >= 0
by A31, SQUARE_1:def 4;
then A34:
- (sqrt (1 - ((((- 2) * r2) + 1) ^2 ))) <= 0
;
|.|[(((- 2) * r2) + 1),(- (sqrt (1 - ((((- 2) * r2) + 1) ^2 ))))]|.| =
sqrt (((|[(((- 2) * r2) + 1),(- (sqrt (1 - ((((- 2) * r2) + 1) ^2 ))))]| `1 ) ^2 ) + ((|[(((- 2) * r2) + 1),(- (sqrt (1 - ((((- 2) * r2) + 1) ^2 ))))]| `2 ) ^2 ))
by JGRAPH_3:10
.=
sqrt (((((- 2) * r2) + 1) ^2 ) + ((sqrt (1 - ((((- 2) * r2) + 1) ^2 ))) ^2 ))
by A33, EUCLID:56
.=
sqrt (((((- 2) * r2) + 1) ^2 ) + (1 - ((((- 2) * r2) + 1) ^2 )))
by A31, 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 A33, A34;
then A35:
|[(((- 2) * r2) + 1),(- (sqrt (1 - ((((- 2) * r2) + 1) ^2 ))))]| in Lower_Arc P
by A1, Th38;
dom h = [.0 ,1.]
by BORSUK_1:83, FUNCT_2:def 1;
then h . r2 =
f1 . (((- 2) * r2) + 1)
by A6, A27, FUNCT_1:22
.=
|[(((- 2) * r2) + 1),(- (sqrt (1 - ((((- 2) * r2) + 1) ^2 ))))]|
by A2, A32, A35
;
then A36:
q2 `1 = ((- 2) * r2) + 1
by A6, EUCLID:56;
r1 <= 1
by A6, XXREAL_1:1;
then
(- 2) * r1 >= (- 2) * 1
by XREAL_1:67;
then
((- 2) * r1) + 1
>= ((- 2) * 1) + 1
by XREAL_1:9;
then A37:
- 1
<= ((- 2) * r1) + 1
;
r1 >= 0
by A6, XXREAL_1:1;
then
(- 2) * r1 <= (- 2) * 0
;
then
((- 2) * r1) + 1
<= ((- 2) * 0 ) + 1
by XREAL_1:9;
then
(((- 2) * r1) + 1) ^2 <= 1
^2
by A37, SQUARE_1:119;
then A38:
1
- ((((- 2) * r1) + 1) ^2 ) >= 0
by XREAL_1:50;
A39:
|[(((- 2) * r1) + 1),(- (sqrt (1 - ((((- 2) * r1) + 1) ^2 ))))]| `1 = ((- 2) * r1) + 1
by EUCLID:56;
A40:
|[(((- 2) * r1) + 1),(- (sqrt (1 - ((((- 2) * r1) + 1) ^2 ))))]| `2 = - (sqrt (1 - ((((- 2) * r1) + 1) ^2 )))
by EUCLID:56;
sqrt (1 - ((((- 2) * r1) + 1) ^2 )) >= 0
by A38, SQUARE_1:def 4;
then A41:
- (sqrt (1 - ((((- 2) * r1) + 1) ^2 ))) <= 0
;
|.|[(((- 2) * r1) + 1),(- (sqrt (1 - ((((- 2) * r1) + 1) ^2 ))))]|.| =
sqrt (((|[(((- 2) * r1) + 1),(- (sqrt (1 - ((((- 2) * r1) + 1) ^2 ))))]| `1 ) ^2 ) + ((|[(((- 2) * r1) + 1),(- (sqrt (1 - ((((- 2) * r1) + 1) ^2 ))))]| `2 ) ^2 ))
by JGRAPH_3:10
.=
sqrt (((((- 2) * r1) + 1) ^2 ) + ((sqrt (1 - ((((- 2) * r1) + 1) ^2 ))) ^2 ))
by A40, EUCLID:56
.=
sqrt (((((- 2) * r1) + 1) ^2 ) + (1 - ((((- 2) * r1) + 1) ^2 )))
by A38, 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 A40, A41;
then A42:
|[(((- 2) * r1) + 1),(- (sqrt (1 - ((((- 2) * r1) + 1) ^2 ))))]| in Lower_Arc P
by A1, Th38;
dom h = [.0 ,1.]
by BORSUK_1:83, FUNCT_2:def 1;
then h . r1 =
f1 . (((- 2) * r1) + 1)
by A6, A28, FUNCT_1:22
.=
|[(((- 2) * r1) + 1),(- (sqrt (1 - ((((- 2) * r1) + 1) ^2 ))))]|
by A2, A39, A42
;
hence
q2 `1 > q1 `1
by A6, A29, A36, A39, XREAL_1:10;
:: thesis: verum end;
hence
(
r1 < r2 iff
q1 `1 > q2 `1 )
by A7;
:: thesis: verum
end;
A45:
dom h = [.0 ,1.]
by BORSUK_1:83, FUNCT_2:def 1;
then
0 in dom h
by XXREAL_1:1;
then A46:
h . 0 = E-max P
by A2, A3, FUNCT_1:22;
1 in dom h
by A45, XXREAL_1:1;
then
h . 1 = W-min P
by A2, A3, FUNCT_1:22;
hence
ex f being Function of I[01] ,((TOP-REAL 2) | (Lower_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 = E-max P & f . 1 = W-min P )
by A4, A5, A46; :: thesis: verum