:: Some Properties of Circles on the Plane
:: by Artur Korni{\l}owicz and Yasunari Shidama
::
:: Received October 18, 2004
:: Copyright (c) 2004-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, RELAT_1, SIN_COS, EUCLID, CARD_1, STRUCT_0, TOPMETR,
ARYTM_1, XXREAL_0, XXREAL_1, ARYTM_3, SUBSET_1, INT_1, PRE_TOPC,
XBOOLE_0, ORDINAL2, SIN_COS6, JGRAPH_2, FUNCT_1, REAL_1, XCMPLX_0,
FUNCT_2, TAXONOM2, SETFAM_1, TARSKI, ZFMISC_1, RCOMP_1, PARTFUN1, TMAP_1,
CONNSP_2, FCONT_1, TOPS_1, TOPS_2, TOPREAL2, BORSUK_2, METRIC_1, MCART_1,
JGRAPH_6, COMPLEX1, NAT_1, SUPINF_2, TOPREALA, T_0TOPSP, TOPREAL1,
FINSEQ_1, SQUARE_1, FUNCOP_1, BORSUK_4, CARD_3, VALUED_1, TOPREALB,
FUNCT_7;
notations TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, ORDINAL1, FUNCT_1, RELSET_1,
PARTFUN1, VALUED_1, NUMBERS, XCMPLX_0, XREAL_0, COMPLEX1, REAL_1,
SQUARE_1, INT_1, CARD_3, FINSEQ_1, FUNCT_4, RCOMP_1, FCONT_1, DOMAIN_1,
FUNCT_2, FUNCOP_1, STRUCT_0, PRE_TOPC, TOPS_1, BORSUK_1, TSEP_1, TOPS_2,
COMPTS_1, CONNSP_2, T_0TOPSP, TMAP_1, TOPREAL1, TOPREAL2, METRIC_1,
TOPMETR, RLVECT_1, EUCLID, BORSUK_2, SIN_COS, JGRAPH_6, BORSUK_3,
TAXONOM2, BORSUK_4, TOPREAL9, TOPALG_2, SIN_COS6, PSCOMP_1, TOPREALA,
XXREAL_0;
constructors REAL_1, SQUARE_1, CARD_3, RCOMP_1, FCONT_1, COMSEQ_3, SIN_COS,
SIN_COS6, TOPS_1, TOPS_2, COMPTS_1, GRCAT_1, TMAP_1, MONOID_0, TOPREAL1,
TOPREAL2, PSCOMP_1, TAXONOM2, BORSUK_2, BORSUK_3, BORSUK_4, JGRAPH_6,
TOPALG_2, TOPREAL9, TOPREALA, XXREAL_2, FUNCOP_1, BINOP_2, FUNCT_4,
NUMBERS;
registrations SUBSET_1, FUNCT_1, RELSET_1, FUNCT_2, NUMBERS, XCMPLX_0,
XXREAL_0, XREAL_0, NAT_1, INT_1, MEMBERED, RCOMP_1, SIN_COS6, STRUCT_0,
PRE_TOPC, TOPS_1, BORSUK_1, MONOID_0, EUCLID, TOPMETR, TOPREAL1,
TOPREAL2, PSCOMP_1, TOPGRP_1, BORSUK_3, FCONT_1, TOPALG_3, TOPREAL9,
TOPREALA, VALUED_0, SIN_COS, FUNCOP_1, MEASURE6, ORDINAL1, SQUARE_1,
CARD_1;
requirements NUMERALS, BOOLE, SUBSET, ARITHM, REAL;
definitions TARSKI, XBOOLE_0, FUNCT_1, FUNCT_2, TOPS_2, T_0TOPSP, TMAP_1,
STRUCT_0, TAXONOM2, TSEP_1, SETFAM_1;
equalities XBOOLE_0, TMAP_1, STRUCT_0, TOPREALA, SQUARE_1, TOPREAL9, SUBSET_1,
ALGSTR_0;
expansions TARSKI, XBOOLE_0, FUNCT_1, FUNCT_2, TMAP_1, TSEP_1, BORSUK_1;
theorems PRE_TOPC, XREAL_0, FUNCT_2, INT_1, SIN_COS, EUCLID, JGRAPH_1,
SQUARE_1, TOPREAL9, TOPALG_1, GOBOARD6, TOPS_2, GRCAT_1, BORSUK_3,
FUNCT_1, XCMPLX_1, TOPRNS_1, ABSVALUE, TOPMETR, JGRAPH_2, BORSUK_4,
RELAT_1, FUNCOP_1, TOPREAL3, TOPREAL6, FCONT_1, TARSKI, PCOMPS_1,
ZFMISC_1, TSEP_1, HILBERT3, TMAP_1, XBOOLE_1, SPPOL_2, COMPLEX2, JORDAN6,
COMPTS_1, JORDAN16, JGRAPH_3, COMPTRIG, CONNSP_2, XBOOLE_0, RCOMP_1,
TOPS_1, GOBOARD9, TOPALG_3, TOPGRP_1, T_0TOPSP, JGRAPH_6, TOPREAL2,
SIN_COS6, BORSUK_5, PSCOMP_1, TOPREALA, XREAL_1, XXREAL_0, VALUED_1,
XXREAL_1, RLVECT_1, ORDINAL1, JORDAN5A, RLVECT_4;
schemes FUNCT_2, INT_1;
begin :: Preliminaries
set P2 = 2*PI;
set o = |[0,0]|;
set R = the carrier of R^1;
Lm1: 0 in INT by INT_1:def 1;
reconsider p0 = -1 as negative Real;
reconsider p1 = 1 as positive Real;
set CIT = Closed-Interval-TSpace(-1,1);
set cCIT = the carrier of CIT;
Lm2: cCIT = [. -1,1 .] by TOPMETR:18;
Lm3: 1-0 <= 1;
Lm4: 3/2-1/2 <= 1;
reserve n for Element of NAT,
i for Integer,
a, b, r for Real,
x for Point of TOP-REAL n;
registration
cluster ].0,1.[ -> non empty;
coherence;
cluster [.-1,1.] -> non empty;
coherence;
cluster ].1/2,3/2.[ -> non empty;
coherence
proof
].1/2,1/2+p1.[ is non empty;
hence thesis;
end;
end;
Lm5: PI/2 < PI/1 by XREAL_1:76;
Lm6: 1*PI < 3/2*PI by XREAL_1:68;
Lm7: 3/2*PI < 2*PI by XREAL_1:68;
Lm8: for X being non empty TopSpace, Y being non empty SubSpace of X, Z being
non empty SubSpace of Y, p being Point of Z holds p is Point of X
proof
let X be non empty TopSpace, Y be non empty SubSpace of X, Z be non empty
SubSpace of Y, p be Point of Z;
p is Point of Y by PRE_TOPC:25;
hence thesis by PRE_TOPC:25;
end;
Lm9: for X being TopSpace, Y being SubSpace of X, Z being SubSpace of Y, A
being Subset of Z holds A is Subset of X
proof
let X be TopSpace, Y be SubSpace of X, Z be SubSpace of Y, A be Subset of Z;
the carrier of Z is Subset of Y by TSEP_1:1;
then
A1: A is Subset of Y by XBOOLE_1:1;
the carrier of Y is Subset of X by TSEP_1:1;
hence thesis by A1,XBOOLE_1:1;
end;
registration
cluster sin -> continuous;
coherence;
cluster cos -> continuous;
coherence;
cluster arcsin -> continuous;
coherence by RELAT_1:69,SIN_COS6:63,84;
cluster arccos -> continuous;
coherence by RELAT_1:69,SIN_COS6:86,107;
end;
theorem Th1:
sin(a*r+b) = (sin*AffineMap(a,b)).r
proof
A1: r in REAL by XREAL_0:def 1;
thus sin(a*r+b) = sin.(a*r+b) by SIN_COS:def 17
.= sin.(AffineMap(a,b).r) by FCONT_1:def 4
.= (sin*AffineMap(a,b)).r by A1,FUNCT_2:15;
end;
theorem Th2:
cos(a*r+b) = (cos*AffineMap(a,b)).r
proof
A1: r in REAL by XREAL_0:def 1;
thus cos(a*r+b) = cos.(a*r+b) by SIN_COS:def 19
.= cos.(AffineMap(a,b).r) by FCONT_1:def 4
.= (cos*AffineMap(a,b)).r by A1,FUNCT_2:15;
end;
registration
let a be non zero Real, b be Real;
cluster AffineMap(a,b) -> onto one-to-one;
coherence
by FCONT_1:55,FCONT_1:50;
end;
definition
let a, b be Real;
func IntIntervals(a,b) -> set equals
the set of all ]. a+n, b+n .[ where n is Element of INT;
coherence;
end;
theorem
for x being set holds x in IntIntervals(a,b) iff ex n being Element of
INT st x = ]. a+n, b+n .[;
registration
let a, b be Real;
cluster IntIntervals(a,b) -> non empty;
coherence
proof
]. a+0, b+0 .[ in IntIntervals(a,b) by Lm1;
hence thesis;
end;
end;
theorem
b-a <= 1 implies IntIntervals(a,b) is mutually-disjoint
proof
assume
A1: b-a <= 1;
A2: now
let k be Element of NAT;
A3: a+1+0 <= a+1+k by XREAL_1:6;
b-a+a <= 1+a by A1,XREAL_1:6;
hence a+(k+1) >= b by A3,XXREAL_0:2;
end;
let x, y be set;
assume x in IntIntervals(a,b);
then consider nx being Element of INT such that
A4: x = ].a+nx,b+nx.[;
assume y in IntIntervals(a,b);
then consider ny being Element of INT such that
A5: y = ].a+ny,b+ny.[;
assume
A6: x <> y;
assume x meets y;
then consider z being object such that
A7: z in x and
A8: z in y by XBOOLE_0:3;
reconsider z as Real by A4,A7;
A9: a+nx < z by A4,A7,XXREAL_1:4;
A10: z < b+ny by A5,A8,XXREAL_1:4;
A11: a+ny < z by A5,A8,XXREAL_1:4;
A12: z < b+nx by A4,A7,XXREAL_1:4;
per cases by XXREAL_0:1;
suppose
nx = ny;
hence contradiction by A4,A5,A6;
end;
suppose
nx < ny;
then nx+1 <= ny by INT_1:7;
then reconsider k = ny-(nx+1) as Element of NAT by INT_1:5;
a+nx+1+k < b+nx by A12,A11,XXREAL_0:2;
then a+nx+(k+1)-nx < b+nx-nx by XREAL_1:14;
then a+(k+1) < b;
hence contradiction by A2;
end;
suppose
nx > ny;
then ny+1 <= nx by INT_1:7;
then reconsider k = nx-(ny+1) as Element of NAT by INT_1:5;
a+ny+1+k < b+ny by A9,A10,XXREAL_0:2;
then a+ny+(k+1)-ny < b+ny-ny by XREAL_1:14;
then a+(k+1) < b;
hence contradiction by A2;
end;
end;
definition
let a, b be Real;
redefine func IntIntervals(a,b) -> Subset-Family of R^1; :: redefines IntIntervals (TOPREALB, definition)
coherence
proof
IntIntervals(a,b) c= bool the carrier of R^1
proof
let x be object;
assume x in IntIntervals(a,b);
then ex n being Element of INT st x = ].a+n,b+n.[;
hence thesis by TOPMETR:17;
end;
hence thesis;
end;
end;
definition
let a, b be Real;
redefine func IntIntervals(a,b) -> open Subset-Family of R^1; :: redefines IntIntervals (TOPREALB, definition)
coherence
proof
IntIntervals(a,b) is open
proof
let A be Subset of R^1;
assume A in IntIntervals(a,b);
then ex n being Element of INT st A = ].a+n,b+n.[;
hence thesis by JORDAN6:35;
end;
hence thesis;
end;
end;
begin :: Correspondence between REAL and R^1
definition
let r be Real;
func R^1(r) -> Point of R^1 equals
r;
coherence by TOPMETR:17,XREAL_0:def 1;
end;
definition
let A be Subset of REAL;
func R^1(A) -> Subset of R^1 equals
A;
coherence by TOPMETR:17;
end;
registration
let A be non empty Subset of REAL;
cluster R^1(A) -> non empty;
coherence;
end;
registration
let A be open Subset of REAL;
cluster R^1(A) -> open;
coherence by BORSUK_5:39;
end;
registration
let A be closed Subset of REAL;
cluster R^1(A) -> closed;
coherence by JORDAN5A:23;
end;
registration
let A be open Subset of REAL;
cluster R^1 | R^1(A) -> open;
coherence
by PRE_TOPC:8;
end;
registration
let A be closed Subset of REAL;
cluster R^1 | R^1(A) -> closed;
coherence
by PRE_TOPC:8;
end;
definition
let f be PartFunc of REAL,REAL;
func R^1(f) -> Function of R^1 | R^1(dom f), R^1 | R^1(rng f) equals
f;
coherence
proof
A1: the carrier of R^1 | R^1(rng f) = R^1(rng f) by PRE_TOPC:8;
the carrier of R^1 | R^1(dom f) = R^1(dom f) by PRE_TOPC:8;
hence thesis by A1,FUNCT_2:2;
end;
end;
registration
let f be PartFunc of REAL,REAL;
cluster R^1(f) -> onto;
coherence
by PRE_TOPC:8;
end;
registration
let f be one-to-one PartFunc of REAL,REAL;
cluster R^1(f) -> one-to-one;
coherence;
end;
theorem Th5:
R^1 | (R^1 [#]REAL) = R^1
proof
[#]R^1 = R^1([#]REAL) by TOPMETR:17;
hence thesis by PRE_TOPC:def 5;
end;
theorem Th6:
for f being PartFunc of REAL,REAL st dom f = REAL holds R^1|(R^1 dom f) = R^1
proof
let f be PartFunc of REAL,REAL;
assume dom f = REAL;
then [#]R^1 = R^1(dom f) by TOPMETR:17;
hence thesis by PRE_TOPC:def 5;
end;
theorem Th7:
for f being Function of REAL,REAL holds f is Function of R^1, R^1
| R^1(rng f)
proof
let f be Function of REAL,REAL;
REAL = dom f by FUNCT_2:def 1;
then R^1 | R^1(dom f) = R^1 by Th6;
then R^1(f) is Function of R^1, R^1 | R^1(rng f);
hence thesis;
end;
theorem Th8:
for f being Function of REAL,REAL holds f is Function of R^1, R^1
proof
let f be Function of REAL,REAL;
dom f = REAL by FUNCT_2:def 1;
then reconsider B = rng f as non empty Subset of REAL by RELAT_1:42;
f is Function of R^1, R^1 | R^1(B) by Th7;
hence thesis by TOPREALA:7;
end;
Lm10: sin is Function of R^1,R^1
proof
A1: sin = R^1(sin);
R^1|(R^1 dom sin) = R^1 by Th6,SIN_COS:24;
hence thesis by A1,COMPTRIG:28,TOPREALA:7;
end;
Lm11: cos is Function of R^1,R^1
proof
A1: cos = R^1(cos);
R^1|(R^1 dom cos) = R^1 by Th6,SIN_COS:24;
hence thesis by A1,COMPTRIG:29,TOPREALA:7;
end;
registration
let f be continuous PartFunc of REAL,REAL;
cluster R^1(f) -> continuous;
coherence
proof
set g = R^1(f);
per cases;
suppose
dom f is non empty;
then reconsider A = dom f, B = rng f as non empty Subset of REAL by
RELAT_1:42;
reconsider g as Function of R^1|R^1(A),R^1|R^1(B);
reconsider h = g as Function of R^1|R^1(A),R^1 by TOPREALA:7;
for x being Point of R^1|R^1(A) holds h is_continuous_at x
proof
let x be Point of R^1|R^1(A);
let G be a_neighborhood of h.x;
consider Z being Neighbourhood of (f.x qua Real) such that
A1: Z c= G by TOPREALA:20;
reconsider xx = x as Point of R^1 by PRE_TOPC:25;
the carrier of R^1|R^1(A) = A by PRE_TOPC:8;
then f is_continuous_in x by FCONT_1:def 2;
then consider N being Neighbourhood of x such that
A2: f.:N c= Z by FCONT_1:5;
consider g being Real such that
A3: 0 < g and
A4: N = ].x-g,x+g.[ by RCOMP_1:def 6;
A5: x+0 < x+g by A3,XREAL_1:6;
reconsider NN = N as open Subset of R^1 by A4,JORDAN6:35,TOPMETR:17;
reconsider M = NN /\ [#](R^1|R^1(A)) as Subset of R^1|R^1(A);
A6: NN = Int NN by TOPS_1:23;
x-g < x-0 by A3,XREAL_1:15;
then xx in Int NN by A4,A6,A5,XXREAL_1:4;
then NN is open a_neighborhood of xx by CONNSP_2:def 1;
then reconsider M as open a_neighborhood of x by TOPREALA:5;
take M;
h.:M c= h.:NN by RELAT_1:123,XBOOLE_1:17;
then h.:M c= Z by A2;
hence thesis by A1;
end;
then h is continuous by TMAP_1:44;
hence thesis by PRE_TOPC:27;
end;
suppose
dom f is empty;
hence thesis;
end;
end;
end;
set A = R^1(].0,1.[);
Lm12: now
let a be non zero Real, b be Real;
A1: rng AffineMap(a,b) = REAL by FCONT_1:55;
A2: [#]R^1 = REAL by TOPMETR:17;
dom AffineMap(a,b) = REAL by FUNCT_2:def 1;
hence R^1 = R^1|R^1(dom AffineMap(a,b)) & R^1 = R^1|R^1(rng AffineMap(a,b))
by A1,A2,TSEP_1:3;
end;
registration
let a be non zero Real, b be Real;
cluster R^1(AffineMap(a,b)) -> open;
coherence
proof
let A be Subset of R^1|R^1(dom AffineMap(a,b));
A1: R^1 = R^1|R^1(dom AffineMap(a,b)) by Lm12;
A2: R^1 = R^1|R^1(rng AffineMap(a,b)) by Lm12;
R^1(AffineMap(a,b)) is being_homeomorphism by A1,A2,JORDAN16:20;
hence thesis by A1,A2,TOPGRP_1:25;
end;
end;
begin :: Circles
definition
let S be SubSpace of TOP-REAL 2;
attr S is being_simple_closed_curve means
:Def5:
the carrier of S is Simple_closed_curve;
end;
registration
cluster being_simple_closed_curve -> non empty pathwise_connected compact
for SubSpace of TOP-REAL 2;
coherence
proof
let S be SubSpace of TOP-REAL 2;
assume
A1: the carrier of S is Simple_closed_curve;
then reconsider A = the carrier of S as Simple_closed_curve;
A is non empty;
hence the carrier of S is non empty;
thus S is pathwise_connected by A1,TOPALG_3:10;
[#]S = A;
then [#]S is compact by COMPTS_1:2;
hence thesis by COMPTS_1:1;
end;
end;
registration
let r be positive Real, x be Point of TOP-REAL 2;
cluster Sphere(x,r) -> being_simple_closed_curve;
coherence
proof
reconsider a = x as Point of Euclid 2 by TOPREAL3:8;
A1: x = |[x`1,x`2]| by EUCLID:53;
Sphere(x,r) = Sphere(a,r) by TOPREAL9:15
.= circle(x`1,x`2,r) by A1,TOPREAL9:49
.= {w where w is Point of TOP-REAL 2: |.w- |[x`1,x`2]| .| = r} by
JGRAPH_6:def 5;
hence thesis by JGRAPH_6:23;
end;
end;
definition
let n be Nat, x be Point of TOP-REAL n, r be Real;
func Tcircle(x,r) -> SubSpace of TOP-REAL n equals
(TOP-REAL n) | Sphere(x,r);
coherence;
end;
registration
let n be non zero Nat, x be Point of TOP-REAL n,
r be non negative Real;
cluster Tcircle(x,r) -> strict non empty;
coherence;
end;
theorem Th9:
the carrier of Tcircle(x,r) = Sphere(x,r)
proof
[#]Tcircle(x,r) = Sphere(x,r) by PRE_TOPC:def 5;
hence thesis;
end;
registration
let n be Nat, x be Point of TOP-REAL n, r be zero Real;
cluster Tcircle(x,r) -> trivial;
coherence
proof
reconsider e = x as Point of Euclid n by TOPREAL3:8;
n in NAT by ORDINAL1:def 12;
then the carrier of Tcircle(x,r) = Sphere(x,r) by Th9
.= Sphere(e,r) by TOPREAL9:15
.= {e} by TOPREAL6:54;
hence thesis;
end;
end;
theorem Th10:
Tcircle(0.TOP-REAL 2,r) is SubSpace of Trectangle(-r,r,-r,r)
proof
set C = Tcircle(0.TOP-REAL 2,r);
set T = Trectangle(-r,r,-r,r);
the carrier of C c= the carrier of T
proof
let x be object;
A1: closed_inside_of_rectangle(-r,r,-r,r) = {p where p is Point of
TOP-REAL 2: -r <= p`1 & p`1 <= r & -r <= p`2 & p`2 <= r} by JGRAPH_6:def 2;
assume
A2: x in the carrier of C;
reconsider x as Point of TOP-REAL 2 by A2,PRE_TOPC:25;
the carrier of C = Sphere(0.TOP-REAL 2,r) by Th9;
then
A3: |. x .| = r by A2,TOPREAL9:12;
A4: |.x`2.| <= |. x .| by JGRAPH_1:33;
then
A5: -r <= x`2 by A3,ABSVALUE:5;
A6: |.x`1.| <= |. x .| by JGRAPH_1:33;
then
A7: x`1 <= r by A3,ABSVALUE:5;
A8: the carrier of Trectangle(-r,r,-r,r) = closed_inside_of_rectangle(-r,r
,-r,r) by PRE_TOPC:8;
A9: x`2 <= r by A3,A4,ABSVALUE:5;
-r <= x`1 by A3,A6,ABSVALUE:5;
hence thesis by A1,A8,A7,A5,A9;
end;
hence thesis by TSEP_1:4;
end;
registration
let x be Point of TOP-REAL 2, r be positive Real;
cluster Tcircle(x,r) -> being_simple_closed_curve;
coherence
by Th9;
end;
registration
cluster being_simple_closed_curve strict for SubSpace of TOP-REAL 2;
existence
proof
set x = the Point of TOP-REAL 2,r = the positive Real;
take Tcircle(x,r);
thus thesis;
end;
end;
theorem
for S, T being being_simple_closed_curve SubSpace of TOP-REAL 2 holds
S,T are_homeomorphic
proof
let S, T be being_simple_closed_curve SubSpace of TOP-REAL 2;
the TopStruct of S, the TopStruct of T are_homeomorphic
proof
reconsider A = the carrier of the TopStruct of S as Simple_closed_curve by
Def5;
consider f being Function of (TOP-REAL 2)|R^2-unit_square, (TOP-REAL 2)|A
such that
A1: f is being_homeomorphism by TOPREAL2:def 1;
A2: f" is being_homeomorphism by A1,TOPS_2:56;
A3: [#]the TopStruct of S = A;
the TopStruct of S is strict SubSpace of TOP-REAL 2 by TMAP_1:6;
then
A4: the TopStruct of S = (TOP-REAL 2)|A by A3,PRE_TOPC:def 5;
reconsider B = the carrier of the TopStruct of T as Simple_closed_curve by
Def5;
consider g being Function of (TOP-REAL 2)|R^2-unit_square, (TOP-REAL 2)|B
such that
A5: g is being_homeomorphism by TOPREAL2:def 1;
A6: [#]the TopStruct of T = B;
A7: the TopStruct of T is strict SubSpace of TOP-REAL 2 by TMAP_1:6;
then reconsider
h = g*f" as Function of the TopStruct of S, the TopStruct of T
by A4,A6,PRE_TOPC:def 5;
take h;
the TopStruct of T = (TOP-REAL 2)|B by A7,A6,PRE_TOPC:def 5;
hence thesis by A5,A4,A2,TOPS_2:57;
end;
hence thesis by TOPREALA:15;
end;
:: Unit circle
definition
let n be Nat;
func Tunit_circle(n) -> SubSpace of TOP-REAL n equals
Tcircle(0.TOP-REAL n,1);
coherence;
end;
set TUC = Tunit_circle(2);
set cS1 = the carrier of TUC;
Lm13: cS1 = Sphere(|[0,0]|,1) by Th9,EUCLID:54;
registration
let n be non zero Nat;
cluster Tunit_circle(n) -> non empty;
coherence;
end;
theorem Th12:
for n being non zero Element of NAT, x being Point of TOP-REAL
n holds x is Point of Tunit_circle(n) implies |. x .| = 1
proof
reconsider j = 1 as non negative Real;
let n be non zero Element of NAT, x be Point of TOP-REAL n;
assume x is Point of Tunit_circle(n);
then x in the carrier of Tcircle(0.TOP-REAL n,j);
then x in Sphere(0.TOP-REAL n,1) by Th9;
hence thesis by TOPREAL9:12;
end;
theorem Th13:
for x being Point of TOP-REAL 2 st x is Point of Tunit_circle(2)
holds -1 <= x`1 & x`1 <= 1 & -1 <= x`2 & x`2 <= 1
proof
let x be Point of TOP-REAL 2 such that
A1: x is Point of Tunit_circle(2);
consider a, b being Element of REAL such that
A2: x = <*a,b*> by EUCLID:51;
A3: b = x`2 by A2,EUCLID:52;
A4: a = x`1 by A2,EUCLID:52;
A5: 1^2 = |. x .|^2 by A1,Th12
.= a^2+b^2 by A4,A3,JGRAPH_3:1;
0 <= a^2 by XREAL_1:63;
then -a^2 <= -0;
then
A6: b^2-1 <= 0 by A5;
0 <= b^2 by XREAL_1:63;
then -b^2 <= -0;
then a^2-1 <= 0 by A5;
hence thesis by A4,A3,A6,SQUARE_1:43;
end;
theorem Th14:
for x being Point of TOP-REAL 2 st x is Point of Tunit_circle(2)
& x`1 = 1 holds x`2 = 0
proof
let x be Point of TOP-REAL 2 such that
A1: x is Point of Tunit_circle(2) and
A2: x`1 = 1;
1^2 = |. x .|^2 by A1,Th12
.= x`1^2+x`2^2 by JGRAPH_3:1;
hence thesis by A2;
end;
theorem Th15:
for x being Point of TOP-REAL 2 st x is Point of Tunit_circle(2)
& x`1 = -1 holds x`2 = 0
proof
let x be Point of TOP-REAL 2 such that
A1: x is Point of Tunit_circle(2) and
A2: x`1 = -1;
1^2 = |. x .|^2 by A1,Th12
.= x`1^2+x`2^2 by JGRAPH_3:1;
hence thesis by A2;
end;
theorem
for x being Point of TOP-REAL 2 st x is Point of Tunit_circle(2) & x`2
= 1 holds x`1 = 0
proof
let x be Point of TOP-REAL 2 such that
A1: x is Point of Tunit_circle(2) and
A2: x`2 = 1;
1^2 = |. x .|^2 by A1,Th12
.= x`1^2+x`2^2 by JGRAPH_3:1;
hence thesis by A2;
end;
theorem
for x being Point of TOP-REAL 2 st x is Point of Tunit_circle(2) & x`2
= -1 holds x`1 = 0
proof
let x be Point of TOP-REAL 2 such that
A1: x is Point of Tunit_circle(2) and
A2: x`2 = -1;
1^2 = |. x .|^2 by A1,Th12
.= x`1^2+x`2^2 by JGRAPH_3:1;
hence thesis by A2;
end;
set TREC = Trectangle(p0,p1,p0,p1);
theorem
Tunit_circle(2) is SubSpace of Trectangle(-1,1,-1,1) by Th10;
theorem Th19:
for n being non zero Element of NAT, r being positive Real
, x being Point of TOP-REAL n, f being Function of Tunit_circle(n),
Tcircle(x,r) st for a being Point of Tunit_circle(n), b being Point of TOP-REAL
n st a = b holds f.a = r*b+x holds f is being_homeomorphism
proof
let n be non zero Element of NAT, r be positive Real, x be Point
of TOP-REAL n, f being Function of Tunit_circle(n), Tcircle(x,r) such that
A1: for a being Point of Tunit_circle(n), b being Point of TOP-REAL n st
a = b holds f.a = r*b+x;
defpred P[Point of TOP-REAL n,set] means $2 = r*$1+x;
set U = Tunit_circle(n), C = Tcircle(x,r);
A2: for u being Point of TOP-REAL n ex y being Point of TOP-REAL n st P[u,y ];
consider F being Function of TOP-REAL n, TOP-REAL n such that
A3: for x being Point of TOP-REAL n holds P[x,F.x] from FUNCT_2:sch 3(
A2);
defpred R[Point of TOP-REAL n,set] means $2 = 1/r*($1-x);
A4: for u being Point of TOP-REAL n ex y being Point of TOP-REAL n st R[u,y ];
consider G being Function of TOP-REAL n, TOP-REAL n such that
A5: for a being Point of TOP-REAL n holds R[a,G.a] from FUNCT_2:sch 3(
A4);
set f2 = (TOP-REAL n) --> x;
set f1 = id TOP-REAL n;
dom G = the carrier of TOP-REAL n by FUNCT_2:def 1;
then
A6: dom (G|Sphere(x,r)) = Sphere(x,r) by RELAT_1:62;
for p being Point of TOP-REAL n holds G.p = 1/r * f1.p + (-1/r) * f2.p
proof
let p be Point of TOP-REAL n;
thus 1/r * f1.p + (-1/r) * f2.p = 1/r*p + (-1/r)*f2.p
.= 1/r*p + (-1/r)*x
.= 1/r*p - 1/r*x by RLVECT_1:79
.= 1/r*(p-x) by RLVECT_1:34
.= G.p by A5;
end;
then
A7: G is continuous by TOPALG_1:16;
thus dom f = [#]U by FUNCT_2:def 1;
A8: dom f = the carrier of U by FUNCT_2:def 1;
for p being Point of TOP-REAL n holds F.p = r * f1.p + 1 * f2.p
proof
let p be Point of TOP-REAL n;
thus r * f1.p + 1 * f2.p = r*f1.p + f2.p by RLVECT_1:def 8
.= r*p + f2.p
.= r*p + x
.= F.p by A3;
end;
then
A9: F is continuous by TOPALG_1:16;
A10: the carrier of C = Sphere(x,r) by Th9;
A11: the carrier of U = Sphere(0.TOP-REAL n,1) by Th9;
A12: for a being object st a in dom f holds f.a = (F|Sphere(0.TOP-REAL n,1)).a
proof
let a be object such that
A13: a in dom f;
reconsider y = a as Point of TOP-REAL n by A13,PRE_TOPC:25;
thus f.a = r*y+x by A1,A13
.= F.y by A3
.= (F|Sphere(0.TOP-REAL n,1)).a by A11,A13,FUNCT_1:49;
end;
A14: 1/r*r = 1 by XCMPLX_1:87;
thus
A15: rng f = [#]C
proof
thus rng f c= [#]C;
let b be object;
assume
A16: b in [#]C;
then reconsider c = b as Point of TOP-REAL n by PRE_TOPC:25;
set a = 1/r * (c - x);
|.a-0.TOP-REAL n.| = |.a.| by RLVECT_1:13
.= |.1/r.|*|. c-x .| by TOPRNS_1:7
.= 1/r*|. c-x .| by ABSVALUE:def 1
.= 1/r*r by A10,A16,TOPREAL9:9;
then
A17: a in Sphere(0.TOP-REAL n,1) by A14;
then f.a = r*a+x by A1,A11
.= r*(1/r)*(c-x)+x by RLVECT_1:def 7
.= c-x+x by A14,RLVECT_1:def 8
.= b by RLVECT_4:1;
hence thesis by A11,A8,A17,FUNCT_1:def 3;
end;
thus
A18: f is one-to-one
proof
let a, b be object such that
A19: a in dom f and
A20: b in dom f and
A21: f.a = f.b;
reconsider a1 = a, b1 = b as Point of TOP-REAL n by A11,A8,A19,A20;
A22: f.b1 = r*b1+x by A1,A20;
f.a1 = r*a1+x by A1,A19;
then r*a1 = r*b1+x-x by A21,A22,RLVECT_4:1;
hence thesis by RLVECT_1:36,RLVECT_4:1;
end;
A23: for a being object st a in dom (f") holds f".a = (G|Sphere(x,r)).a
proof
reconsider ff = f as Function;
let a be object such that
A24: a in dom (f");
reconsider y = a as Point of TOP-REAL n by A24,PRE_TOPC:25;
set e = 1/r * (y - x);
A25: f is onto by A15;
|.e-0.TOP-REAL n.| = |.e.| by RLVECT_1:13
.= |.1/r.|*|. y-x .| by TOPRNS_1:7
.= 1/r*|. y-x .| by ABSVALUE:def 1
.= 1/r*r by A10,A24,TOPREAL9:9;
then
A26: 1/r * (y - x) in Sphere(0.TOP-REAL n,1) by A14;
then f.e = r*e+x by A1,A11
.= r*(1/r)*(y-x)+x by RLVECT_1:def 7
.= y-x+x by A14,RLVECT_1:def 8
.= y by RLVECT_4:1;
then ff".a = 1/r * (y - x) by A11,A8,A18,A26,FUNCT_1:32;
hence f".a = 1/r*(y-x) by A25,A18,TOPS_2:def 4
.= G.y by A5
.= (G|Sphere(x,r)).a by A10,A24,FUNCT_1:49;
end;
dom F = the carrier of TOP-REAL n by FUNCT_2:def 1;
then dom (F|Sphere(0.TOP-REAL n,1)) = Sphere(0.TOP-REAL n,1) by RELAT_1:62;
hence f is continuous by A11,A8,A9,A12,BORSUK_4:44,FUNCT_1:2;
dom (f") = the carrier of C by FUNCT_2:def 1;
hence thesis by A10,A6,A7,A23,BORSUK_4:44,FUNCT_1:2;
end;
registration
cluster Tunit_circle(2) -> being_simple_closed_curve;
coherence;
end;
Lm14: for n being non zero Element of NAT, r being positive Real, x
being Point of TOP-REAL n holds Tunit_circle(n), Tcircle(x,r) are_homeomorphic
proof
let n be non zero Element of NAT, r be positive Real, x be Point
of TOP-REAL n;
set U = Tunit_circle(n), C = Tcircle(x,r);
defpred P[Point of U,set] means ex w being Point of TOP-REAL n st w = $1 &
$2 = r*w+x;
A1: the carrier of C = Sphere(x,r) by Th9;
A2: for u being Point of U ex y being Point of C st P[u,y]
proof
let u be Point of U;
reconsider v = u as Point of TOP-REAL n by PRE_TOPC:25;
set y = r*v+x;
|. y-x .| = |. r*v .| by RLVECT_4:1
.= |.r.|*|. v .| by TOPRNS_1:7
.= r*|. v .| by ABSVALUE:def 1
.= r*1 by Th12;
then reconsider y as Point of C by A1,TOPREAL9:9;
take y;
thus thesis;
end;
consider f being Function of U,C such that
A3: for x being Point of U holds P[x,f.x] from FUNCT_2:sch 3(A2);
take f;
for a being Point of U, b being Point of TOP-REAL n st a = b holds f.a =
r*b+x
proof
let a be Point of U, b be Point of TOP-REAL n;
P[a,f.a] by A3;
hence thesis;
end;
hence thesis by Th19;
end;
theorem
for n being non zero Element of NAT, r, s being positive Real,
x, y being Point of TOP-REAL n holds
Tcircle(x,r), Tcircle(y,s) are_homeomorphic
proof
let n be non zero Element of NAT, r, s be positive Real, x, y be
Point of TOP-REAL n;
A1: Tunit_circle(n), Tcircle(y,s) are_homeomorphic by Lm14;
Tcircle(x,r), Tunit_circle(n) are_homeomorphic by Lm14;
hence thesis by A1,BORSUK_3:3;
end;
registration
let x be Point of TOP-REAL 2, r be non negative Real;
cluster Tcircle(x,r) -> pathwise_connected;
coherence
proof
per cases;
suppose
r is positive;
then reconsider r as positive Real;
Tcircle(x,r) is pathwise_connected;
hence thesis;
end;
suppose
r is non positive;
then reconsider r as non negative non positive Real;
Tcircle(x,r) is trivial;
hence thesis;
end;
end;
end;
:: Open unit circle
definition
func c[10] -> Point of Tunit_circle(2) equals
|[1,0]|;
coherence
proof
A1: |[1,0]|`2 = 0 by EUCLID:52;
A2: |[1,0]|`1 = 1 by EUCLID:52;
|. |[1+0,0+0]| - o .| = |.|[1,0]|+o- o.| by EUCLID:56
.= |.|[1,0]|+(o-o).| by RLVECT_1:def 3
.= |.|[1,0]|+(0.TOP-REAL 2).| by RLVECT_1:5
.= |.|[1,0]|.| by RLVECT_1:4
.= sqrt(1^2+0^2) by A2,A1,JGRAPH_1:30
.= 1;
hence thesis by Lm13,TOPREAL9:9;
end;
func c[-10] -> Point of Tunit_circle(2) equals
|[-1,0]|;
coherence
proof
A3: |[-1,0]|`2 = 0 by EUCLID:52;
A4: |[-1,0]|`1 = -1 by EUCLID:52;
|. |[-1+0,0+0]| - o .| = |.|[-1,0]|+o- o.| by EUCLID:56
.= |.|[-1,0]|+(o-o).| by RLVECT_1:def 3
.= |.|[-1,0]|+(0.TOP-REAL 2).| by RLVECT_1:5
.= |.|[-1,0]|.| by RLVECT_1:4
.= sqrt((-1)^2+0^2) by A4,A3,JGRAPH_1:30
.= sqrt(1^2+0^2)
.= 1;
hence thesis by Lm13,TOPREAL9:9;
end;
end;
Lm15: c[10] <> c[-10] by SPPOL_2:1;
definition
let p be Point of Tunit_circle(2);
func Topen_unit_circle(p) -> strict SubSpace of Tunit_circle(2) means
:Def10
:
the carrier of it = (the carrier of Tunit_circle(2)) \ {p};
existence
proof
reconsider A = cS1 \ {p} as Subset of TUC;
take TUC|A;
thus thesis by PRE_TOPC:8;
end;
uniqueness by TSEP_1:5;
end;
registration
let p be Point of Tunit_circle(2);
cluster Topen_unit_circle(p) -> non empty;
coherence
proof
set X = Topen_unit_circle(p);
A1: the carrier of X = cS1 \ {p} by Def10;
per cases;
suppose
A2: p = c[10];
set x = |[0,1]|;
reconsider r = p as Point of TOP-REAL 2 by PRE_TOPC:25;
A3: x`1 = 0 by EUCLID:52;
A4: x`2 = 1 by EUCLID:52;
|. |[0+0,1+0]| - o .| = |.x+o- o.| by EUCLID:56
.= |.x+(o-o).| by RLVECT_1:def 3
.= |.x+(0.TOP-REAL 2).| by RLVECT_1:5
.= |. x .| by RLVECT_1:4
.= sqrt(1^2+0^2) by A3,A4,JGRAPH_1:30
.= 1;
then
A5: x in cS1 by Lm13;
r`1 = 1 by A2,EUCLID:52;
then not x in {p} by A3,TARSKI:def 1;
hence the carrier of X is non empty by A1,A5,XBOOLE_0:def 5;
end;
suppose
p <> c[10];
then not c[10] in {p} by TARSKI:def 1;
hence the carrier of X is non empty by A1,XBOOLE_0:def 5;
end;
end;
end;
theorem Th21:
for p being Point of Tunit_circle(2) holds p is not Point of
Topen_unit_circle(p)
proof
let p be Point of Tunit_circle(2);
A1: p in {p} by TARSKI:def 1;
the carrier of Topen_unit_circle(p) = (the carrier of Tunit_circle(2)) \
{p} by Def10;
hence thesis by A1,XBOOLE_0:def 5;
end;
theorem Th22:
for p being Point of Tunit_circle(2) holds Topen_unit_circle(p)
= (Tunit_circle(2)) | (([#]Tunit_circle(2)) \ {p})
proof
let p be Point of Tunit_circle(2);
[#]Topen_unit_circle(p) = ([#]Tunit_circle(2)) \ {p} by Def10;
hence thesis by PRE_TOPC:def 5;
end;
theorem Th23:
for p, q being Point of Tunit_circle(2) st p <> q holds q is
Point of Topen_unit_circle(p)
proof
let p, q be Point of Tunit_circle(2) such that
A1: p <> q;
the carrier of Topen_unit_circle(p) = (the carrier of Tunit_circle(2)) \
{p } by Def10;
hence thesis by A1,ZFMISC_1:56;
end;
theorem Th24:
for p being Point of TOP-REAL 2 st p is Point of
Topen_unit_circle(c[10]) & p`2 = 0 holds p = c[-10]
proof
let p be Point of TOP-REAL 2 such that
A1: p is Point of Topen_unit_circle(c[10]) and
A2: p`2 = 0;
A3: now
assume p`1 = 1;
then p = c[10] by A2,EUCLID:53;
hence contradiction by A1,Th21;
end;
p is Point of TUC by A1,PRE_TOPC:25;
then 1^2 = |. p .|^2 by Th12
.= p`1^2+p`2^2 by JGRAPH_3:1;
then p`1 = 1 or p`1 = -1 by A2,SQUARE_1:41;
hence thesis by A2,A3,EUCLID:53;
end;
theorem Th25:
for p being Point of TOP-REAL 2 st p is Point of
Topen_unit_circle(c[-10]) & p`2 = 0 holds p = c[10]
proof
let p be Point of TOP-REAL 2 such that
A1: p is Point of Topen_unit_circle(c[-10]) and
A2: p`2 = 0;
A3: now
assume p`1 = -1;
then p = c[-10] by A2,EUCLID:53;
hence contradiction by A1,Th21;
end;
p is Point of TUC by A1,PRE_TOPC:25;
then 1^2 = |. p .|^2 by Th12
.= p`1^2+p`2^2 by JGRAPH_3:1;
then p`1 = 1 or p`1 = -1 by A2,SQUARE_1:41;
hence thesis by A2,A3,EUCLID:53;
end;
set TOUC = Topen_unit_circle(c[10]);
set TOUCm = Topen_unit_circle(c[-10]);
set X = the carrier of TOUC;
set Xm = the carrier of TOUCm;
set Y = the carrier of (R^1|R^1(].0,0+p1.[));
set Ym = the carrier of (R^1|R^1(].1/2,1/2+p1.[));
Lm16: X = [#]TOUC;
Lm17: Xm = [#]TOUCm;
theorem Th26:
for p being Point of Tunit_circle(2), x being Point of TOP-REAL
2 st x is Point of Topen_unit_circle(p) holds -1 <= x`1 & x`1 <= 1 & -1 <= x`2
& x`2 <= 1
proof
let p be Point of Tunit_circle(2), x be Point of TOP-REAL 2;
assume x is Point of Topen_unit_circle(p);
then
A1: x in the carrier of Topen_unit_circle(p);
the carrier of Topen_unit_circle(p) is Subset of cS1 by TSEP_1:1;
hence thesis by A1,Th13;
end;
theorem Th27:
for x being Point of TOP-REAL 2 st x is Point of
Topen_unit_circle(c[10]) holds -1 <= x`1 & x`1 < 1
proof
let x be Point of TOP-REAL 2;
assume
A1: x is Point of Topen_unit_circle(c[10]);
A2: now
A3: the carrier of TOUC = cS1 \ {c[10]} by Def10;
then
A4: not x in {c[10]} by A1,XBOOLE_0:def 5;
A5: x = |[x`1,x`2]| by EUCLID:53;
assume
A6: x`1 = 1;
x in cS1 by A1,A3,XBOOLE_0:def 5;
then x = c[10] by A6,A5,Th14;
hence contradiction by A4,TARSKI:def 1;
end;
x`1 <= 1 by A1,Th26;
hence thesis by A1,A2,Th26,XXREAL_0:1;
end;
theorem Th28:
for x being Point of TOP-REAL 2 st x is Point of
Topen_unit_circle(c[-10]) holds -1 < x`1 & x`1 <= 1
proof
let x be Point of TOP-REAL 2;
assume
A1: x is Point of Topen_unit_circle(c[-10]);
A2: now
A3: the carrier of TOUCm = cS1 \ {c[-10]} by Def10;
then
A4: not x in {c[-10]} by A1,XBOOLE_0:def 5;
A5: x = |[x`1,x`2]| by EUCLID:53;
assume
A6: x`1 = -1;
x in cS1 by A1,A3,XBOOLE_0:def 5;
then x = c[-10] by A6,A5,Th15;
hence contradiction by A4,TARSKI:def 1;
end;
-1 <= x`1 by A1,Th26;
hence thesis by A1,A2,Th26,XXREAL_0:1;
end;
registration
let p be Point of Tunit_circle(2);
cluster Topen_unit_circle(p) -> open;
coherence
proof
let A be Subset of TUC;
assume A = the carrier of Topen_unit_circle(p);
then
A1: A` = cS1 \ (cS1 \ {p}) by Def10
.= cS1 /\ {p} by XBOOLE_1:48
.= {p} by ZFMISC_1:46;
TUC is T_2 by TOPMETR:2;
then A` is closed by A1,PCOMPS_1:7;
hence thesis by TOPS_1:4;
end;
end;
theorem
for p being Point of Tunit_circle(2) holds Topen_unit_circle(p), I(01)
are_homeomorphic
proof
set D = Sphere(0.TOP-REAL 2,p1);
let p be Point of Tunit_circle(2);
set P = Topen_unit_circle(p);
reconsider p2 = p as Point of TOP-REAL 2 by PRE_TOPC:25;
D\{p} c= D by XBOOLE_1:36;
then reconsider A = D\{p} as Subset of Tcircle(0.TOP-REAL 2,1) by Th9;
P = Tcircle(0.TOP-REAL 2,1) | A by Lm13,Th22,EUCLID:54
.= (TOP-REAL 2) | (D \ {p2}) by GOBOARD9:2;
hence thesis by Lm13,BORSUK_4:52,EUCLID:54;
end;
theorem
for p, q being Point of Tunit_circle(2) holds Topen_unit_circle(p),
Topen_unit_circle(q) are_homeomorphic
proof
set D = Sphere(0.TOP-REAL 2,p1);
let p, q be Point of Tunit_circle(2);
set P = Topen_unit_circle(p);
set Q = Topen_unit_circle(q);
reconsider p2 = p, q2 = q as Point of TOP-REAL 2 by PRE_TOPC:25;
A1: D\{q} c= D by XBOOLE_1:36;
D\{p} c= D by XBOOLE_1:36;
then reconsider
A = D\{p}, B = D\{q} as Subset of Tcircle(0.TOP-REAL 2,1) by A1,Th9;
A2: Q = Tcircle(0.TOP-REAL 2,1) | B by Lm13,Th22,EUCLID:54
.= (TOP-REAL 2) | (D \ {q2}) by GOBOARD9:2;
P = Tcircle(0.TOP-REAL 2,1) | A by Lm13,Th22,EUCLID:54
.= (TOP-REAL 2) | (D \ {p2}) by GOBOARD9:2;
hence thesis by A2,Lm13,BORSUK_4:53,EUCLID:54;
end;
begin :: Correspondence between the real line and circles
definition
func CircleMap -> Function of R^1, Tunit_circle(2) means
:Def11:
for x being Real holds it.x = |[ cos(2*PI*x), sin(2*PI*x) ]|;
existence
proof
defpred P[Real,set] means $2 = |[ cos(2*PI*$1), sin(2*PI*$1) ]|;
A1: for x being Element of R^1 ex y being Element of cS1 st P[x,y]
proof
let x be Element of R^1;
set y = |[ cos(2*PI*x), sin(2*PI*x) ]|;
|. y - o .| = |. y .| by EUCLID:54,RLVECT_1:13
.= sqrt((y`1)^2+(y`2)^2) by JGRAPH_1:30
.= sqrt((cos(2*PI*x))^2+(y`2)^2) by EUCLID:52
.= sqrt((cos(2*PI*x))^2+(sin(2*PI*x))^2) by EUCLID:52
.= 1 by SIN_COS:29,SQUARE_1:18;
then y is Element of cS1 by Lm13,TOPREAL9:9;
hence thesis;
end;
consider f being Function of R, cS1 such that
A2: for x being Element of R^1 holds P[x,f.x] from FUNCT_2:sch 3(A1);
take f;
let x be Real;
x is Point of R^1 by TOPMETR:17,XREAL_0:def 1;
hence thesis by A2;
end;
uniqueness
proof
let f, g be Function of R^1, TUC such that
A3: for x being Real holds f.x = |[cos(2*PI*x),sin(2*PI*x)]| and
A4: for x being Real holds g.x = |[cos(2*PI*x),sin(2*PI*x)]|;
for x being Point of R^1 holds f.x = g.x
proof
let x be Point of R^1;
thus f.x = |[cos(2*PI*x),sin(2*PI*x)]| by A3
.= g.x by A4;
end;
hence f = g;
end;
end;
Lm18: dom CircleMap = REAL by FUNCT_2:def 1,TOPMETR:17;
theorem Th31:
CircleMap.r = CircleMap.(r+i)
proof
defpred P[Integer] means CircleMap.r = CircleMap.(r+$1);
A1: for i holds P[i] implies P[i-1] & P[i+1]
proof
let i such that
A2: P[i];
thus CircleMap.(r+(i-1)) = |[ cos(2*PI*(r+i-1)), sin(2*PI*(r+i-1)) ]| by
Def11
.= |[ cos(2*PI*(r+i)), sin(2*PI*(r+i)+2*PI*(-1)) ]| by COMPLEX2:9
.= |[ cos(2*PI*(r+i)), sin(2*PI*(r+i)) ]| by COMPLEX2:8
.= CircleMap.r by A2,Def11;
thus CircleMap.(r+(i+1)) = |[ cos(2*PI*(r+i+1)), sin(2*PI*(r+i+1)) ]| by
Def11
.= |[ cos(2*PI*(r+i)), sin(2*PI*(r+i)+2*PI*1) ]| by COMPLEX2:9
.= |[ cos(2*PI*(r+i)), sin(2*PI*(r+i)) ]| by COMPLEX2:8
.= CircleMap.r by A2,Def11;
end;
A3: P[0];
for i holds P[i] from INT_1:sch 4(A3,A1);
hence thesis;
end;
theorem Th32:
CircleMap.i = c[10]
proof
thus CircleMap.i = |[ cos(2*PI*i+0), sin(2*PI*i) ]| by Def11
.= |[ cos(0), sin(2*PI*i+0) ]| by COMPLEX2:9
.= c[10] by COMPLEX2:8,SIN_COS:31;
end;
theorem Th33:
CircleMap"{c[10]} = INT
proof
hereby
let i be object;
assume
A1: i in CircleMap"{c[10]};
then reconsider x = i as Real;
CircleMap.i in {c[10]} by A1,FUNCT_2:38;
then CircleMap.i = c[10] by TARSKI:def 1;
then |[ cos(2*PI*x), sin(2*PI*x) ]| = |[1,0]| by Def11;
then cos(2*PI*x) = 1 by SPPOL_2:1;
hence i in INT by SIN_COS6:44;
end;
let i be object;
assume i in INT;
then reconsider i as Integer;
CircleMap.i = c[10] by Th32;
then
A2: CircleMap.i in {c[10]} by TARSKI:def 1;
i in R by TOPMETR:17,XREAL_0:def 1;
hence thesis by A2,FUNCT_2:38;
end;
Lm19: CircleMap.(1/2) = |[-1,0]|
proof
thus CircleMap.(1/2) = |[ cos(2*PI*(1/2)), sin(2*PI*(1/2)) ]| by Def11
.= |[-1,0]| by SIN_COS:77;
end;
theorem Th34:
frac r = 1/2 implies CircleMap.r = |[-1,0]|
proof
assume
A1: frac r = 1/2;
thus CircleMap.r = CircleMap.(r+-[\r/]) by Th31
.= CircleMap.(r-[\r/])
.= |[-1,0]| by A1,Lm19,INT_1:def 8;
end;
theorem
frac r = 1/4 implies CircleMap.r = |[0,1]|
proof
assume frac r = 1/4;
then
A1: r-[\r/] = 1/4 by INT_1:def 8;
thus CircleMap.r = CircleMap.(r+-[\r/]) by Th31
.= |[ cos(2*PI*(1/4)), sin(2*PI*(1/4)) ]| by A1,Def11
.= |[0,1]| by SIN_COS:77;
end;
theorem
frac r = 3/4 implies CircleMap.r = |[0,-1]|
proof
assume frac r = 3/4;
then
A1: r-[\r/] = 3/4 by INT_1:def 8;
thus CircleMap.r = CircleMap.(r+-[\r/]) by Th31
.= |[ cos(2*PI*(3/4)), sin(2*PI*(3/4)) ]| by A1,Def11
.= |[0,-1]| by SIN_COS:77;
end;
Lm20: CircleMap.r = |[ (cos*AffineMap(2*PI,0)).r, (sin*AffineMap(2*PI,0)).r ]|
proof
thus CircleMap.r = |[ cos(2*PI*r+0), sin(2*PI*r) ]| by Def11
.= |[ (cos*AffineMap(2*PI,0)).r, sin(2*PI*r+0) ]| by Th2
.= |[ (cos*AffineMap(2*PI,0)).r, (sin*AffineMap(2*PI,0)).r ]| by Th1;
end;
theorem
for i, j being Integer holds CircleMap.r = |[ (cos*AffineMap(2*PI,2*PI
*i)).r, (sin*AffineMap(2*PI,2*PI*j)).r ]|
proof
let i, j be Integer;
thus CircleMap.r = |[ cos(2*PI*r+0), sin(2*PI*r) ]| by Def11
.= |[ cos(2*PI*r+2*PI*i), sin(2*PI*r+0) ]| by COMPLEX2:9
.= |[ cos(2*PI*r+2*PI*i), sin(2*PI*r+2*PI*j) ]| by COMPLEX2:8
.= |[ (cos*AffineMap(2*PI,2*PI*i)).r, sin(2*PI*r+2*PI*j) ]| by Th2
.= |[ (cos*AffineMap(2*PI,2*PI*i)).r, (sin*AffineMap(2*PI,2*PI*j)).r ]|
by Th1;
end;
registration
cluster CircleMap -> continuous;
coherence
proof
reconsider l = AffineMap(2*PI,0) as Function of R^1,R^1 by Th8;
set sR = R^1(sin), cR = R^1(cos);
A1: dom AffineMap(2*PI,0) = REAL by FUNCT_2:def 1;
reconsider sR, cR as Function of R^1,R^1 by Lm10,Lm11;
A2: AffineMap(2*PI,0) = R^1(AffineMap(2*PI,0));
reconsider g = CircleMap as Function of R^1,TOP-REAL 2 by TOPREALA:7;
A3: rng AffineMap(2*PI,0) = [#]REAL by FCONT_1:55;
set c = cR*l;
set s = sR*l;
A4: R^1|(R^1 dom cos) = R^1 by Th6,SIN_COS:24;
A5: R^1|(R^1 dom sin) = R^1 by Th6,SIN_COS:24;
for p being Point of R^1, V being Subset of TOP-REAL 2 st g.p in V & V
is open ex W being Subset of R^1 st p in W & W is open & g.:W c= V
proof
let p be Point of R^1, V be Subset of TOP-REAL 2 such that
A6: g.p in V and
A7: V is open;
reconsider e = g.p as Point of Euclid 2 by TOPREAL3:8;
V = Int V by A7,TOPS_1:23;
then consider r being Real such that
A8: r > 0 and
A9: Ball(e,r) c= V by A6,GOBOARD6:5;
set B = ].(g.p)`2-r/sqrt 2,(g.p)`2+r/sqrt 2.[;
set A = ].(g.p)`1-r/sqrt 2,(g.p)`1+r/sqrt 2.[;
set F = (1,2) --> (A,B);
reconsider A, B as Subset of R^1 by TOPMETR:17;
A10: B is open by JORDAN6:35;
A11: product F c= Ball(e,r) by TOPREAL6:41;
A12: cR is continuous by A4,PRE_TOPC:26;
A13: sR is continuous by A5,PRE_TOPC:26;
A14: g.p = |[ c.p, s.p ]| by Lm20;
then (g.p)`2 = s.p by EUCLID:52;
then s.p in B by A8,SQUARE_1:19,TOPREAL6:15;
then consider Ws being Subset of R^1 such that
A15: p in Ws and
A16: Ws is open and
A17: s.:Ws c= B by A2,A1,A3,A10,A13,Th5,JGRAPH_2:10;
A18: A is open by JORDAN6:35;
(g.p)`1 = c.p by A14,EUCLID:52;
then c.p in A by A8,SQUARE_1:19,TOPREAL6:15;
then consider Wc being Subset of R^1 such that
A19: p in Wc and
A20: Wc is open and
A21: c.:Wc c= A by A2,A1,A3,A18,A12,Th5,JGRAPH_2:10;
set W = Ws /\ Wc;
take W;
thus p in W by A15,A19,XBOOLE_0:def 4;
thus W is open by A16,A20;
let y be object;
assume y in g.:W;
then consider x being Element of R^1 such that
A22: x in W and
A23: y = g.x by FUNCT_2:65;
x in Ws by A22,XBOOLE_0:def 4;
then
A24: s.x in s.:Ws by FUNCT_2:35;
x in Wc by A22,XBOOLE_0:def 4;
then
A25: c.x in c.:Wc by FUNCT_2:35;
|[c.x,s.x]| = (1,2) --> (c.x,s.x) by TOPREALA:28;
then |[c.x,s.x]| in product F by A17,A21,A24,A25,HILBERT3:11;
then
A26: |[c.x,s.x]| in Ball(e,r) by A11;
g.x = |[ c.x, s.x ]| by Lm20;
hence thesis by A9,A23,A26;
end;
then g is continuous by JGRAPH_2:10;
hence thesis by PRE_TOPC:27;
end;
end;
Lm21: for A being Subset of R^1 holds CircleMap|A is Function of R^1|A,
Tunit_circle(2)
proof
let A be Subset of R^1;
A1: rng (CircleMap|A) c= cS1;
dom (CircleMap|A) = A by Lm18,RELAT_1:62,TOPMETR:17
.= the carrier of R^1|A by PRE_TOPC:8;
hence thesis by A1,FUNCT_2:2;
end;
Lm22: -1 <= r & r <= 1 implies 0 <= arccos r/(2*PI) & arccos r/(2*PI) <= 1/2
proof
assume that
A1: -1 <= r and
A2: r <= 1;
arccos r <= PI by A1,A2,SIN_COS6:99;
then
A3: arccos r/(2*PI) <= 1*PI/(2*PI) by XREAL_1:72;
0 <= arccos r by A1,A2,SIN_COS6:99;
hence thesis by A3,XCMPLX_1:91;
end;
theorem Th38:
for A being Subset of R^1, f being Function of R^1|A,
Tunit_circle(2) st [.0,1.[ c= A & f = CircleMap | A holds f is onto
proof
let A be Subset of R^1, f be Function of R^1|A, Tunit_circle(2) such that
A1: [.0,1.[ c= A and
A2: f = CircleMap | A;
A3: dom f = A by A2,Lm18,RELAT_1:62,TOPMETR:17;
thus rng f c= cS1;
let y be object;
assume
A4: y in cS1;
then reconsider z = y as Point of TOP-REAL 2 by PRE_TOPC:25;
set z1 = z`1, z2 = z`2;
A5: z1 <= 1 by A4,Th13;
set x = arccos z1/(2*PI);
A6: -1 <= z1 by A4,Th13;
then
A7: 0 <= x by A5,Lm22;
x <= 1/2 by A6,A5,Lm22;
then
A8: x < 1 by XXREAL_0:2;
A9: z1^2 + z2^2 = |. z .|^2 by JGRAPH_1:29;
A10: |. z .| = 1 by A4,Th12;
per cases;
suppose
A11: z2 < 0;
now
assume x = 0;
then arccos z1 = 0;
then z1 = 1 by A6,A5,SIN_COS6:96;
hence contradiction by A10,A9,A11;
end;
then
A12: 1-0 > 1-x by A7,XREAL_1:15;
1-x > 1-1 by A8,XREAL_1:15;
then
A13: 1-x in [.0,1.[ by A12,XXREAL_1:3;
then f.(1-x) = CircleMap.(-x+1) by A1,A2,FUNCT_1:49
.= CircleMap.-x by Th31
.= |[cos(-2*PI*x), sin(2*PI*(-x))]| by Def11
.= |[cos(2*PI*x), sin(2*PI*(-x))]| by SIN_COS:31
.= |[cos arccos z1, sin(-2*PI*x)]| by XCMPLX_1:87
.= |[cos arccos z1, -sin(2*PI*x)]| by SIN_COS:31
.= |[cos arccos z1, -sin arccos z1]| by XCMPLX_1:87
.= |[z1, -sin arccos z1]| by A6,A5,SIN_COS6:91
.= |[z1, --z2]| by A10,A9,A11,SIN_COS6:103
.= y by EUCLID:53;
hence thesis by A1,A3,A13,FUNCT_1:def 3;
end;
suppose
A14: z2 >= 0;
A15: x in [.0,1.[ by A7,A8,XXREAL_1:3;
then f.x = CircleMap.x by A1,A2,FUNCT_1:49
.= |[cos(2*PI*x), sin(2*PI*x)]| by Def11
.= |[cos arccos z1, sin(2*PI*x)]| by XCMPLX_1:87
.= |[cos arccos z1, sin arccos z1]| by XCMPLX_1:87
.= |[z1, sin arccos z1]| by A6,A5,SIN_COS6:91
.= |[z1, z2]| by A10,A9,A14,SIN_COS6:102
.= y by EUCLID:53;
hence thesis by A1,A3,A15,FUNCT_1:def 3;
end;
end;
registration
cluster CircleMap -> onto;
coherence
proof
A1: R^1 | [#]R^1 = R^1 by TSEP_1:3;
CircleMap|REAL = CircleMap by Lm18,RELAT_1:69;
hence thesis by A1,Th38,TOPMETR:17;
end;
end;
Lm23: CircleMap | [.0,1.[ is one-to-one
proof
A1: sin | [.PI/2,3/2*PI.] is one-to-one;
let x1, y1 be object;
set f = CircleMap | [.0,1.[;
A2: [.0,PI/2.] c= [.-PI/2,PI/2.] by XXREAL_1:34;
A3: dom f = [.0,1.[ by Lm18,RELAT_1:62;
assume
A4: x1 in dom f;
then reconsider x = x1 as Real;
A5: f.x = CircleMap.x by A3,A4,FUNCT_1:49
.= |[cos(2*PI*x),sin(2*PI*x)]| by Def11;
assume
A6: y1 in dom f;
then reconsider y = y1 as Real;
assume
A7: f.x1 = f.y1;
A8: f.y = CircleMap.y by A3,A6,FUNCT_1:49
.= |[cos(2*PI*y),sin(2*PI*y)]| by Def11;
then
A9: cos(2*PI*x) = cos(2*PI*y) by A7,A5,SPPOL_2:1;
A10: cos(2*PI*y) = cos.(2*PI*y) by SIN_COS:def 19;
A11: cos(2*PI*x) = cos.(2*PI*x) by SIN_COS:def 19;
A12: sin(2*PI*x) = sin(2*PI*y) by A7,A5,A8,SPPOL_2:1;
A13: sin(2*PI*y) = sin.(2*PI*y) by SIN_COS:def 17;
A14: sin(2*PI*x) = sin.(2*PI*x) by SIN_COS:def 17;
per cases by A3,A4,XXREAL_1:3;
suppose
A15: 0 <= x & x <= 1/4;
A16: [.0,PI/2.] c= [.0,PI.] by Lm5,XXREAL_1:34;
2*PI*x <= 2*PI*(1/4) by A15,XREAL_1:64;
then
A17: 2*PI*x in [.0,2*PI*1/4.] by A15,XXREAL_1:1;
per cases by A3,A6,XXREAL_1:3;
suppose
A18: 0 <= y & y <= 1/4;
then 2*PI*y <= 2*PI*(1/4) by XREAL_1:64;
then
A19: 2*PI*y in [.0,2*PI*1/4.] by A18,XXREAL_1:1;
set g = sin | [.0,PI/2.];
A20: dom g = [.0,PI/2.] by RELAT_1:62,SIN_COS:24;
g.(2*PI*x) = sin.(2*PI*x) by A17,FUNCT_1:49
.= sin.(2*PI*y) by A12,A14,SIN_COS:def 17
.= g.(2*PI*y) by A19,FUNCT_1:49;
then 2*PI*x = 2*PI*y by A17,A19,A20,FUNCT_1:def 4;
then x = 2*PI*y/P2 by XCMPLX_1:89;
hence thesis by XCMPLX_1:89;
end;
suppose
A21: 1/4 < y & y < 3/4;
then
A22: 2*PI*y < 2*PI*(3/4) by XREAL_1:68;
2*PI*(1/4) < 2*PI*y by A21,XREAL_1:68;
then 2*PI*y in ].PI/2,3/2*PI.[ by A22,XXREAL_1:4;
hence thesis by A9,A11,A10,A2,A17,COMPTRIG:12,13;
end;
suppose
A23: 3/4 <= y & y < 1;
then
A24: 2*PI*y < 2*PI*1 by XREAL_1:68;
A25: [.3/2*PI,2*PI.[ c= ].PI,2*PI.[ by Lm6,XXREAL_1:48;
2*PI*(3/4) <= 2*PI*y by A23,XREAL_1:64;
then 2*PI*y in [.3/2*PI,2*PI.[ by A24,XXREAL_1:3;
hence thesis by A12,A14,A13,A17,A16,A25,COMPTRIG:8,9;
end;
end;
suppose
A26: 1/4 < x & x <= 1/2;
then
A27: 2*PI*x <= 2*PI*(1/2) by XREAL_1:64;
2*PI*(1/4) < 2*PI*x by A26,XREAL_1:68;
then
A28: 2*PI*x in ].PI/2,2*PI*(1/2).] by A27,XXREAL_1:2;
A29: ].PI/2,PI.] c= ].PI/2,3/2*PI.[ by Lm6,XXREAL_1:49;
A30: ].PI/2,PI.] c= [.0,PI.] by XXREAL_1:36;
per cases by A3,A6,XXREAL_1:3;
suppose
A31: 0 <= y & y <= 1/4;
then 2*PI*y <= 2*PI*(1/4) by XREAL_1:64;
then 2*PI*y in [.0,2*PI*(1/4).] by A31,XXREAL_1:1;
hence thesis by A9,A11,A10,A2,A28,A29,COMPTRIG:12,13;
end;
suppose
A32: 1/4 < y & y <= 1/2;
then
A33: 2*PI*y <= 2*PI*(1/2) by XREAL_1:64;
2*PI*(1/4) < 2*PI*y by A32,XREAL_1:68;
then
A34: 2*PI*y in ].2*PI*(1/4),2*PI*(1/2).] by A33,XXREAL_1:2;
set g = sin | ].PI/2,PI.];
A35: dom g = ].PI/2,PI.] by RELAT_1:62,SIN_COS:24;
A36: g is one-to-one by A1,Lm6,SIN_COS6:2,XXREAL_1:36;
g.(2*PI*x) = sin.(2*PI*x) by A28,FUNCT_1:49
.= sin.(2*PI*y) by A12,A14,SIN_COS:def 17
.= g.(2*PI*y) by A34,FUNCT_1:49;
then 2*PI*x = 2*PI*y by A28,A34,A36,A35;
then x = 2*PI*y/P2 by XCMPLX_1:89;
hence thesis by XCMPLX_1:89;
end;
suppose
A37: 1/2 < y & y < 1;
then
A38: 2*PI*y < 2*PI*1 by XREAL_1:68;
2*PI*(1/2) < 2*PI*y by A37,XREAL_1:68;
then 2*PI*y in ].PI,2*PI.[ by A38,XXREAL_1:4;
hence thesis by A12,A14,A13,A28,A30,COMPTRIG:8,9;
end;
end;
suppose
A39: 1/2 < x & x <= 3/4;
then
A40: 2*PI*x <= 2*PI*(3/4) by XREAL_1:64;
2*PI*(1/2) < 2*PI*x by A39,XREAL_1:68;
then
A41: 2*PI*x in ].PI,2*PI*(3/4).] by A40,XXREAL_1:2;
A42: ].PI,3/2*PI.] c= [.PI/2,3/2*PI.] by Lm5,XXREAL_1:36;
A43: ].PI,3/2*PI.] c= ].PI,2*PI.[ by Lm7,XXREAL_1:49;
per cases by A3,A6,XXREAL_1:3;
suppose
A44: 0 <= y & y <= 1/2;
then 2*PI*y <= 2*PI*(1/2) by XREAL_1:64;
then 2*PI*y in [.0,PI.] by A44,XXREAL_1:1;
hence thesis by A12,A14,A13,A41,A43,COMPTRIG:8,9;
end;
suppose
A45: 1/2 < y & y <= 3/4;
then
A46: 2*PI*y <= 2*PI*(3/4) by XREAL_1:64;
2*PI*(1/2) < 2*PI*y by A45,XREAL_1:68;
then
A47: 2*PI*y in ].PI,2*PI*(3/4).] by A46,XXREAL_1:2;
set g = sin | ].PI,3/2*PI.];
A48: dom g = ].PI,3/2*PI.] by RELAT_1:62,SIN_COS:24;
A49: g is one-to-one by A1,Lm5,SIN_COS6:2,XXREAL_1:36;
g.(2*PI*x) = sin.(2*PI*x) by A41,FUNCT_1:49
.= sin.(2*PI*y) by A12,A14,SIN_COS:def 17
.= g.(2*PI*y) by A47,FUNCT_1:49;
then 2*PI*x = 2*PI*y by A41,A47,A49,A48;
then x = 2*PI*y/P2 by XCMPLX_1:89;
hence thesis by XCMPLX_1:89;
end;
suppose
A50: 3/4 < y & y < 1;
then
A51: 2*PI*y < 2*PI*1 by XREAL_1:68;
2*PI*(3/4) < 2*PI*y by A50,XREAL_1:68;
then 2*PI*y in ].3/2*PI,2*PI.[ by A51,XXREAL_1:4;
hence thesis by A9,A11,A10,A41,A42,COMPTRIG:14,15;
end;
end;
suppose
A52: 3/4 < x & x < 1;
then
A53: 2*PI*x < 2*PI*1 by XREAL_1:68;
2*PI*(3/4) < 2*PI*x by A52,XREAL_1:68;
then
A54: 2*PI*x in ].3/2*PI,2*PI.[ by A53,XXREAL_1:4;
A55: ].3/2*PI,2*PI.[ c= ].PI,2*PI.[ by Lm6,XXREAL_1:46;
per cases by A3,A6,XXREAL_1:3;
suppose
A56: 0 <= y & y <= 1/2;
then 2*PI*y <= 2*PI*(1/2) by XREAL_1:64;
then 2*PI*y in [.0,PI.] by A56,XXREAL_1:1;
hence thesis by A12,A14,A13,A54,A55,COMPTRIG:8,9;
end;
suppose
A57: 1/2 < y & y <= 3/4;
then
A58: 2*PI*y <= 2*PI*(3/4) by XREAL_1:64;
A59: ].PI,3/2*PI.] c= [.PI/2,3/2*PI.] by Lm5,XXREAL_1:36;
2*PI*(1/2) < 2*PI*y by A57,XREAL_1:68;
then 2*PI*y in ].PI,3/2*PI.] by A58,XXREAL_1:2;
hence thesis by A9,A11,A10,A54,A59,COMPTRIG:14,15;
end;
suppose
A60: 3/4 < y & y < 1;
then
A61: 2*PI*y < 2*PI*1 by XREAL_1:68;
2*PI*(3/4) < 2*PI*y by A60,XREAL_1:68;
then
A62: 2*PI*y in ].3/2*PI,2*PI.[ by A61,XXREAL_1:4;
set g = sin | ].3/2*PI,2*PI.[;
A63: dom g = ].3/2*PI,2*PI.[ by RELAT_1:62,SIN_COS:24;
g.(2*PI*x) = sin.(2*PI*x) by A54,FUNCT_1:49
.= sin.(2*PI*y) by A12,A14,SIN_COS:def 17
.= g.(2*PI*y) by A62,FUNCT_1:49;
then 2*PI*x = 2*PI*y by A54,A62,A63,FUNCT_1:def 4;
then x = 2*PI*y/P2 by XCMPLX_1:89;
hence thesis by XCMPLX_1:89;
end;
end;
end;
registration
let r be Real;
cluster CircleMap | [.r,r+1.[ -> one-to-one;
coherence
proof
let x, y be object;
set g = CircleMap | [.0,1.[;
set f = CircleMap | [.r,r+1.[;
assume that
A1: x in dom f and
A2: y in dom f and
A3: f.x = f.y;
A4: dom f = [.r,r+1.[ by Lm18,RELAT_1:62;
reconsider x, y as Real by A1,A2;
A5: dom g = [.0,1.[ by Lm18,RELAT_1:62;
A6: r <= y by A4,A2,XXREAL_1:3;
A7: x < r+1 by A4,A1,XXREAL_1:3;
set x1 = frac x;
A8: x1 = x-[\x/] by INT_1:def 8;
A9: x1 < 1 by INT_1:43;
0 <= x1 by INT_1:43;
then
A10: x1 in [.0,1.[ by A9,XXREAL_1:3;
set y1 = frac y;
A11: y1 = y-[\y/] by INT_1:def 8;
A12: y1 < 1 by INT_1:43;
0 <= y1 by INT_1:43;
then
A13: y1 in [.0,1.[ by A12,XXREAL_1:3;
A14: f.y = CircleMap.y by A2,FUNCT_1:47
.= CircleMap.(y+-[\y/]) by Th31
.= g.y1 by A5,A11,A13,FUNCT_1:47;
f.x = CircleMap.x by A1,FUNCT_1:47
.= CircleMap.(x+-[\x/]) by Th31
.= g.x1 by A5,A8,A10,FUNCT_1:47;
then
A15: x1 = y1 by A5,A3,A10,A13,A14,Lm23;
A16: y < r+1 by A4,A2,XXREAL_1:3;
r <= x by A4,A1,XXREAL_1:3;
hence thesis by A7,A6,A16,A15,INT_1:72;
end;
end;
registration
let r be Real;
cluster CircleMap | ].r,r+1.[ -> one-to-one;
coherence
proof
CircleMap | [.r,r+1.[ is one-to-one;
hence thesis by SIN_COS6:2,XXREAL_1:45;
end;
end;
theorem Th39:
b-a <= 1 implies for d being set st d in IntIntervals(a,b) holds
CircleMap|d is one-to-one
proof
assume that
A1: b-a <= 1;
let d be set;
assume d in IntIntervals(a,b);
then consider n being Element of INT such that
A2: d = ].a+n,b+n.[;
A3: CircleMap | [.a+n,a+n+1.[ is one-to-one;
b-a+(a+n) <= 1+(a+n) by A1,XREAL_1:6;
hence thesis by A2,A3,SIN_COS6:2,XXREAL_1:45;
end;
theorem Th40:
for d being set st d in IntIntervals(a,b) holds CircleMap.:d =
CircleMap.:union IntIntervals(a,b)
proof
set D = IntIntervals(a,b);
let d be set;
assume
A1: d in D;
hence CircleMap.:d c= CircleMap.:union D by RELAT_1:123,ZFMISC_1:74;
consider i being Element of INT such that
A2: d = ]. a+i, b+i .[ by A1;
let y be object;
assume y in CircleMap.:union D;
then consider x being Element of R^1 such that
A3: x in union D and
A4: y = CircleMap.x by FUNCT_2:65;
consider Z being set such that
A5: x in Z and
A6: Z in D by A3,TARSKI:def 4;
consider n being Element of INT such that
A7: Z = ]. a+n, b+n .[ by A6;
x < b+n by A5,A7,XXREAL_1:4;
then x+i < b+n+i by XREAL_1:6;
then
A8: x+i-n < b+n+i-n by XREAL_1:9;
set k = x+i-n;
A9: CircleMap.k = CircleMap.(x+(i-n)) .= y by A4,Th31;
A10: k in R by TOPMETR:17,XREAL_0:def 1;
a+n < x by A5,A7,XXREAL_1:4;
then a+n+i < x+i by XREAL_1:6;
then a+n+i-n < x+i-n by XREAL_1:9;
then k in d by A2,A8,XXREAL_1:4;
hence thesis by A10,A9,FUNCT_2:35;
end;
definition
let r be Point of R^1;
func CircleMap(r) -> Function of R^1 | R^1(].r,r+1.[), Topen_unit_circle(
CircleMap.r) equals
CircleMap | ].r,r+1.[;
coherence
proof
set B = [.r,r+1.[;
set A = ].r,r+1.[;
set X = Topen_unit_circle(CircleMap.r);
set f = CircleMap | A;
set g = CircleMap | B;
A1: A c= B by XXREAL_1:45;
A2: dom f = A by Lm18,RELAT_1:62;
A3: the carrier of X = cS1 \ {CircleMap.r} by Def10;
A4: rng f c= the carrier of X
proof
let y be object;
assume
A5: y in rng f;
now
A6: dom g = B by Lm18,RELAT_1:62;
assume
A7: y = CircleMap.r;
r+0 < r+1 by XREAL_1:8;
then
A8: r in B by XXREAL_1:3;
consider x being object such that
A9: x in dom f and
A10: f.x = y by A5,FUNCT_1:def 3;
g.x = CircleMap.x by A1,A2,A9,FUNCT_1:49
.= CircleMap.r by A2,A7,A9,A10,FUNCT_1:49
.= g.r by A8,FUNCT_1:49;
then x = r by A1,A2,A9,A8,A6,FUNCT_1:def 4;
hence contradiction by A2,A9,XXREAL_1:4;
end;
then not y in {CircleMap.r} by TARSKI:def 1;
hence thesis by A3,A5,XBOOLE_0:def 5;
end;
the carrier of R^1 | R^1(A) = A by PRE_TOPC:8;
hence thesis by A2,A4,FUNCT_2:2;
end;
end;
Lm24: rng (AffineMap(1,-a) | ].r+a,r+a+1.[) = ].r,r+1.[
proof
set F = AffineMap(1,-a);
set f = F | ].r+a,r+a+1.[;
dom F = REAL by FUNCT_2:def 1;
then
A1: dom f = ].r+a,r+a+1.[ by RELAT_1:62;
thus rng f = ].r,r+1.[
proof
thus rng f c= ].r,r+1.[
proof
let y be object;
assume y in rng f;
then consider x being object such that
A2: x in dom f and
A3: f.x = y by FUNCT_1:def 3;
reconsider x as Real by A2;
r+a < x by A1,A2,XXREAL_1:4;
then
A4: r+a-a < x-a by XREAL_1:9;
x < r+a+1 by A1,A2,XXREAL_1:4;
then
A5: x-a < r+a+1-a by XREAL_1:9;
y = F.x by A2,A3,FUNCT_1:47
.= 1*x+-a by FCONT_1:def 4;
hence thesis by A4,A5,XXREAL_1:4;
end;
let y be object;
assume
A6: y in ].r,r+1.[;
then reconsider y as Real;
y < r+1 by A6,XXREAL_1:4;
then
A7: y+a < r+1+a by XREAL_1:6;
r < y by A6,XXREAL_1:4;
then r+a < y+a by XREAL_1:6;
then
A8: y+a in ].r+a,r+a+1.[ by A7,XXREAL_1:4;
then f.(y+a) = F.(y+a) by FUNCT_1:49
.= 1*(y+a)+-a by FCONT_1:def 4
.= y;
hence thesis by A1,A8,FUNCT_1:def 3;
end;
end;
theorem Th41:
CircleMap(R^1(a+i)) = CircleMap(R^1(a)) * (AffineMap(1,-i) | ].a +i,a+i+1.[)
proof
set W = ].a,a+1.[;
set Q = ].a+i,a+i+1.[;
set h = CircleMap(R^1(a+i));
set g = CircleMap(R^1(a));
set F = AffineMap(1,-i);
set f = F|Q;
A1: dom h = Q by Lm18,RELAT_1:62;
dom F = REAL by FUNCT_2:def 1;
then
A2: dom f = Q by RELAT_1:62;
A3: for x being object st x in dom h holds h.x = (g*f).x
proof
let x be object;
assume
A4: x in dom h;
then reconsider y = x as Real;
y < a+i+1 by A1,A4,XXREAL_1:4;
then
A5: y-i < a+i+1-i by XREAL_1:9;
a+i < y by A1,A4,XXREAL_1:4;
then a+i-i < y-i by XREAL_1:9;
then
A6: y-i in W by A5,XXREAL_1:4;
thus (g*f).x = g.(f.x) by A1,A2,A4,FUNCT_1:13
.= g.(F.x) by A1,A4,FUNCT_1:49
.= g.(1*y+-i) by FCONT_1:def 4
.= CircleMap.(y+-i) by A6,FUNCT_1:49
.= CircleMap.y by Th31
.= h.x by A1,A4,FUNCT_1:49;
end;
A7: rng f = ].a,a+1.[ by Lm24;
dom g = W by Lm18,RELAT_1:62;
then dom (g*f) = dom f by A7,RELAT_1:27;
hence thesis by A2,A3,Lm18,RELAT_1:62;
end;
registration
let r be Point of R^1;
cluster CircleMap(r) -> one-to-one onto continuous;
coherence
proof
thus CircleMap(r) is one-to-one;
thus CircleMap(r) is onto
proof
set TOUC = Topen_unit_circle(CircleMap.r);
set A = ].r,r+1.[;
set f = CircleMap | A;
set X = the carrier of TOUC;
thus rng CircleMap(r) c= X;
let y be object;
A1: [\r/] <= r by INT_1:def 6;
A2: dom f = ].r,r+1.[ by Lm18,RELAT_1:62;
assume
A3: y in X;
then reconsider z = y as Point of TOP-REAL 2 by Lm8;
set z1 = z`1, z2 = z`2;
A4: z1 <= 1 by A3,Th26;
set x = arccos z1/(2*PI);
A5: -1 <= z1 by A3,Th26;
then
A6: 0 <= x by A4,Lm22;
x <= 1/2 by A5,A4,Lm22;
then
A7: x < 1 by XXREAL_0:2;
then
A8: x-x < 1-x by XREAL_1:14;
A9: z1^2 + z2^2 = |. z .|^2 by JGRAPH_1:29;
z is Point of TUC by A3,PRE_TOPC:25;
then
A10: |. z .| = 1 by Th12;
per cases;
suppose
A11: z2 < 0;
A12: CircleMap.-x = |[cos(-2*PI*x), sin(2*PI*(-x))]| by Def11
.= |[cos(2*PI*x), sin(2*PI*(-x))]| by SIN_COS:31
.= |[cos arccos z1, sin(-2*PI*x)]| by XCMPLX_1:87
.= |[cos arccos z1, -sin(2*PI*x)]| by SIN_COS:31
.= |[cos arccos z1, -sin arccos z1]| by XCMPLX_1:87
.= |[z1, -sin arccos z1]| by A5,A4,SIN_COS6:91
.= |[z1, --z2]| by A10,A9,A11,SIN_COS6:103
.= y by EUCLID:53;
per cases;
suppose
A13: 1-x+[\r/] in A;
then f.(1-x+[\r/]) = CircleMap.(-x+([\r/]+1)) by FUNCT_1:49
.= CircleMap.-x by Th31;
hence thesis by A2,A12,A13,FUNCT_1:def 3;
end;
suppose
A14: not 1-x+[\r/] in A;
now
assume x = 0;
then arccos z1 = 0;
then z1 = 1 by A5,A4,SIN_COS6:96;
hence contradiction by A10,A9,A11;
end;
then [\r/]-x < r-0 by A1,A6,XREAL_1:15;
then -x+[\r/]+1 < r+1 by XREAL_1:6;
then
A15: r >= 1-x+[\r/] by A14,XXREAL_1:4;
[\r/]+1+0 < [\r/]+1+(1-x) by A8,XREAL_1:6;
then
A16: r < 2-x+[\r/] by INT_1:29,XXREAL_0:2;
now
assume -x+[\r/]+1 = r;
then CircleMap.r = CircleMap.(-x+([\r/]+1))
.= CircleMap.-x by Th31;
hence contradiction by A3,A12,Th21;
end;
then 1-x+[\r/] < r by A15,XXREAL_0:1;
then 1-x+[\r/]+1 < r+1 by XREAL_1:6;
then
A17: -x+[\r/]+2 in A by A16,XXREAL_1:4;
then f.(-x+([\r/]+2)) = CircleMap.(-x+([\r/]+2)) by FUNCT_1:49
.= CircleMap.-x by Th31;
hence thesis by A2,A12,A17,FUNCT_1:def 3;
end;
end;
suppose
A18: z2 >= 0;
A19: CircleMap.x = |[cos(2*PI*x), sin(2*PI*x)]| by Def11
.= |[cos arccos z1, sin(2*PI*x)]| by XCMPLX_1:87
.= |[cos arccos z1, sin arccos z1]| by XCMPLX_1:87
.= |[z1, sin arccos z1]| by A5,A4,SIN_COS6:91
.= |[z1, z2]| by A10,A9,A18,SIN_COS6:102
.= y by EUCLID:53;
per cases;
suppose
A20: x+[\r/] in A;
then f.(x+[\r/]) = CircleMap.(x+[\r/]) by FUNCT_1:49
.= CircleMap.x by Th31;
hence thesis by A2,A19,A20,FUNCT_1:def 3;
end;
suppose
A21: not x+[\r/] in A;
0+([\r/]+1) <= x+([\r/]+1) by A6,XREAL_1:6;
then
A22: r < x+[\r/]+1 by INT_1:29,XXREAL_0:2;
A23: now
assume x+[\r/]+1 = r+1;
then CircleMap.r = CircleMap.x by Th31;
hence contradiction by A3,A19,Th21;
end;
x+[\r/] < 1+r by A1,A7,XREAL_1:8;
then x+[\r/] <= r by A21,XXREAL_1:4;
then x+[\r/]+1 <= r+1 by XREAL_1:6;
then x+[\r/]+1 < r+1 by A23,XXREAL_0:1;
then
A24: x+[\r/]+1 in A by A22,XXREAL_1:4;
then f.(x+[\r/]+1) = CircleMap.(x+([\r/]+1)) by FUNCT_1:49
.= CircleMap.x by Th31;
hence thesis by A2,A19,A24,FUNCT_1:def 3;
end;
end;
end;
Topen_unit_circle(CircleMap.r) = (Tunit_circle(2)) | (([#]
Tunit_circle(2)) \ {CircleMap.r}) by Th22;
hence thesis by TOPREALA:8;
end;
end;
definition
func Circle2IntervalR -> Function of Topen_unit_circle(c[10]), R^1 | R^1(].0
,1.[) means
:Def13:
for p being Point of Topen_unit_circle(c[10]) ex x, y being
Real st p = |[x,y]| & (y >= 0 implies it.p = arccos x/(2*PI)) & (y <= 0
implies it.p = 1-arccos x/(2*PI));
existence
proof
defpred P[set,set] means ex x, y being Real st $1 = |[x,y]| & (y >=
0 implies $2 = arccos x/P2) & (y <= 0 implies $2 = 1-arccos x/P2);
reconsider A as non empty Subset of R^1;
A1: Y = A by PRE_TOPC:8;
A2: for x being Element of X ex y being Element of Y st P[x,y]
proof
let x be Element of X;
A3: X = cS1 \ {c[10]} by Def10;
then
A4: x in cS1 by XBOOLE_0:def 5;
A5: cS1 is Subset of TOP-REAL 2 by TSEP_1:1;
then consider a, b being Element of REAL such that
A6: x = <*a,b*> by A4,EUCLID:51;
reconsider x1 = x as Point of TOP-REAL 2 by A4,A5;
A7: b = x1`2 by A6,EUCLID:52;
set k = arccos a;
A8: a = x1`1 by A6,EUCLID:52;
then
A9: -1 <= a by Th26;
A10: 1^2 = |. x1 .|^2 by A4,Th12
.= a^2+b^2 by A8,A7,JGRAPH_3:1;
A11: a <= 1 by A8,Th26;
then
A12: 0 <= k by A9,SIN_COS6:99;
A13: k/P2 <= 1/2 by A9,A11,Lm22;
A14: not x in {c[10]} by A3,XBOOLE_0:def 5;
A15: now
assume
A16: k = 0;
then 1-1 = 1+b^2-1 by A9,A11,A10,SIN_COS6:96;
then
A17: b = 0;
a = 1 by A9,A11,A16,SIN_COS6:96;
hence contradiction by A6,A14,A17,TARSKI:def 1;
end;
A18: k <= PI by A9,A11,SIN_COS6:99;
A19: 0 <= k/P2 by A9,A11,Lm22;
per cases;
suppose
A20: b = 0;
set y = k/P2;
y < 1 by A13,XXREAL_0:2;
then reconsider y as Element of Y by A1,A19,A15,XXREAL_1:4;
take y, a, b;
thus x = |[a,b]| by A6;
thus b >= 0 implies y = arccos a/P2;
assume b <= 0;
A21: a <> 1 by A6,A14,A20,TARSKI:def 1;
hence y = 1*PI/P2 by A10,A20,SIN_COS6:93,SQUARE_1:41
.= 1-1/2 by XCMPLX_1:91
.= 1-1*PI/P2 by XCMPLX_1:91
.= 1-arccos a/P2 by A10,A20,A21,SIN_COS6:93,SQUARE_1:41;
end;
suppose
A22: b > 0;
set y = k/P2;
y < 1 by A13,XXREAL_0:2;
then reconsider y as Element of Y by A1,A19,A15,XXREAL_1:4;
take y, a, b;
thus thesis by A6,A22;
end;
suppose
A23: b < 0;
set y = 1-k/P2;
A24: (P2-k)/P2 = P2/P2-k/P2 by XCMPLX_1:120
.= y by XCMPLX_1:60;
P2-k < P2-0 by A12,A15,XREAL_1:15;
then y < P2/P2 by A24,XREAL_1:74;
then
A25: y < 1 by XCMPLX_1:60;
1*k < P2 by A18,XREAL_1:98;
then k-k < P2-k by XREAL_1:14;
then reconsider y as Element of Y by A1,A24,A25,XXREAL_1:4;
take y, a, b;
thus thesis by A6,A23;
end;
end;
ex G being Function of TOUC, R^1|R^1(].0,0+p1.[) st for p being Point
of TOUC holds P[p,G.p] from FUNCT_2:sch 3(A2);
hence thesis;
end;
uniqueness
proof
let f, g be Function of TOUC, R^1 | A such that
A26: for p being Point of TOUC ex x, y being Real st p = |[x,y
]| & (y >= 0 implies f.p = arccos x/(2*PI)) & (y <= 0 implies f.p = 1-arccos x/
(2*PI)) and
A27: for p being Point of TOUC ex x, y being Real st p = |[x,y
]| & (y >= 0 implies g.p = arccos x/(2*PI)) & (y <= 0 implies g.p = 1-arccos x/
(2*PI));
now
let p be Point of TOUC;
A28: ex x2, y2 being Real st p = |[x2,y2]| & (y2 >= 0 implies g.p
= arccos x2/(2*PI)) & (y2 <= 0 implies g.p = 1-arccos x2/(2*PI)) by A27;
ex x1, y1 being Real st p = |[x1,y1]| & (y1 >= 0 implies f.p
= arccos x1/(2*PI)) & (y1 <= 0 implies f.p = 1-arccos x1/(2*PI)) by A26;
hence f.p = g.p by A28,SPPOL_2:1;
end;
hence thesis;
end;
end;
set A1 = R^1(].1/2,1/2+p1.[);
definition
func Circle2IntervalL -> Function of Topen_unit_circle(c[-10]), R^1 | R^1(].
1/2,3/2.[) means
:Def14:
for p being Point of Topen_unit_circle(c[-10]) ex x, y
being Real st p = |[x,y]| & (y >= 0 implies it.p = 1+arccos x/(2*PI)) &
(y <= 0 implies it.p = 1-arccos x/(2*PI));
existence
proof
defpred P[set,set] means ex x, y being Real st $1 = |[x,y]| & (y >=
0 implies $2 = 1+arccos x/P2) & (y <= 0 implies $2 = 1-arccos x/P2);
reconsider A1 as non empty Subset of R^1;
A1: Ym = A1 by PRE_TOPC:8;
A2: for x being Element of Xm ex y being Element of Ym st P[x,y]
proof
let x be Element of Xm;
A3: Xm = cS1 \ {c[-10]} by Def10;
then
A4: x in cS1 by XBOOLE_0:def 5;
A5: not x in {c[-10]} by A3,XBOOLE_0:def 5;
A6: cS1 is Subset of TOP-REAL 2 by TSEP_1:1;
then consider a, b being Element of REAL such that
A7: x = <*a,b*> by A4,EUCLID:51;
reconsider x1 = x as Point of TOP-REAL 2 by A4,A6;
A8: b = x1`2 by A7,EUCLID:52;
set k = arccos a;
A9: a = x1`1 by A7,EUCLID:52;
then
A10: -1 <= a by Th26;
A11: a <= 1 by A9,Th26;
then
A12: k/P2 <= 1/2 by A10,Lm22;
A13: 1^2 = |. x1 .|^2 by A4,Th12
.= a^2+b^2 by A9,A8,JGRAPH_3:1;
A14: now
assume
A15: k = PI;
then 1-1 = (-1)^2+b^2-1 by A10,A11,A13,SIN_COS6:98
.= 1^2+b^2-1;
then
A16: b = 0;
a = -1 by A10,A11,A15,SIN_COS6:98;
hence contradiction by A7,A5,A16,TARSKI:def 1;
end;
A17: now
assume k/P2 = 1/2;
then k/P2*2 = 1/2*2;
then k/PI = 1 by XCMPLX_1:92;
hence contradiction by A14,XCMPLX_1:58;
end;
A18: 0 <= k/P2 by A10,A11,Lm22;
A19: now
let y be Real;
assume
A20: y = 1+k/P2;
then
A21: y <> 1+1/2 by A17;
1+0 <= y by A18,A20,XREAL_1:6;
then
A22: 1/2 < y by XXREAL_0:2;
y <= 1+1/2 by A12,A20,XREAL_1:6;
then y < 3/2 by A21,XXREAL_0:1;
hence y is Element of Ym by A1,A22,XXREAL_1:4;
end;
per cases;
suppose
A23: b = 0;
reconsider y = 1+k/P2 as Element of Ym by A19;
take y, a, b;
thus x = |[a,b]| by A7;
a <> -1 by A7,A5,A23,TARSKI:def 1;
then a = 1 by A13,A23,SQUARE_1:41;
hence thesis by SIN_COS6:95;
end;
suppose
A24: b > 0;
reconsider y = 1+k/P2 as Element of Ym by A19;
take y, a, b;
thus thesis by A7,A24;
end;
suppose
A25: b < 0;
set y = 1-k/P2;
A26: y <> 1/2 by A17;
y >= 1-1/2 by A12,XREAL_1:13;
then
A27: 1/2 < y by A26,XXREAL_0:1;
1-0 >= y by A18,XREAL_1:13;
then y < 3/2 by XXREAL_0:2;
then reconsider y as Element of Ym by A1,A27,XXREAL_1:4;
take y, a, b;
thus thesis by A7,A25;
end;
end;
ex G being Function of TOUCm, R^1|R^1(].1/2,1/2+p1.[) st for p being
Point of TOUCm holds P[p,G.p] from FUNCT_2:sch 3(A2);
hence thesis;
end;
uniqueness
proof
let f, g be Function of TOUCm, R^1 | R^1(].1/2,3/2.[) such that
A28: for p being Point of TOUCm ex x, y being Real st p = |[x,y
]| & (y >= 0 implies f.p = 1+arccos x/(2*PI)) & (y <= 0 implies f.p = 1-arccos
x/(2*PI)) and
A29: for p being Point of TOUCm ex x, y being Real st p = |[x,y
]| & (y >= 0 implies g.p = 1+arccos x/(2*PI)) & (y <= 0 implies g.p = 1-arccos
x/(2*PI));
now
let p be Point of TOUCm;
A30: ex x2, y2 being Real st p = |[x2,y2]| & (y2 >= 0 implies g.p
= 1+arccos x2/(2*PI)) & (y2 <= 0 implies g.p = 1-arccos x2/(2*PI)) by A29;
ex x1, y1 being Real st p = |[x1,y1]| & (y1 >= 0 implies f.p
= 1+arccos x1/(2*PI)) & (y1 <= 0 implies f.p = 1-arccos x1/(2*PI)) by A28;
hence f.p = g.p by A30,SPPOL_2:1;
end;
hence thesis;
end;
end;
set C = Circle2IntervalR;
set Cm = Circle2IntervalL;
theorem Th42:
(CircleMap(R^1(0)))" = Circle2IntervalR
proof
reconsider A as non empty Subset of R^1;
set f = CircleMap(R^1(0));
set Y = the carrier of (R^1|A);
reconsider f as Function of R^1|A, TOUC by Th32;
reconsider r0 = In(0,REAL) as Point of R^1 by TOPMETR:17;
set F = AffineMap(2*PI,0);
A1: dom id Y = Y by RELAT_1:45;
CircleMap.r0 = c[10] by Th32;
then
A2: rng f = X by FUNCT_2:def 3;
A3: Y = A by PRE_TOPC:8;
A4: now
let a be object;
assume
A5: a in dom (C*f);
then reconsider b = a as Point of R^1|A;
reconsider c = b as Element of REAL by XREAL_0:def 1;
consider x, y being Real such that
A6: f.b = |[x,y]| and
A7: y >= 0 implies C.(f.b) = arccos x/P2 and
A8: y <= 0 implies C.(f.b) = 1-arccos x/P2 by Def13;
A9: f.b = CircleMap.b by A3,FUNCT_1:49
.= |[ (cos*F).c, (sin*F).c ]| by Lm20;
then y = (sin*F).c by A6,SPPOL_2:1;
then
A10: y = sin.(F.c) by FUNCT_2:15;
x = (cos*F).c by A6,A9,SPPOL_2:1;
then x = cos.(F.c) by FUNCT_2:15;
then
A11: x = cos(F.c) by SIN_COS:def 19;
A12: c < 1 by A3,XXREAL_1:4;
A13: F.c = 2*PI*c+0 by FCONT_1:def 4;
then
A14: F.c/(2*PI*1) = c/1 by XCMPLX_1:91;
A15: F.(1-c) = 2*PI*(1-c)+0 by FCONT_1:def 4;
then
A16: F.(1-c)/(2*PI*1) = (1-c)/1 by XCMPLX_1:91;
A17: now
per cases;
suppose
A18: y >= 0;
then not F.c in ].PI,2*PI.[ by A10,COMPTRIG:9;
then F.c <= PI or F.c >= 2*PI by XXREAL_1:4;
then F.c/P2 <= (1*PI)/P2 or F.c/P2 >= 2*PI/P2 by XREAL_1:72;
then c <= 1/2 by A14,A12,XCMPLX_1:60,91;
then
A19: 2*PI*c <= 2*PI*(1/2) by XREAL_1:64;
0 <= c by A3,XXREAL_1:4;
hence C.(f.b) = F.c/P2 by A7,A11,A13,A18,A19,SIN_COS6:92
.= b by A13,XCMPLX_1:89;
end;
suppose
A20: y < 0;
then not F.c in [.0,PI.] by A10,COMPTRIG:8;
then F.c < 0 or F.c > PI by XXREAL_1:1;
then F.c/P2 < 0/P2 or F.c/P2 > (1*PI)/P2 by XREAL_1:74;
then c < 0 or c > 1/2 by A14,XCMPLX_1:91;
then 1-c < 1-1/2 by A3,XREAL_1:15,XXREAL_1:4;
then
A21: 2*PI*(1-c) <= 2*PI*(1/2) by XREAL_1:64;
A22: 1-c > 1-1 by A12,XREAL_1:15;
cos.(F.(1-c)) = cos(-2*PI*c+2*PI*1) by A15,SIN_COS:def 19
.= cos(-2*PI*c) by COMPLEX2:9
.= cos(2*PI*c) by SIN_COS:31;
then arccos x = arccos cos F.(1-c) by A11,A13,SIN_COS:def 19
.= F.(1-c) by A15,A22,A21,SIN_COS6:92;
hence C.(f.b) = b by A8,A16,A20;
end;
end;
thus (C*f).a = C.(f.b) by A5,FUNCT_1:12
.= (id Y).a by A17;
end;
dom (C*f) = Y by FUNCT_2:def 1;
then C = f qua Function" by A2,A1,A4,FUNCT_1:2,FUNCT_2:30;
hence thesis by TOPS_2:def 4;
end;
theorem Th43:
(CircleMap(R^1(1/2)))" = Circle2IntervalL
proof
reconsider A1 as non empty Subset of R^1;
set f = CircleMap(R^1(1/2));
set Y = the carrier of (R^1|A1);
reconsider f as Function of R^1|A1, TOUCm by Lm19;
set G = AffineMap(2*PI,0);
A1: dom id Ym = Ym by RELAT_1:45;
A2: rng f = Xm by Lm19,FUNCT_2:def 3;
A3: Y = A1 by PRE_TOPC:8;
A4: now
let a be object;
assume
A5: a in dom (Cm*f);
then reconsider b = a as Point of R^1|A1;
reconsider c = b as Real;
consider x, y being Real such that
A6: f.b = |[x,y]| and
A7: y >= 0 implies Cm.(f.b) = 1+arccos x/P2 and
A8: y <= 0 implies Cm.(f.b) = 1-arccos x/P2 by Def14;
A9: f.b = CircleMap.b by A3,FUNCT_1:49
.= |[ cos(2*PI*c), sin(2*PI*c) ]| by Def11;
then
A10: y = sin(2*PI*c) by A6,SPPOL_2:1;
A11: 1/2 < c by A3,XXREAL_1:4;
then 2*PI*(1/2) < 2*PI*c by XREAL_1:68;
then
A12: PI+2*PI*0 < 2*PI*c;
A13: c < 3/2 by A3,XXREAL_1:4;
then c-1 < 3/2-1 by XREAL_1:9;
then
A14: 2*PI*(c-1) <= 2*PI*(1/2) by XREAL_1:64;
2*PI*c <= 2*PI*(1/2+1) by A13,XREAL_1:64;
then
A15: 2*PI*c <= PI+2*PI*1;
A16: G.(1-c) = 2*PI*(1-c)+0 by FCONT_1:def 4;
then
A17: G.(1-c)/(2*PI*1) = (1-c)/1 by XCMPLX_1:91;
A18: x = cos(2*PI*c) by A6,A9,SPPOL_2:1
.= cos(2*PI*c+2*PI*(-1)) by COMPLEX2:9
.= cos(2*PI*(c-1));
A19: now
per cases;
suppose
A20: c >= 1;
then
A21: 1-1 <= c-1 by XREAL_1:9;
2*PI*c >= 2*PI*1 by A20,XREAL_1:64;
hence Cm.(f.b) = 1+(2*PI*(c-1))/P2 by A7,A18,A10,A14,A15,A21,
SIN_COS6:16,92
.= 1+(c-1) by XCMPLX_1:89
.= b;
end;
suppose
A22: c < 1;
then 2*PI*c < 2*PI*1 by XREAL_1:68;
then
A23: 2*PI*c < 2*PI+2*PI*0;
1-c < 1-1/2 by A11,XREAL_1:15;
then
A24: 2*PI*(1-c) <= 2*PI*(1/2) by XREAL_1:64;
A25: 1-1 <= 1-c by A22,XREAL_1:15;
arccos x = arccos cos(2*PI*c) by A6,A9,SPPOL_2:1
.= arccos cos(-2*PI*c) by SIN_COS:31
.= arccos cos(2*PI*(-c)+2*PI*1) by COMPLEX2:9
.= G.(1-c) by A16,A25,A24,SIN_COS6:92;
hence Cm.(f.b) = b by A8,A10,A17,A12,A23,SIN_COS6:12;
end;
end;
thus (Cm*f).a = Cm.(f.b) by A5,FUNCT_1:12
.= (id Ym).a by A19;
end;
dom (Cm*f) = Ym by FUNCT_2:def 1;
then Cm = f qua Function" by A2,A1,A4,FUNCT_1:2,FUNCT_2:30;
hence thesis by TOPS_2:def 4;
end;
set A = ].0,1.[;
set Q = [.-1,1.[;
set E = ].0,PI.];
set j = 1/P2;
reconsider Q, E as non empty Subset of REAL;
Lm25: the carrier of R^1 | R^1(Q) = R^1(Q) by PRE_TOPC:8;
Lm26: the carrier of R^1 | R^1(E) = R^1(E) by PRE_TOPC:8;
Lm27: the carrier of R^1 | R^1(A) = R^1(A) by PRE_TOPC:8;
set Af = AffineMap(j,0) | R^1(E);
dom AffineMap(j,0) = R by FUNCT_2:def 1,TOPMETR:17;
then
Lm28: dom Af = R^1(E) by RELAT_1:62;
rng Af c= A
proof
let y be object;
assume y in rng Af;
then consider x being object such that
A1: x in dom Af and
A2: Af.x = y by FUNCT_1:def 3;
reconsider x as Real by A1;
A3: y = AffineMap(j,0).x by A1,A2,Lm28,FUNCT_1:49
.= j*x+0 by FCONT_1:def 4
.= x/P2 by XCMPLX_1:99;
then reconsider y as Real;
x <= PI by A1,Lm28,XXREAL_1:2;
then y <= (1*PI)/P2 by A3,XREAL_1:72;
then y <= 1/2 by XCMPLX_1:91;
then
A4: y < 1 by XXREAL_0:2;
0 < x by A1,Lm28,XXREAL_1:2;
hence thesis by A3,A4,XXREAL_1:4;
end;
then reconsider
Af as Function of R^1 | R^1(E), R^1 | R^1(A) by Lm26,Lm27,Lm28,FUNCT_2:2;
Lm29: R^1(AffineMap(j,0)) = AffineMap(j,0);
Lm30: dom AffineMap(j,0) = REAL by FUNCT_2:def 1;
Lm31: rng AffineMap(j,0) = REAL by FCONT_1:55;
R^1| [#](R^1) = R^1 by TSEP_1:3;
then reconsider
Af as continuous Function of R^1 | R^1(E), R^1 | R^1(A) by Lm29,Lm30,Lm31,
TOPMETR:17,TOPREALA:8;
set L = (R^1(AffineMap(-1,1))) | R^1(A);
Lm32: dom AffineMap(-1,1) = REAL by FUNCT_2:def 1;
then
Lm33: dom L = A by RELAT_1:62;
rng L c= A
proof
let y be object;
assume y in rng L;
then consider x being object such that
A1: x in dom L and
A2: L.x = y by FUNCT_1:def 3;
reconsider x as Real by A1;
0 < x by A1,Lm33,XXREAL_1:4;
then
A3: 1-x < 1-0 by XREAL_1:15;
x < 1 by A1,Lm33,XXREAL_1:4;
then
A4: 1-1 < 1-x by XREAL_1:15;
y = AffineMap(-1,1).x by A1,A2,Lm33,FUNCT_1:49
.= (-1)*x+1 by FCONT_1:def 4;
hence thesis by A4,A3,XXREAL_1:4;
end;
then reconsider L as Function of R^1 | R^1(A), R^1 | R^1(A) by Lm27,Lm33,
FUNCT_2:2;
Lm34: rng AffineMap(-1,1) = REAL by FCONT_1:55;
Lm35: R^1| [#](R^1) = R^1 by TSEP_1:3;
then reconsider
L as continuous Function of R^1 | R^1(A), R^1 | R^1(A) by Lm32,Lm34,TOPMETR:17
,TOPREALA:8;
reconsider ac = R^1(arccos) as continuous Function of R^1 | R^1[.-1,1.], R^1 |
R^1[.0,PI.] by SIN_COS6:85,86;
set c = ac | R^1(Q);
Lm36: dom c = Q by RELAT_1:62,SIN_COS6:86,XXREAL_1:35;
Lm37: rng c c= E
proof
let y be object;
assume
A1: y in rng c;
then consider x being object such that
A2: x in dom c and
A3: c.x = y by FUNCT_1:def 3;
reconsider x as Real by A2;
A4: -1 <= x by A2,Lm36,XXREAL_1:3;
A5: x < 1 by A2,Lm36,XXREAL_1:3;
A6: rng c c= rng ac by RELAT_1:70;
then y in [.0,PI.] by A1,SIN_COS6:85;
then reconsider y as Real;
A7: y <= PI by A1,A6,SIN_COS6:85,XXREAL_1:1;
y = arccos.x by A2,A3,Lm36,FUNCT_1:49
.= arccos x by SIN_COS6:def 4;
then
A8: y <> 0 by A4,A5,SIN_COS6:96;
0 <= y by A1,A6,SIN_COS6:85,XXREAL_1:1;
hence thesis by A7,A8,XXREAL_1:2;
end;
then reconsider c as Function of R^1 | R^1(Q), R^1 | R^1(E) by Lm25,Lm26,Lm36,
FUNCT_2:2;
the carrier of R^1 | R^1[.-1,1.] = [.-1,1.] by PRE_TOPC:8;
then reconsider QQ = R^1(Q) as Subset of R^1 | R^1[.-1,1.] by XXREAL_1:35;
the carrier of R^1 | R^1[.0,PI.] = [.0,PI.] by PRE_TOPC:8;
then reconsider EE = R^1(E) as Subset of R^1 | R^1[.0,PI.] by XXREAL_1:36;
Lm38: (R^1 | R^1[.-1,1.]) | QQ = R^1 | R^1(Q) by GOBOARD9:2;
(R^1 | R^1[.0,PI.]) | EE = R^1 | R^1(E) by GOBOARD9:2;
then
Lm39: c is continuous by Lm38,TOPREALA:8;
reconsider p = proj1 as Function of TOP-REAL 2,R^1 by TOPMETR:17;
Lm40: dom p = the carrier of TOP-REAL 2 by FUNCT_2:def 1;
Lm41: p is continuous by JORDAN5A:27;
Lm42: for aX1 being Subset of TOUC st aX1 = {q where q is Point of TOP-REAL 2:
q in X & 0 <= q`2} holds Circle2IntervalR | (TOUC|aX1) is continuous
proof
reconsider c1 = c[-10] as Point of TOP-REAL 2;
let aX1 being Subset of TOUC such that
A1: aX1 = {q where q is Point of TOP-REAL 2: q in X & 0 <= q`2};
A2: c1`2 = 0 by EUCLID:52;
c[-10] is Point of Topen_unit_circle(c[10]) by Lm15,Th23;
then c[-10] in aX1 by A1,A2;
then reconsider aX1 as non empty Subset of TOUC;
set X1 = TOUC | aX1;
A3: cS1 is Subset of TOP-REAL 2 by TSEP_1:1;
[#]X1 is Subset of TUC by Lm9;
then reconsider B = [#]X1 as non empty Subset of TOP-REAL 2 by A3,XBOOLE_1:1;
set f = p|B;
A4: dom f = B by Lm40,RELAT_1:62;
A5: aX1 = the carrier of X1 by PRE_TOPC:8;
A6: rng f c= Q
proof
let y be object;
assume y in rng f;
then consider x being object such that
A7: x in dom f and
A8: f.x = y by FUNCT_1:def 3;
consider q being Point of TOP-REAL 2 such that
A9: q = x and
A10: q in X and
0 <= q`2 by A1,A5,A4,A7;
A11: -1 <= q`1 by A10,Th27;
A12: q`1 < 1 by A10,Th27;
y = p.x by A4,A7,A8,FUNCT_1:49
.= q`1 by A9,PSCOMP_1:def 5;
hence thesis by A11,A12,XXREAL_1:3;
end;
the carrier of (TOP-REAL 2) | B = B by PRE_TOPC:8;
then reconsider f as Function of (TOP-REAL 2) | B, R^1 | R^1(Q) by A4,A6,Lm25
,FUNCT_2:2;
X1 is SubSpace of TUC by TSEP_1:7;
then X1 is SubSpace of TOP-REAL 2 by TSEP_1:7;
then
A13: (TOP-REAL 2) | B = X1 by PRE_TOPC:def 5;
A14: for a being Point of X1 holds (C|X1).a = (Af*(c*f)).a
proof
let a be Point of X1;
reconsider b = a as Point of TOUC by PRE_TOPC:25;
consider x, y being Real such that
A15: b = |[x,y]| and
A16: y >= 0 implies C.b = arccos x/P2 and
y <= 0 implies C.b = 1-arccos x/P2 by Def13;
A17: |[x,y]|`1 < 1 by A15,Th27;
A18: |[x,y]|`1 = x by EUCLID:52;
-1 <= |[x,y]|`1 by A15,Th26;
then
A19: x in Q by A18,A17,XXREAL_1:3;
then arccos.x = c.x by FUNCT_1:49;
then
A20: arccos.x in rng c by A19,Lm36,FUNCT_1:def 3;
a in aX1 by A5;
then ex q being Point of TOP-REAL 2 st a = q & q in X & 0 <= q`2 by A1;
hence (C|X1).a = arccos x/P2 by A15,A16,EUCLID:52,FUNCT_1:49
.= arccos.x/P2 by SIN_COS6:def 4
.= 1/P2 * (arccos.x) + 0 by XCMPLX_1:99
.= AffineMap(j,0).(arccos.x) by FCONT_1:def 4
.= Af.(arccos.x) by A20,Lm37,FUNCT_1:49
.= Af.(c.x) by A19,FUNCT_1:49
.= Af.(c.(|[x,y]|`1)) by EUCLID:52
.= Af.(c.(p.a)) by A15,PSCOMP_1:def 5
.= Af.(c.(f.a)) by FUNCT_1:49
.= Af.((c*f).a) by A13,FUNCT_2:15
.= (Af*(c*f)).a by A13,FUNCT_2:15;
end;
f is continuous by Lm41,TOPREALA:8;
hence thesis by A13,A14,Lm39,FUNCT_2:63;
end;
Lm43: for aX1 being Subset of TOUC st aX1 = {q where q is Point of TOP-REAL 2:
q in X & 0 >= q`2} holds Circle2IntervalR | (TOUC|aX1) is continuous
proof
reconsider c1 = c[-10] as Point of TOP-REAL 2;
let aX1 being Subset of TOUC such that
A1: aX1 = {q where q is Point of TOP-REAL 2: q in X & 0 >= q`2};
A2: c1`2 = 0 by EUCLID:52;
c[-10] is Point of Topen_unit_circle(c[10]) by Lm15,Th23;
then c[-10] in aX1 by A1,A2;
then reconsider aX1 as non empty Subset of TOUC;
set X1 = TOUC | aX1;
A3: cS1 is Subset of TOP-REAL 2 by TSEP_1:1;
[#]X1 is Subset of TUC by Lm9;
then reconsider B = [#]X1 as non empty Subset of TOP-REAL 2 by A3,XBOOLE_1:1;
set f = p|B;
A4: dom f = B by Lm40,RELAT_1:62;
A5: aX1 = the carrier of X1 by PRE_TOPC:8;
A6: rng f c= Q
proof
let y be object;
assume y in rng f;
then consider x being object such that
A7: x in dom f and
A8: f.x = y by FUNCT_1:def 3;
consider q being Point of TOP-REAL 2 such that
A9: q = x and
A10: q in X and
0 >= q`2 by A1,A5,A4,A7;
A11: -1 <= q`1 by A10,Th27;
A12: q`1 < 1 by A10,Th27;
y = p.x by A4,A7,A8,FUNCT_1:49
.= q`1 by A9,PSCOMP_1:def 5;
hence thesis by A11,A12,XXREAL_1:3;
end;
A13: the carrier of (TOP-REAL 2) | B = B by PRE_TOPC:8;
then reconsider f as Function of (TOP-REAL 2) | B, R^1 | R^1(Q) by A4,A6,Lm25
,FUNCT_2:2;
X1 is SubSpace of TUC by TSEP_1:7;
then X1 is SubSpace of TOP-REAL 2 by TSEP_1:7;
then
A14: (TOP-REAL 2) | B = X1 by PRE_TOPC:def 5;
A15: for a being Point of X1 holds (C|X1).a = (L*(Af*(c*f))).a
proof
let a be Point of X1;
reconsider b = a as Point of TOUC by PRE_TOPC:25;
consider x, y being Real such that
A16: b = |[x,y]| and
y >= 0 implies C.b = arccos x/P2 and
A17: y <= 0 implies C.b = 1-arccos x/P2 by Def13;
A18: |[x,y]|`1 < 1 by A16,Th27;
reconsider r = (Af*(c*f)).a as Real;
dom (Af*(c*f)) = the carrier of (TOP-REAL 2)|B by FUNCT_2:def 1;
then
A19: r in rng (Af*(c*f)) by A13,FUNCT_1:def 3;
A99: rng (Af*(c*f)) c= the carrier of (R^1 | R^1(A)) by RELAT_1:def 19;
a in aX1 by A5;
then
A20: ex q being Point of TOP-REAL 2 st a = q & q in X & 0 >= q`2 by A1;
A21: |[x,y]|`1 = x by EUCLID:52;
-1 <= |[x,y]|`1 by A16,Th26;
then
A22: x in Q by A21,A18,XXREAL_1:3;
then arccos.x = c.x by FUNCT_1:49;
then
A23: arccos.x in rng c by A22,Lm36,FUNCT_1:def 3;
arccos x/P2 = arccos.x/P2 by SIN_COS6:def 4
.= (j * (arccos.x) + 0) by XCMPLX_1:99
.= AffineMap(j,0).(arccos.x) by FCONT_1:def 4
.= Af.(arccos.x) by A23,Lm37,FUNCT_1:49
.= Af.(c.x) by A22,FUNCT_1:49
.= Af.(c.(|[x,y]|`1)) by EUCLID:52
.= Af.(c.(p.a)) by A16,PSCOMP_1:def 5
.= Af.(c.(f.a)) by FUNCT_1:49
.= Af.((c*f).a) by A14,FUNCT_2:15
.= (Af*(c*f)).a by A14,FUNCT_2:15;
hence (C|X1).a = (-1)*r+1 by A16,A17,A20,EUCLID:52,FUNCT_1:49
.= (R^1(AffineMap(-1,1))).r by FCONT_1:def 4
.= L.r by A19,A99,Lm27,FUNCT_1:49
.= (L*(Af*(c*f))).a by A14,FUNCT_2:15;
end;
f is continuous by Lm41,TOPREALA:8;
hence thesis by A14,A15,Lm39,FUNCT_2:63;
end;
Lm44: for p being Point of Topen_unit_circle(c[10]) st p = c[-10] holds
Circle2IntervalR is_continuous_at p
proof
reconsider c1 = c[-10] as Point of TOP-REAL 2;
set aX2 = {q where q is Point of TOP-REAL 2: q in X & 0 >= q`2};
set aX1 = {q where q is Point of TOP-REAL 2: q in X & 0 <= q`2};
A1: aX1 c= X
proof
let x be object;
assume x in aX1;
then ex q being Point of TOP-REAL 2 st x = q & q in X & 0 <= q`2;
hence thesis;
end;
A2: aX2 c= X
proof
let x be object;
assume x in aX2;
then ex q being Point of TOP-REAL 2 st x = q & q in X & 0 >= q`2;
hence thesis;
end;
A3: TOUC is SubSpace of TOUC by TSEP_1:2;
A4: c1`2 = 0 by EUCLID:52;
A5: c[-10] is Point of Topen_unit_circle(c[10]) by Lm15,Th23;
then
A6: c[-10] in aX1 by A4;
A7: c[-10] in aX2 by A4,A5;
then reconsider aX1, aX2 as non empty Subset of TOUC by A1,A2,A6;
set X1 = TOUC | aX1;
let p be Point of Topen_unit_circle(c[10]) such that
A8: p = c[-10];
reconsider x1 = p as Point of X1 by A8,A6,PRE_TOPC:8;
set X2 = TOUC | aX2;
reconsider x2 = p as Point of X2 by A8,A7,PRE_TOPC:8;
A9: the carrier of X2 = aX2 by PRE_TOPC:8;
X c= aX1 \/ aX2
proof
let a be object;
assume
A10: a in X;
then reconsider a as Point of TOP-REAL 2 by Lm8;
0 >= a`2 or 0 <= a`2;
then a in aX1 or a in aX2 by A10;
hence thesis by XBOOLE_0:def 3;
end;
then
A11: X = aX1 \/ aX2;
C|X2 is continuous by Lm43;
then
A12: C|X2 is_continuous_at x2;
C|X1 is continuous by Lm42;
then
A13: C|X1 is_continuous_at x1;
the carrier of X1 = aX1 by PRE_TOPC:8;
then TOUC = X1 union X2 by A9,A3,A11,TSEP_1:def 2;
hence thesis by A13,A12,TMAP_1:113;
end;
reconsider jj=1 as Element of REAL by XREAL_0:def 1;
set h1 = REAL --> jj;
reconsider h1 as PartFunc of REAL,REAL;
Lm45: Circle2IntervalR is continuous
proof
set h = j(#)arccos;
set K = [.-1,1.];
set J = [.p0,0 .[;
set I = ].0,p1.];
set Z = R^1 | R^1(].0,0+p1.[);
for p being Point of TOUC holds C is_continuous_at p
proof
Tcircle(0.TOP-REAL 2,1) is SubSpace of TREC by Th10;
then
A1: TOUC is SubSpace of TREC by TSEP_1:7;
let p be Point of TOUC;
A2: K = [#]CIT by TOPMETR:18;
reconsider q = p as Point of TOP-REAL 2 by Lm8;
A3: the carrier of Z = ].0,0+p1.[ by PRE_TOPC:8;
consider x, y being Real such that
A4: p = |[x,y]| and
A5: y >= 0 implies C.p = arccos x/P2 and
A6: y <= 0 implies C.p = 1-arccos x/P2 by Def13;
A7: y = q`2 by A4,EUCLID:52;
A8: x = q`1 by A4,EUCLID:52;
then
A9: x <= 1 by Th26;
-1 <= x by A8,Th26;
then
A10: x in K by A9,XXREAL_1:1;
then
A11: (h|K).x = h.x by FUNCT_1:49;
dom h = dom arccos by VALUED_1:def 5
.= K by SIN_COS6:86;
then x in dom(h|K) by A10,RELAT_1:57;
then
A12: h|K is_continuous_in x by FCONT_1:def 2;
A13: dom h = dom arccos by VALUED_1:def 5;
then
A14: h.x = arccos.x*j by A10,SIN_COS6:86,VALUED_1:def 5
.= 1*arccos.x/P2 by XCMPLX_1:74;
per cases;
suppose
y = 0;
hence thesis by A7,Lm44,Th24;
end;
suppose
A15: y < 0;
for V being Subset of Z st V is open & C.p in V ex W being Subset
of TOUC st W is open & p in W & C.:W c= V
proof
set hh = h1-h;
let V be Subset of Z such that
A16: V is open and
A17: C.p in V;
reconsider V1 = V as Subset of REAL by A3,XBOOLE_1:1;
reconsider V2 = V1 as Subset of R^1 by TOPMETR:17;
V2 is open by A16,TSEP_1:17;
then reconsider V1 as open Subset of REAL by BORSUK_5:39;
consider N1 being Neighbourhood of C.p such that
A18: N1 c= V1 by A17,RCOMP_1:18;
A19: (hh|K).x = hh.x by A10,FUNCT_1:49;
dom hh = dom h1 /\ dom h by VALUED_1:12;
then
A20: dom hh = REAL /\ dom h
.= K by A13,SIN_COS6:86,XBOOLE_1:28;
then
A21: dom (hh|K) = K by RELAT_1:62;
A22: C.p = 1-arccos.x/P2 by A6,A15,SIN_COS6:def 4;
A23: p = (1,2) --> (x,y) by A4,TOPREALA:28;
x in dom(hh|K) by A10,A20,RELAT_1:57;
then
A24: hh|K is_continuous_in x by FCONT_1:def 2;
hh.x = h1.x - h.x by A10,A20,VALUED_1:13
.= 1-1*arccos.x/P2 by A10,A14,FUNCOP_1:7;
then consider N being Neighbourhood of x such that
A25: (hh|K).:N c= N1 by A22,A19,A24,FCONT_1:5;
set N3 = N /\ K;
A26: N3 c= K by XBOOLE_1:17;
reconsider N3, J as Subset of CIT by Lm2,XBOOLE_1:17,XXREAL_1:35;
set W = product ((1,2) --> (N3,J)) /\ X;
reconsider W as Subset of TOUC by XBOOLE_1:17;
take W;
reconsider KK = product ((1,2) --> (N3,J)) as Subset of TREC by
TOPREALA:38;
reconsider I3 = J as open Subset of CIT by TOPREALA:26;
A27: (hh|K).:N3 c= (hh|K).:N by RELAT_1:123,XBOOLE_1:17;
R^1(N) = N;
then reconsider M3 = N3 as open Subset of CIT by A2,TOPS_2:24;
KK = product ((1,2) --> (M3,I3));
then KK is open by TOPREALA:39;
hence W is open by A1,Lm16,TOPS_2:24;
x in N by RCOMP_1:16;
then
A28: x in N3 by A10,XBOOLE_0:def 4;
y >= -1 by A7,Th26;
then y in J by A15,XXREAL_1:3;
then p in product ((1,2) --> (N3,J)) by A23,A28,HILBERT3:11;
hence p in W by XBOOLE_0:def 4;
let m be object;
assume m in C.:W;
then consider c being Element of TOUC such that
A29: c in W and
A30: m = C.c by FUNCT_2:65;
A31: c in product ((1,2) --> (N3,J)) by A29,XBOOLE_0:def 4;
then
A32: c.1 in N3 by TOPREALA:3;
consider c1, c2 being Real such that
A33: c = |[c1,c2]| and
c2 >= 0 implies C.c = arccos c1/P2 and
A34: c2 <= 0 implies C.c = 1-arccos c1/P2 by Def13;
c.2 in J by A31,TOPREALA:3;
then c2 in J by A33,TOPREALA:29;
then
A35: 1-1*arccos c1*j = m by A30,A34,XCMPLX_1:74,XXREAL_1:3;
(hh|K).(c.1) = hh.(c.1) by A26,A32,FUNCT_1:49
.= h1.(c.1) - h.(c.1) by A20,A26,A32,VALUED_1:13
.= 1 - h.(c.1) by A32,FUNCOP_1:7
.= 1-arccos.(c.1)*j by A13,A26,A32,SIN_COS6:86,VALUED_1:def 5
.= 1-arccos.c1*j by A33,TOPREALA:29
.= 1-arccos c1*j by SIN_COS6:def 4;
then m in (hh|K).:N3 by A26,A32,A21,A35,FUNCT_1:def 6;
then m in (hh|K).:N by A27;
then m in N1 by A25;
hence thesis by A18;
end;
hence thesis by TMAP_1:43;
end;
suppose
A36: y > 0;
for V being Subset of Z st V is open & C.p in V ex W being Subset
of TOUC st W is open & p in W & C.:W c= V
proof
let V be Subset of Z such that
A37: V is open and
A38: C.p in V;
reconsider V1 = V as Subset of REAL by A3,XBOOLE_1:1;
reconsider V2 = V1 as Subset of R^1 by TOPMETR:17;
V2 is open by A37,TSEP_1:17;
then reconsider V1 as open Subset of REAL by BORSUK_5:39;
consider N1 being Neighbourhood of C.p such that
A39: N1 c= V1 by A38,RCOMP_1:18;
C.p = arccos.x/P2 by A5,A36,SIN_COS6:def 4;
then consider N being Neighbourhood of x such that
A40: (h|K).:N c= N1 by A11,A14,A12,FCONT_1:5;
set N3 = N /\ K;
A41: N3 c= K by XBOOLE_1:17;
reconsider N3, I as Subset of CIT by Lm2,XBOOLE_1:17,XXREAL_1:36;
set W = product ((1,2) --> (N3,I)) /\ X;
reconsider W as Subset of TOUC by XBOOLE_1:17;
take W;
reconsider KK = product ((1,2) --> (N3,I)) as Subset of TREC by
TOPREALA:38;
reconsider I3 = I as open Subset of CIT by TOPREALA:25;
A42: (h|K).:N3 c= (h|K).:N by RELAT_1:123,XBOOLE_1:17;
R^1(N) = N;
then reconsider M3 = N3 as open Subset of CIT by A2,TOPS_2:24;
KK = product ((1,2) --> (M3,I3));
then KK is open by TOPREALA:39;
hence W is open by A1,Lm16,TOPS_2:24;
x in N by RCOMP_1:16;
then
A43: x in N3 by A10,XBOOLE_0:def 4;
A44: dom (h|K) = K by A13,RELAT_1:62,SIN_COS6:86;
A45: p = (1,2) --> (x,y) by A4,TOPREALA:28;
y <= 1 by A7,Th26;
then y in I by A36,XXREAL_1:2;
then p in product ((1,2) --> (N3,I)) by A45,A43,HILBERT3:11;
hence p in W by XBOOLE_0:def 4;
let m be object;
assume m in C.:W;
then consider c being Element of TOUC such that
A46: c in W and
A47: m = C.c by FUNCT_2:65;
A48: c in product ((1,2) --> (N3,I)) by A46,XBOOLE_0:def 4;
then
A49: c.1 in N3 by TOPREALA:3;
consider c1, c2 being Real such that
A50: c = |[c1,c2]| and
A51: c2 >= 0 implies C.c = arccos c1/P2 and
c2 <= 0 implies C.c = 1-arccos c1/P2 by Def13;
c.2 in I by A48,TOPREALA:3;
then c2 in I by A50,TOPREALA:29;
then
A52: 1*arccos c1*j = m by A47,A51,XCMPLX_1:74,XXREAL_1:2;
(h|K).(c.1) = h.(c.1) by A41,A49,FUNCT_1:49
.= arccos.(c.1)*j by A13,A41,A49,SIN_COS6:86,VALUED_1:def 5
.= arccos.c1*j by A50,TOPREALA:29
.= arccos c1*j by SIN_COS6:def 4;
then m in (h|K).:N3 by A41,A49,A44,A52,FUNCT_1:def 6;
then m in (h|K).:N by A42;
then m in N1 by A40;
hence thesis by A39;
end;
hence thesis by TMAP_1:43;
end;
end;
hence thesis by TMAP_1:44;
end;
set A = ].1/2,1/2+p1.[;
set Q = ].-1,1.];
set E = [.0,PI.[;
reconsider Q, E as non empty Subset of REAL;
Lm46: the carrier of R^1 | R^1(Q) = R^1(Q) by PRE_TOPC:8;
Lm47: the carrier of R^1 | R^1(E) = R^1(E) by PRE_TOPC:8;
Lm48: the carrier of R^1 | R^1(A) = R^1(A) by PRE_TOPC:8;
set Af = AffineMap(-j,1) | R^1(E);
dom AffineMap(-j,1) = R by FUNCT_2:def 1,TOPMETR:17;
then
Lm49: dom Af = R^1(E) by RELAT_1:62;
rng Af c= A
proof
let y be object;
assume y in rng Af;
then consider x being object such that
A1: x in dom Af and
A2: Af.x = y by FUNCT_1:def 3;
reconsider x as Real by A1;
A3: y = AffineMap(-j,1).x by A1,A2,Lm49,FUNCT_1:49
.= (-j)*x+1 by FCONT_1:def 4
.= -j*x+1
.= -x/P2+1 by XCMPLX_1:99;
then reconsider y as Real;
x < PI by A1,Lm49,XXREAL_1:3;
then x/P2 < (1*PI)/P2 by XREAL_1:74;
then x/P2 < 1/2 by XCMPLX_1:91;
then -x/P2 > -1/2 by XREAL_1:24;
then
A4: -x/P2+1 > -1/2+1 by XREAL_1:6;
0 <= x by A1,Lm49,XXREAL_1:3;
then 0+1 >= -x/P2+1 by XREAL_1:6;
then y < 3/2 by A3,XXREAL_0:2;
hence thesis by A3,A4,XXREAL_1:4;
end;
then reconsider
Af as Function of R^1 | R^1(E), R^1 | R^1(A) by Lm47,Lm48,Lm49,FUNCT_2:2;
Lm50: R^1(AffineMap(-j,1)) = AffineMap(-j,1);
Lm51: dom AffineMap(-j,1) = REAL by FUNCT_2:def 1;
rng AffineMap(-j,1) = REAL by FCONT_1:55;
then reconsider
Af as continuous Function of R^1 | R^1(E), R^1 | R^1(A) by Lm35,Lm50,Lm51,
TOPMETR:17,TOPREALA:8;
set Af1 = AffineMap(j,1) | R^1(E);
dom AffineMap(j,1) = R by FUNCT_2:def 1,TOPMETR:17;
then
Lm52: dom Af1 = R^1(E) by RELAT_1:62;
rng Af1 c= A
proof
let y be object;
assume y in rng Af1;
then consider x being object such that
A1: x in dom Af1 and
A2: Af1.x = y by FUNCT_1:def 3;
reconsider x as Real by A1;
A3: y = AffineMap(j,1).x by A1,A2,Lm52,FUNCT_1:49
.= j*x+1 by FCONT_1:def 4
.= x/P2+1 by XCMPLX_1:99;
then reconsider y as Real;
x < PI by A1,Lm52,XXREAL_1:3;
then x/P2 < (1*PI)/P2 by XREAL_1:74;
then x/P2 < 1/2 by XCMPLX_1:91;
then
A4: x/P2+1 < 1/2+1 by XREAL_1:6;
0 <= x by A1,Lm52,XXREAL_1:3;
then 0+1 <= x/P2+1 by XREAL_1:6;
then 1/2 < y by A3,XXREAL_0:2;
hence thesis by A3,A4,XXREAL_1:4;
end;
then reconsider
Af1 as Function of R^1 | R^1(E), R^1 | R^1(A) by Lm47,Lm48,Lm52,FUNCT_2:2;
Lm53: R^1(AffineMap(j,1)) = AffineMap(j,1);
Lm54: dom AffineMap(j,1) = REAL by FUNCT_2:def 1;
rng AffineMap(j,1) = REAL by FCONT_1:55;
then reconsider
Af1 as continuous Function of R^1 | R^1(E), R^1 | R^1(A) by Lm35,Lm53,Lm54,
TOPMETR:17,TOPREALA:8;
set c = ac | R^1(Q);
Lm55: dom c = Q by RELAT_1:62,SIN_COS6:86,XXREAL_1:36;
Lm56: rng c c= E
proof
let y be object;
assume
A1: y in rng c;
then consider x being object such that
A2: x in dom c and
A3: c.x = y by FUNCT_1:def 3;
A4: rng c c= rng ac by RELAT_1:70;
then y in [.0,PI.] by A1,SIN_COS6:85;
then reconsider y as Real;
A5: 0 <= y by A1,A4,SIN_COS6:85,XXREAL_1:1;
A6: y <= PI by A1,A4,SIN_COS6:85,XXREAL_1:1;
reconsider x as Real by A2;
A7: -1 < x by A2,Lm55,XXREAL_1:2;
A8: x <= 1 by A2,Lm55,XXREAL_1:2;
y = arccos.x by A2,A3,Lm55,FUNCT_1:49
.= arccos x by SIN_COS6:def 4;
then y < PI by A6,A7,A8,SIN_COS6:98,XXREAL_0:1;
hence thesis by A5,XXREAL_1:3;
end;
then reconsider c as Function of R^1 | R^1(Q), R^1 | R^1(E) by Lm46,Lm47,Lm55,
FUNCT_2:2;
the carrier of R^1 | R^1[.-1,1.] = [.-1,1.] by PRE_TOPC:8;
then reconsider QQ = R^1(Q) as Subset of R^1 | R^1[.-1,1.] by XXREAL_1:36;
the carrier of R^1 | R^1[.0,PI.] = [.0,PI.] by PRE_TOPC:8;
then reconsider EE = R^1(E) as Subset of R^1 | R^1[.0,PI.] by XXREAL_1:35;
Lm57: (R^1 | R^1[.-1,1.]) | QQ = R^1 | R^1(Q) by GOBOARD9:2;
(R^1 | R^1[.0,PI.]) | EE = R^1 | R^1(E) by GOBOARD9:2;
then
Lm58: c is continuous by Lm57,TOPREALA:8;
Lm59: for aX1 being Subset of TOUCm st aX1 = {q where q is Point of TOP-REAL 2
: q in Xm & 0 <= q`2} holds Circle2IntervalL | (TOUCm|aX1) is continuous
proof
reconsider c1 = c[10] as Point of TOP-REAL 2;
let aX1 being Subset of TOUCm such that
A1: aX1 = {q where q is Point of TOP-REAL 2: q in Xm & 0 <= q`2};
A2: c1`2 = 0 by EUCLID:52;
c[10] is Point of Topen_unit_circle(c[-10]) by Lm15,Th23;
then c[10] in aX1 by A1,A2;
then reconsider aX1 as non empty Subset of TOUCm;
set X1 = TOUCm | aX1;
A3: cS1 is Subset of TOP-REAL 2 by TSEP_1:1;
[#]X1 is Subset of TUC by Lm9;
then reconsider B = [#]X1 as non empty Subset of TOP-REAL 2 by A3,XBOOLE_1:1;
set f = p|B;
A4: dom f = B by Lm40,RELAT_1:62;
A5: aX1 = the carrier of X1 by PRE_TOPC:8;
A6: rng f c= Q
proof
let y be object;
assume y in rng f;
then consider x being object such that
A7: x in dom f and
A8: f.x = y by FUNCT_1:def 3;
consider q being Point of TOP-REAL 2 such that
A9: q = x and
A10: q in Xm and
0 <= q`2 by A1,A5,A4,A7;
A11: -1 < q`1 by A10,Th28;
A12: q`1 <= 1 by A10,Th28;
y = p.x by A4,A7,A8,FUNCT_1:49
.= q`1 by A9,PSCOMP_1:def 5;
hence thesis by A11,A12,XXREAL_1:2;
end;
the carrier of (TOP-REAL 2) | B = B by PRE_TOPC:8;
then reconsider f as Function of (TOP-REAL 2) | B, R^1 | R^1(Q) by A4,A6,Lm46
,FUNCT_2:2;
X1 is SubSpace of TUC by TSEP_1:7;
then X1 is SubSpace of TOP-REAL 2 by TSEP_1:7;
then
A13: (TOP-REAL 2) | B = X1 by PRE_TOPC:def 5;
A14: for a being Point of X1 holds (Cm|X1).a = (Af1*(c*f)).a
proof
let a be Point of X1;
reconsider b = a as Point of TOUCm by PRE_TOPC:25;
consider x, y being Real such that
A15: b = |[x,y]| and
A16: y >= 0 implies Cm.b = 1+arccos x/P2 and
y <= 0 implies Cm.b = 1-arccos x/P2 by Def14;
A17: |[x,y]|`1 <= 1 by A15,Th28;
A18: |[x,y]|`1 = x by EUCLID:52;
-1 < |[x,y]|`1 by A15,Th28;
then
A19: x in Q by A18,A17,XXREAL_1:2;
then arccos.x = c.x by FUNCT_1:49;
then
A20: arccos.x in rng c by A19,Lm55,FUNCT_1:def 3;
a in aX1 by A5;
then ex q being Point of TOP-REAL 2 st a = q & q in Xm & 0 <= q`2 by A1;
hence (Cm|X1).a = 1+arccos x/P2 by A15,A16,EUCLID:52,FUNCT_1:49
.= 1+arccos.x/P2 by SIN_COS6:def 4
.= 1+j*(arccos.x) by XCMPLX_1:99
.= AffineMap(j,1).(arccos.x) by FCONT_1:def 4
.= Af1.(arccos.x) by A20,Lm56,FUNCT_1:49
.= Af1.(c.x) by A19,FUNCT_1:49
.= Af1.(c.(|[x,y]|`1)) by EUCLID:52
.= Af1.(c.(p.a)) by A15,PSCOMP_1:def 5
.= Af1.(c.(f.a)) by FUNCT_1:49
.= Af1.((c*f).a) by A13,FUNCT_2:15
.= (Af1*(c*f)).a by A13,FUNCT_2:15;
end;
f is continuous by Lm41,TOPREALA:8;
hence thesis by A13,A14,Lm58,FUNCT_2:63;
end;
Lm60: for aX1 being Subset of TOUCm st aX1 = {q where q is Point of TOP-REAL 2
: q in Xm & 0 >= q`2} holds Circle2IntervalL | (TOUCm|aX1) is continuous
proof
reconsider c1 = c[10] as Point of TOP-REAL 2;
let aX1 being Subset of TOUCm such that
A1: aX1 = {q where q is Point of TOP-REAL 2: q in Xm & 0 >= q`2};
A2: c1`2 = 0 by EUCLID:52;
c[10] is Point of Topen_unit_circle(c[-10]) by Lm15,Th23;
then c[10] in aX1 by A1,A2;
then reconsider aX1 as non empty Subset of TOUCm;
set X1 = TOUCm | aX1;
A3: cS1 is Subset of TOP-REAL 2 by TSEP_1:1;
[#]X1 is Subset of TUC by Lm9;
then reconsider B = [#]X1 as non empty Subset of TOP-REAL 2 by A3,XBOOLE_1:1;
set f = p|B;
A4: dom f = B by Lm40,RELAT_1:62;
A5: aX1 = the carrier of X1 by PRE_TOPC:8;
A6: rng f c= Q
proof
let y be object;
assume y in rng f;
then consider x being object such that
A7: x in dom f and
A8: f.x = y by FUNCT_1:def 3;
consider q being Point of TOP-REAL 2 such that
A9: q = x and
A10: q in Xm and
0 >= q`2 by A1,A5,A4,A7;
A11: -1 < q`1 by A10,Th28;
A12: q`1 <= 1 by A10,Th28;
y = p.x by A4,A7,A8,FUNCT_1:49
.= q`1 by A9,PSCOMP_1:def 5;
hence thesis by A11,A12,XXREAL_1:2;
end;
the carrier of (TOP-REAL 2) | B = B by PRE_TOPC:8;
then reconsider f as Function of (TOP-REAL 2) | B, R^1 | R^1(Q) by A4,A6,Lm46
,FUNCT_2:2;
X1 is SubSpace of TUC by TSEP_1:7;
then X1 is SubSpace of TOP-REAL 2 by TSEP_1:7;
then
A13: (TOP-REAL 2) | B = X1 by PRE_TOPC:def 5;
A14: for a being Point of X1 holds (Cm|X1).a = (Af*(c*f)).a
proof
let a be Point of X1;
reconsider b = a as Point of TOUCm by PRE_TOPC:25;
consider x, y being Real such that
A15: b = |[x,y]| and
y >= 0 implies Cm.b = 1+arccos x/P2 and
A16: y <= 0 implies Cm.b = 1-arccos x/P2 by Def14;
A17: |[x,y]|`1 <= 1 by A15,Th28;
A18: |[x,y]|`1 = x by EUCLID:52;
-1 < |[x,y]|`1 by A15,Th28;
then
A19: x in Q by A18,A17,XXREAL_1:2;
then arccos.x = c.x by FUNCT_1:49;
then
A20: arccos.x in rng c by A19,Lm55,FUNCT_1:def 3;
a in aX1 by A5;
then ex q being Point of TOP-REAL 2 st a = q & q in Xm & 0 >= q`2 by A1;
hence (Cm|X1).a = 1-arccos x/P2 by A15,A16,EUCLID:52,FUNCT_1:49
.= 1-arccos.x/P2 by SIN_COS6:def 4
.= 1-j*(arccos.x) by XCMPLX_1:99
.= (-j)*(arccos.x)+1
.= AffineMap(-j,1).(arccos.x) by FCONT_1:def 4
.= Af.(arccos.x) by A20,Lm56,FUNCT_1:49
.= Af.(c.x) by A19,FUNCT_1:49
.= Af.(c.(|[x,y]|`1)) by EUCLID:52
.= Af.(c.(p.a)) by A15,PSCOMP_1:def 5
.= Af.(c.(f.a)) by FUNCT_1:49
.= Af.((c*f).a) by A13,FUNCT_2:15
.= (Af*(c*f)).a by A13,FUNCT_2:15;
end;
f is continuous by Lm41,TOPREALA:8;
hence thesis by A13,A14,Lm58,FUNCT_2:63;
end;
Lm61: for p being Point of Topen_unit_circle(c[-10]) st p = c[10] holds
Circle2IntervalL is_continuous_at p
proof
reconsider c1 = c[10] as Point of TOP-REAL 2;
set aX2 = {q where q is Point of TOP-REAL 2: q in Xm & 0 >= q`2};
set aX1 = {q where q is Point of TOP-REAL 2: q in Xm & 0 <= q`2};
A1: aX1 c= Xm
proof
let x be object;
assume x in aX1;
then ex q being Point of TOP-REAL 2 st x = q & q in Xm & 0 <= q`2;
hence thesis;
end;
A2: aX2 c= Xm
proof
let x be object;
assume x in aX2;
then ex q being Point of TOP-REAL 2 st x = q & q in Xm & 0 >= q`2;
hence thesis;
end;
A3: TOUCm is SubSpace of TOUCm by TSEP_1:2;
A4: c1`2 = 0 by EUCLID:52;
A5: c[10] is Point of Topen_unit_circle(c[-10]) by Lm15,Th23;
then
A6: c[10] in aX1 by A4;
A7: c[10] in aX2 by A4,A5;
then reconsider aX1, aX2 as non empty Subset of TOUCm by A1,A2,A6;
set X1 = TOUCm | aX1;
let p be Point of Topen_unit_circle(c[-10]) such that
A8: p = c[10];
reconsider x1 = p as Point of X1 by A8,A6,PRE_TOPC:8;
set X2 = TOUCm | aX2;
reconsider x2 = p as Point of X2 by A8,A7,PRE_TOPC:8;
A9: the carrier of X2 = aX2 by PRE_TOPC:8;
Xm c= aX1 \/ aX2
proof
let a be object;
assume
A10: a in Xm;
then reconsider a as Point of TOP-REAL 2 by Lm8;
0 >= a`2 or 0 <= a`2;
then a in aX1 or a in aX2 by A10;
hence thesis by XBOOLE_0:def 3;
end;
then
A11: Xm = aX1 \/ aX2;
Cm|X2 is continuous by Lm60;
then
A12: Cm|X2 is_continuous_at x2;
Cm|X1 is continuous by Lm59;
then
A13: Cm|X1 is_continuous_at x1;
the carrier of X1 = aX1 by PRE_TOPC:8;
then TOUCm = X1 union X2 by A9,A3,A11,TSEP_1:def 2;
hence thesis by A13,A12,TMAP_1:113;
end;
Lm62: Circle2IntervalL is continuous
proof
set h = j(#)arccos;
set K = [.-1,1.];
set J = [.p0,0 .[;
set I = ].0,p1.];
set Z = R^1 | R^1(].1/2,1/2+p1.[);
for p being Point of TOUCm holds Cm is_continuous_at p
proof
Tcircle(0.TOP-REAL 2,1) is SubSpace of TREC by Th10;
then
A1: TOUCm is SubSpace of TREC by TSEP_1:7;
let p be Point of TOUCm;
A2: K = [#]CIT by TOPMETR:18;
reconsider q = p as Point of TOP-REAL 2 by Lm8;
A3: the carrier of Z = ].1/2,1/2+p1.[ by PRE_TOPC:8;
consider x, y being Real such that
A4: p = |[x,y]| and
A5: y >= 0 implies Cm.p = 1+arccos x/P2 and
A6: y <= 0 implies Cm.p = 1-arccos x/P2 by Def14;
A7: y = q`2 by A4,EUCLID:52;
A8: x = q`1 by A4,EUCLID:52;
then
A9: x <= 1 by Th26;
-1 <= x by A8,Th26;
then
A10: x in K by A9,XXREAL_1:1;
A11: dom h = dom arccos by VALUED_1:def 5;
then
A12: h.x = arccos.x*j by A10,SIN_COS6:86,VALUED_1:def 5
.= 1*arccos.x/P2 by XCMPLX_1:74;
per cases;
suppose
y = 0;
hence thesis by A7,Lm61,Th25;
end;
suppose
A13: y < 0;
for V being Subset of Z st V is open & Cm.p in V ex W being Subset
of TOUCm st W is open & p in W & Cm.:W c= V
proof
set hh = h1-h;
let V be Subset of Z such that
A14: V is open and
A15: Cm.p in V;
reconsider V1 = V as Subset of REAL by A3,XBOOLE_1:1;
reconsider V2 = V1 as Subset of R^1 by TOPMETR:17;
V2 is open by A14,TSEP_1:17;
then reconsider V1 as open Subset of REAL by BORSUK_5:39;
consider N1 being Neighbourhood of Cm.p such that
A16: N1 c= V1 by A15,RCOMP_1:18;
A17: (hh|K).x = hh.x by A10,FUNCT_1:49;
dom hh = dom h1 /\ dom h by VALUED_1:12;
then
A18: dom hh = REAL /\ dom h
.= K by A11,SIN_COS6:86,XBOOLE_1:28;
then
A19: dom (hh|K) = K by RELAT_1:62;
A20: Cm.p = 1-arccos.x/P2 by A6,A13,SIN_COS6:def 4;
A21: p = (1,2) --> (x,y) by A4,TOPREALA:28;
x in dom(hh|K) by A10,A18,RELAT_1:57;
then
A22: hh|K is_continuous_in x by FCONT_1:def 2;
hh.x = h1.x - h.x by A10,A18,VALUED_1:13
.= 1-1*arccos.x/P2 by A10,A12,FUNCOP_1:7;
then consider N being Neighbourhood of x such that
A23: (hh|K).:N c= N1 by A20,A17,A22,FCONT_1:5;
set N3 = N /\ K;
A24: N3 c= K by XBOOLE_1:17;
reconsider N3, J as Subset of CIT by Lm2,XBOOLE_1:17,XXREAL_1:35;
set W = product ((1,2) --> (N3,J)) /\ Xm;
reconsider W as Subset of TOUCm by XBOOLE_1:17;
take W;
reconsider KK = product ((1,2) --> (N3,J)) as Subset of TREC by
TOPREALA:38;
reconsider I3 = J as open Subset of CIT by TOPREALA:26;
A25: (hh|K).:N3 c= (hh|K).:N by RELAT_1:123,XBOOLE_1:17;
R^1(N) = N;
then reconsider M3 = N3 as open Subset of CIT by A2,TOPS_2:24;
KK = product ((1,2) --> (M3,I3));
then KK is open by TOPREALA:39;
hence W is open by A1,Lm17,TOPS_2:24;
x in N by RCOMP_1:16;
then
A26: x in N3 by A10,XBOOLE_0:def 4;
y >= -1 by A7,Th26;
then y in J by A13,XXREAL_1:3;
then p in product ((1,2) --> (N3,J)) by A21,A26,HILBERT3:11;
hence p in W by XBOOLE_0:def 4;
let m be object;
assume m in Cm.:W;
then consider c being Element of TOUCm such that
A27: c in W and
A28: m = Cm.c by FUNCT_2:65;
A29: c in product ((1,2) --> (N3,J)) by A27,XBOOLE_0:def 4;
then
A30: c.1 in N3 by TOPREALA:3;
consider c1, c2 being Real such that
A31: c = |[c1,c2]| and
c2 >= 0 implies Cm.c = 1+arccos c1/P2 and
A32: c2 <= 0 implies Cm.c = 1-arccos c1/P2 by Def14;
c.2 in J by A29,TOPREALA:3;
then c2 in J by A31,TOPREALA:29;
then
A33: 1-1*arccos c1*j = m by A28,A32,XCMPLX_1:74,XXREAL_1:3;
(hh|K).(c.1) = hh.(c.1) by A24,A30,FUNCT_1:49
.= h1.(c.1) - h.(c.1) by A18,A24,A30,VALUED_1:13
.= 1 - h.(c.1) by A30,FUNCOP_1:7
.= 1-arccos.(c.1)*j by A11,A24,A30,SIN_COS6:86,VALUED_1:def 5
.= 1-arccos.c1*j by A31,TOPREALA:29
.= 1-arccos c1*j by SIN_COS6:def 4;
then m in (hh|K).:N3 by A24,A30,A19,A33,FUNCT_1:def 6;
then m in (hh|K).:N by A25;
then m in N1 by A23;
hence thesis by A16;
end;
hence thesis by TMAP_1:43;
end;
suppose
A34: y > 0;
for V being Subset of Z st V is open & Cm.p in V ex W being Subset
of TOUCm st W is open & p in W & Cm.:W c= V
proof
set hh = h1+h;
let V be Subset of Z such that
A35: V is open and
A36: Cm.p in V;
reconsider V1 = V as Subset of REAL by A3,XBOOLE_1:1;
reconsider V2 = V1 as Subset of R^1 by TOPMETR:17;
V2 is open by A35,TSEP_1:17;
then reconsider V1 as open Subset of REAL by BORSUK_5:39;
consider N1 being Neighbourhood of Cm.p such that
A37: N1 c= V1 by A36,RCOMP_1:18;
A38: (hh|K).x = hh.x by A10,FUNCT_1:49;
dom hh = dom h1 /\ dom h by VALUED_1:def 1;
then
A39: dom hh = REAL /\ dom h
.= K by A11,SIN_COS6:86,XBOOLE_1:28;
then
A40: dom (hh|K) = K by RELAT_1:62;
A41: Cm.p = 1+arccos.x/P2 by A5,A34,SIN_COS6:def 4;
A42: p = (1,2) --> (x,y) by A4,TOPREALA:28;
x in dom(hh|K) by A10,A39,RELAT_1:57;
then
A43: hh|K is_continuous_in x by FCONT_1:def 2;
hh.x = h1.x + h.x by A10,A39,VALUED_1:def 1
.= 1+1*arccos.x/P2 by A10,A12,FUNCOP_1:7;
then consider N being Neighbourhood of x such that
A44: (hh|K).:N c= N1 by A41,A38,A43,FCONT_1:5;
set N3 = N /\ K;
A45: N3 c= K by XBOOLE_1:17;
reconsider N3, I as Subset of CIT by Lm2,XBOOLE_1:17,XXREAL_1:36;
set W = product ((1,2) --> (N3,I)) /\ Xm;
reconsider W as Subset of TOUCm by XBOOLE_1:17;
take W;
reconsider KK = product ((1,2) --> (N3,I)) as Subset of TREC by
TOPREALA:38;
reconsider I3 = I as open Subset of CIT by TOPREALA:25;
A46: (hh|K).:N3 c= (hh|K).:N by RELAT_1:123,XBOOLE_1:17;
R^1(N) = N;
then reconsider M3 = N3 as open Subset of CIT by A2,TOPS_2:24;
KK = product ((1,2) --> (M3,I3));
then KK is open by TOPREALA:39;
hence W is open by A1,Lm17,TOPS_2:24;
x in N by RCOMP_1:16;
then
A47: x in N3 by A10,XBOOLE_0:def 4;
y <= 1 by A7,Th26;
then y in I by A34,XXREAL_1:2;
then p in product ((1,2) --> (N3,I)) by A42,A47,HILBERT3:11;
hence p in W by XBOOLE_0:def 4;
let m be object;
assume m in Cm.:W;
then consider c being Element of TOUCm such that
A48: c in W and
A49: m = Cm.c by FUNCT_2:65;
A50: c in product ((1,2) --> (N3,I)) by A48,XBOOLE_0:def 4;
then
A51: c.1 in N3 by TOPREALA:3;
consider c1, c2 being Real such that
A52: c = |[c1,c2]| and
A53: c2 >= 0 implies Cm.c = 1+arccos c1/P2 and
c2 <= 0 implies Cm.c = 1-arccos c1/P2 by Def14;
c.2 in I by A50,TOPREALA:3;
then c2 in I by A52,TOPREALA:29;
then
A54: 1+1*arccos c1*j = m by A49,A53,XCMPLX_1:74,XXREAL_1:2;
(hh|K).(c.1) = hh.(c.1) by A45,A51,FUNCT_1:49
.= h1.(c.1) + h.(c.1) by A39,A45,A51,VALUED_1:def 1
.= 1 + h.(c.1) by A51,FUNCOP_1:7
.= 1+arccos.(c.1)*j by A11,A45,A51,SIN_COS6:86,VALUED_1:def 5
.= 1+arccos.c1*j by A52,TOPREALA:29
.= 1+arccos c1*j by SIN_COS6:def 4;
then m in (hh|K).:N3 by A45,A51,A40,A54,FUNCT_1:def 6;
then m in (hh|K).:N by A46;
then m in N1 by A44;
hence thesis by A37;
end;
hence thesis by TMAP_1:43;
end;
end;
hence thesis by TMAP_1:44;
end;
registration
cluster Circle2IntervalR -> one-to-one onto continuous;
coherence by Lm45,Th42,GRCAT_1:41;
cluster Circle2IntervalL -> one-to-one onto continuous;
coherence by Lm62,Th43,GRCAT_1:41;
end;
Lm63: CircleMap(R^1(0)) is open
proof
CircleMap.R^1(0) = c[10] by Th32;
hence thesis by Th42,TOPREALA:14;
end;
Lm64: CircleMap(R^1(1/2)) is open by Lm19,Th43,TOPREALA:14;
registration
let i be Integer;
cluster CircleMap(R^1(i)) -> open;
coherence
proof
set F = AffineMap(1,-i);
set f = F | ].0+i,0+i+p1.[;
A1: the carrier of R^1|R^1(].0,1.[) = R^1(].0,1.[) by PRE_TOPC:8;
dom F = REAL by FUNCT_2:def 1;
then
A2: dom f = ].i,i+1.[ by RELAT_1:62;
A3: rng f = ].0,0+1.[ by Lm24;
the carrier of R^1|R^1(].i,i+1.[) = R^1(].i,i+1.[) by PRE_TOPC:8;
then reconsider
f as Function of R^1|R^1(].i,i+p1.[), R^1|R^1(].0,0+p1.[) by A1,A2,A3,
FUNCT_2:2;
A4: CircleMap(R^1(0+i)) = CircleMap(R^1(0)) * f by Th41;
A5: R^1 | R^1(rng F) = R^1 by Lm12;
A6: CircleMap.R^1(i) = c[10] by Th32
.= CircleMap.R^1(0) by Th32;
A7: R^1 | R^1(dom F) = R^1 by Lm12;
A8: R^1(F) = F;
f is onto by A1,A3;
then f is open by A7,A5,A8,TOPREALA:10;
hence thesis by A4,A6,Lm63,TOPREALA:11;
end;
cluster CircleMap(R^1(1/2+i)) -> open;
coherence
proof
1/2-1 < 0;
then [\1/2/] = 0 by INT_1:def 6;
then
A9: 1/2-[\1/2/] = 1/2;
frac(1/2+i) = frac(1/2) by INT_1:66
.= 1/2 by A9,INT_1:def 8;
then
A10: CircleMap.R^1(1/2+i) = CircleMap.R^1(1/2+0) by Lm19,Th34;
set F = AffineMap(1,-i);
set f = F | ].1/2+i,1/2+i+p1.[;
A11: the carrier of R^1|R^1(].1/2,3/2.[) = R^1(].1/2,3/2.[) by PRE_TOPC:8;
dom F = REAL by FUNCT_2:def 1;
then
A12: dom f = ].1/2+i,1/2+i+1.[ by RELAT_1:62;
A13: rng f = ].1/2,1/2+1.[ by Lm24;
the carrier of R^1|R^1(].1/2+i,1/2+i+1.[) = R^1(].1/2+i,1/2+i+1.[) by
PRE_TOPC:8;
then reconsider
f as Function of R^1|R^1(].1/2+i,1/2+i+p1.[), R^1|R^1(].1/2,1/2
+p1.[) by A11,A12,A13,FUNCT_2:2;
A14: CircleMap(R^1(1/2+i)) = CircleMap(R^1(1/2)) * f by Th41;
A15: R^1 | R^1(rng F) = R^1 by Lm12;
A16: R^1 | R^1(dom F) = R^1 by Lm12;
A17: R^1(F) = F;
f is onto by A11,A13;
then f is open by A16,A15,A17,TOPREALA:10;
hence thesis by A14,A10,Lm64,TOPREALA:11;
end;
end;
registration
cluster Circle2IntervalR -> open;
coherence
proof
CircleMap.R^1(0) = c[10] by Th32;
hence thesis by Th42,TOPREALA:13;
end;
cluster Circle2IntervalL -> open;
coherence by Lm19,Th43,TOPREALA:13;
end;
theorem
CircleMap(R^1(1/2)) is being_homeomorphism
proof
reconsider r = 0 as Integer;
CircleMap(R^1(1/2+r)) is open;
hence thesis by TOPREALA:16;
end;
theorem
ex F being Subset-Family of Tunit_circle(2) st F = { CircleMap.:].0,1
.[, CircleMap.:].1/2,3/2.[ } & F is Cover of Tunit_circle(2) & F is open & for
U being Subset of Tunit_circle(2) holds ( U = CircleMap.:].0,1.[ implies union
IntIntervals(0,1) = (CircleMap)"U & for d being Subset of R^1 st d in
IntIntervals(0,1) for f being Function of R^1 | d, (Tunit_circle(2)) | U st f =
CircleMap|d holds f is being_homeomorphism ) & ( U = CircleMap.:].1/2,3/2.[
implies union IntIntervals(1/2,3/2) = (CircleMap)"U & for d being Subset of R^1
st d in IntIntervals(1/2,3/2) for f being Function of R^1 | d, (Tunit_circle(2)
) | U st f = CircleMap|d holds f is being_homeomorphism )
proof
set D2 = IntIntervals(1/2,3/2);
set D1 = IntIntervals(0,1);
set F1 = CircleMap.:union D1;
set F2 = CircleMap.:union D2;
set F = {F1,F2};
reconsider F as Subset-Family of TUC;
take F;
].1/2+0,3/2+0 .[ in D2 by Lm1;
then
A1: F2 = CircleMap.:].1/2,3/2.[ by Th40;
A2: ].0+0,1+0 .[ in D1 by Lm1;
hence F = {CircleMap.:].0,1.[, CircleMap.:].1/2,3/2.[} by A1,Th40;
thus F is Cover of TUC
proof
reconsider A = [.0,0+1.[ as Subset of R^1 by TOPMETR:17;
reconsider f = CircleMap | A as Function of R^1|A,TUC by Lm21;
let a be object;
A3: F2 in F by TARSKI:def 2;
f is onto by Th38;
then
A4: rng f = cS1;
assume a in the carrier of TUC;
then consider x being object such that
A5: x in dom f and
A6: f.x = a by A4,FUNCT_1:def 3;
A7: dom f = A by Lm18,RELAT_1:62;
then reconsider x as Element of REAL by A5;
A8: CircleMap.x = f.x by A5,FUNCT_1:47;
per cases by A5,A7,XXREAL_1:3;
suppose
A9: x = 0;
0 in A by XXREAL_1:3;
then
A10: f.0 = CircleMap.0 by FUNCT_1:49
.= c[10] by Th32
.= CircleMap.1 by Th32;
1 in ].1/2,3/2.[ by XXREAL_1:4;
then a in CircleMap.:].1/2,3/2.[ by A6,A9,A10,Lm18,FUNCT_1:def 6;
hence a in union F by A1,A3,TARSKI:def 4;
end;
suppose
A11: 0 < x & x < 1;
A12: ].0+0,1+0 .[ in D1 by Lm1;
x in ].0,1.[ by A11,XXREAL_1:4;
then x in union D1 by A12,TARSKI:def 4;
then
A13: a in F1 by A6,A8,Lm18,FUNCT_1:def 6;
F1 in F by TARSKI:def 2;
hence a in union F by A13,TARSKI:def 4;
end;
suppose
x >= 1 & x < 1;
hence a in union F;
end;
end;
A14: F1 = CircleMap.:].0,1.[ by A2,Th40;
thus F is open
proof
reconsider r = 0 as Integer;
A15: now
let A be Subset of REAL;
A c= A;
hence A is Subset of R^1 | R^1(A) by PRE_TOPC:8;
end;
then reconsider M = ].0,1.[ as Subset of R^1 | R^1(].r,r+1.[);
reconsider N = ].1/2,3/2.[ as Subset of R^1 | R^1(].1/2+r,1/2+r+1.[) by A15
;
let P be Subset of TUC;
A16: now
let A be open Subset of REAL;
reconsider B = A as Subset of R^1 | R^1(A) by A15;
the carrier of R^1 | R^1(A) = A by PRE_TOPC:8;
then B = [#](R^1 | R^1(A)) /\ R^1(A);
hence A is open Subset of R^1 | R^1(A) by TOPS_2:24;
end;
then M is open;
then
A17: (CircleMap(R^1(r))).:M is open by T_0TOPSP:def 2;
N is open by A16;
then
A18: (CircleMap(R^1(1/2+r))).:N is open by T_0TOPSP:def 2;
CircleMap.:].1/2,3/2.[ = (CircleMap(R^1(1/2))).:].1/2,3/2.[ by RELAT_1:129;
then
A19: F2 is open by A1,A18,TSEP_1:17;
CircleMap.:].0,1.[ = (CircleMap(R^1(0))).:].0,1.[ by RELAT_1:129;
then F1 is open by A14,A17,TSEP_1:17;
hence thesis by A19,TARSKI:def 2;
end;
let U be Subset of TUC;
A20: c[10] in {c[10]} by TARSKI:def 1;
thus U = CircleMap.:].0,1.[ implies union IntIntervals(0,1) = (CircleMap)"U
& for d being Subset of R^1 st d in IntIntervals(0,1) for f being Function of
R^1 | d, (Tunit_circle(2)) | U st f = CircleMap|d holds f is
being_homeomorphism
proof
assume
A21: U = CircleMap.:].0,1.[;
then reconsider U1 = U as non empty Subset of TUC by Lm18;
A22: [#](TUC | U) = U by PRE_TOPC:def 5;
].0+0,1+0 .[ in D1 by Lm1;
then
A23: CircleMap.:].0,1.[ = CircleMap.:union D1 by Th40;
now
let x1, x2 be Element of R^1;
set k = [\x2/];
set K = ].0+k,1+k.[;
assume x1 in union D1;
then consider Z being set such that
A24: x1 in Z and
A25: Z in D1 by TARSKI:def 4;
consider n being Element of INT such that
A26: Z = ].0+n,1+n.[ by A25;
x1 < 1+n by A24,A26,XXREAL_1:4;
then
A27: x1-1 < 1+n-1 by XREAL_1:9;
then x1-1-n < n-n by XREAL_1:9;
then x1-n-1+1 < 0+1 by XREAL_1:8;
then
A28: 2*PI*(x1-n) < 2*PI*1 by XREAL_1:68;
A29: CircleMap.(x2-k) = |[ cos(2*PI*(x2-k)), sin(2*PI*(x2-k)) ]| by Def11;
x2-1 < k by INT_1:def 6;
then x2-1-k < k-k by XREAL_1:9;
then x2-1-k+1 < 0+1 by XREAL_1:6;
then
A30: 2*PI*(x2-k) < 2*PI*1 by XREAL_1:68;
assume
A31: CircleMap.x1 = CircleMap.x2;
A32: n < x1 by A24,A26,XXREAL_1:4;
then
A33: 0 < x1-n by XREAL_1:50;
k in INT by INT_1:def 2;
then
A34: K in D1;
A35: CircleMap.x2 = CircleMap.(x2+-k) by Th31;
[\x1/] = n by A32,A27,INT_1:def 6;
then
A36: not x1 in INT by A32,INT_1:26;
A37: now
assume k = x2;
then CircleMap.x1 = c[10] by A31,Th32;
hence contradiction by A20,A36,Lm18,Th33,FUNCT_1:def 7,TOPMETR:17;
end;
A38: CircleMap.(x1-n) = |[ cos(2*PI*(x1-n)), sin(2*PI*(x1-n)) ]| by Def11;
A39: CircleMap.x1 = CircleMap.(x1+-n) by Th31;
then
A40: cos(2*PI*(x1-n)) = cos(2*PI*(x2-k)) by A31,A35,A38,A29,SPPOL_2:1;
A41: sin(2*PI*(x1-n)) = sin(2*PI*(x2-k)) by A31,A39,A35,A38,A29,SPPOL_2:1;
k <= x2 by INT_1:def 6;
then
A42: k < x2 by A37,XXREAL_0:1;
then 0 <= x2-k by XREAL_1:50;
then 2*PI*(x1-n) = 2*PI*(x2-k) by A33,A28,A30,A40,A41,COMPLEX2:11;
then x1-n = x2-k by XCMPLX_1:5;
then
A43: x2 = x1-n+k;
x1 < 1+n by A24,A26,XXREAL_1:4;
then x1-n < 1 by XREAL_1:19;
then x2 < 1+k by A43,XREAL_1:6;
then x2 in K by A42,XXREAL_1:4;
hence x2 in union D1 by A34,TARSKI:def 4;
end;
hence union D1 = (CircleMap)"U by A21,A23,T_0TOPSP:1;
let d be Subset of R^1;
assume
A44: d in D1;
then consider n being Element of INT such that
A45: d = ].0+n,1+n.[;
reconsider d1 = d as non empty Subset of R^1 by A45;
reconsider J = ].n,n+p1.[ as non empty Subset of R^1 by TOPMETR:17;
A46: CircleMap|d = CircleMap|J|d1 by A45,RELAT_1:74;
let f be Function of R^1 | d, TUC | U;
reconsider f1 = f as Function of R^1 | d1, TUC | U1;
assume
A47: f = CircleMap|d;
then
A48: f is continuous by TOPREALA:8;
d c= J by A45;
then reconsider d2 = d as Subset of R^1|J by PRE_TOPC:8;
A49: R^1|J|d2 = R^1|d by A45,PRE_TOPC:7;
reconsider F = CircleMap|J as Function of R^1|J,TUC by Lm21;
CircleMap(R^1(n)) is open;
then
A50: F is open by TOPREALA:12;
A51: F1 = CircleMap.:d by A44,Th40;
A52: f1 is onto
proof
thus rng f1 c= the carrier of TUC | U1;
let b be object;
A53: dom (CircleMap|d) = d by Lm18,RELAT_1:62,TOPMETR:17;
assume b in the carrier of TUC | U1;
then consider a being Element of R^1 such that
A54: a in d and
A55: b = CircleMap.a by A21,A23,A22,A51,FUNCT_2:65;
(CircleMap|d).a = CircleMap.a by A54,FUNCT_1:49;
hence thesis by A47,A54,A55,A53,FUNCT_1:def 3;
end;
f is one-to-one by A44,A47,Lm3,Th39;
hence thesis by A47,A48,A49,A46,A52,A50,TOPREALA:10,16;
end;
assume
A56: U = CircleMap.:].1/2,3/2.[;
then reconsider U1 = U as non empty Subset of TUC by Lm18;
now
let x1, x2 be Element of R^1;
set k = [\x2/];
A57: k <= x2 by INT_1:def 6;
assume x1 in union D2;
then consider Z being set such that
A58: x1 in Z and
A59: Z in D2 by TARSKI:def 4;
consider n being Element of INT such that
A60: Z = ].1/2+n,3/2+n.[ by A59;
A61: 1/2+n < x1 by A58,A60,XXREAL_1:4;
0+n < 1/2+n by XREAL_1:8;
then
A62: n < x1 by A61,XXREAL_0:2;
assume
A63: CircleMap.x1 = CircleMap.x2;
A64: x1 < 3/2+n by A58,A60,XXREAL_1:4;
then
A65: x1-n < 3/2 by XREAL_1:19;
per cases by XXREAL_0:1;
suppose
x1 = 1+n;
then CircleMap.x2 = c[10] by A63,Th32;
then reconsider w = x2 as Element of INT by A20,Lm18,Th33,FUNCT_1:def 7
,TOPMETR:17;
A66: 0+w < 1/2+w by XREAL_1:8;
w-1 in INT by INT_1:def 2;
then
A67: ].1/2+(w-1),3/2+(w-1).[ in D2;
-1/2+w < 0+w by XREAL_1:8;
then x2 in ].1/2+(w-1),3/2+(w-1).[ by A66,XXREAL_1:4;
hence x2 in union D2 by A67,TARSKI:def 4;
end;
suppose
x1 < 1+n;
then x1-1 < n+1-1 by XREAL_1:9;
then x1-1-n < n-n by XREAL_1:9;
then x1-n-1+1 < 0+1 by XREAL_1:8;
then
A68: 2*PI*(x1-n) < 2*PI*1 by XREAL_1:68;
set K = ].1/2+k,3/2+k.[;
k in INT by INT_1:def 2;
then
A69: K in D2;
A70: x2-x2 <= x2-k by A57,XREAL_1:13;
A71: 0 < x1-n by A62,XREAL_1:50;
A72: CircleMap.(x2-k) = |[ cos(2*PI*(x2-k)), sin(2*PI*(x2-k)) ]| by Def11;
x2-1 < k by INT_1:def 6;
then x2-1-k < k-k by XREAL_1:9;
then x2-1-k+1 < 0+1 by XREAL_1:6;
then
A73: 2*PI*(x2-k) < 2*PI*1 by XREAL_1:68;
A74: CircleMap.x2 = CircleMap.(x2+-k) by Th31;
1/2+n-n < x1-n by A61,XREAL_1:9;
then
A75: 1/2+k < x1-n+k by XREAL_1:8;
A76: CircleMap.(x1-n) = |[ cos(2*PI*(x1-n)), sin(2*PI*(x1-n)) ]| by Def11;
A77: CircleMap.x1 = CircleMap.(x1+-n) by Th31;
then
A78: sin(2*PI*(x1-n)) = sin(2*PI*(x2-k)) by A63,A74,A76,A72,SPPOL_2:1;
cos(2*PI*(x1-n)) = cos(2*PI*(x2-k)) by A63,A77,A74,A76,A72,SPPOL_2:1;
then 2*PI*(x1-n) = 2*PI*(x2-k) by A78,A71,A68,A70,A73,COMPLEX2:11;
then
A79: x1-n = x2-k by XCMPLX_1:5;
then x2 = x1-n+k;
then x2 < 3/2+k by A65,XREAL_1:6;
then x2 in K by A79,A75,XXREAL_1:4;
hence x2 in union D2 by A69,TARSKI:def 4;
end;
suppose
x1 > 1+n;
then
A80: n+1-1 < x1-1 by XREAL_1:9;
then
A81: n-n < x1-1-n by XREAL_1:9;
set K = ].1/2+(k-1),3/2+(k-1).[;
A82: -1/2 < 0;
n-n < x1-1-n by A80,XREAL_1:9;
then
A83: -1/2+k < x1-1-n+k by A82,XREAL_1:8;
k-1 in INT by INT_1:def 2;
then
A84: K in D2;
A85: x1-n-1 < 3/2-1 by A65,XREAL_1:9;
A86: x2-x2 <= x2-k by A57,XREAL_1:13;
A87: CircleMap.(x2-k) = |[ cos(2*PI*(x2-k)), sin(2*PI*(x2-k)) ]| by Def11;
x1-1 < 3/2+n-1 by A64,XREAL_1:9;
then x1-1-n < 1/2+n-n by XREAL_1:9;
then x1-1-n < 1 by XXREAL_0:2;
then
A88: 2*PI*(x1-1-n) < 2*PI*1 by XREAL_1:68;
A89: CircleMap.x2 = CircleMap.(x2+-k) by Th31;
x2-1 < k by INT_1:def 6;
then x2-1-k < k-k by XREAL_1:9;
then x2-1-k+1 < 0+1 by XREAL_1:6;
then
A90: 2*PI*(x2-k) < 2*PI*1 by XREAL_1:68;
A91: CircleMap.(x1-1-n) = |[ cos(2*PI*(x1-1-n)), sin(2*PI*(x1-1-n)) ]|
by Def11;
A92: CircleMap.x1 = CircleMap.(x1+(-1-n)) by Th31;
then
A93: sin(2*PI*(x1-1-n)) = sin(2*PI*(x2-k)) by A63,A89,A91,A87,SPPOL_2:1;
cos(2*PI*(x1-1-n)) = cos(2*PI*(x2-k)) by A63,A92,A89,A91,A87,SPPOL_2:1;
then 2*PI*(x1-1-n) = 2*PI*(x2-k) by A93,A81,A88,A86,A90,COMPLEX2:11;
then
A94: x1-1-n = x2-k by XCMPLX_1:5;
then x2 = x1-1-n+k;
then x2 < 1/2+k by A85,XREAL_1:6;
then x2 in K by A94,A83,XXREAL_1:4;
hence x2 in union D2 by A84,TARSKI:def 4;
end;
end;
hence union D2 = (CircleMap)"U by A1,A56,T_0TOPSP:1;
let d be Subset of R^1;
assume
A95: d in D2;
then consider n being Element of INT such that
A96: d = ].1/2+n,3/2+n.[;
A97: 1+n < 3/2+n by XREAL_1:6;
1/2+n < 1+n by XREAL_1:6;
then reconsider d1 = d as non empty Subset of R^1 by A96,A97,XXREAL_1:4;
A98: [#](TUC | U) = U by PRE_TOPC:def 5;
let f be Function of R^1 | d, TUC | U;
reconsider f1 = f as Function of R^1 | d1, TUC | U1;
assume
A99: f = CircleMap|d;
then
A100: f is continuous by TOPREALA:8;
reconsider J = ].1/2+n,1/2+n+p1.[ as non empty Subset of R^1 by TOPMETR:17;
A101: CircleMap|d = CircleMap|J|d1 by A96,RELAT_1:74;
d c= J by A96;
then reconsider d2 = d as Subset of R^1|J by PRE_TOPC:8;
A102: R^1|J|d2 = R^1|d by A96,PRE_TOPC:7;
A103: F2 = CircleMap.:d by A95,Th40;
A104: f1 is onto
proof
thus rng f1 c= the carrier of TUC | U1;
let b be object;
A105: dom (CircleMap|d) = d by Lm18,RELAT_1:62,TOPMETR:17;
assume b in the carrier of TUC | U1;
then consider a being Element of R^1 such that
A106: a in d and
A107: b = CircleMap.a by A1,A56,A98,A103,FUNCT_2:65;
(CircleMap|d).a = CircleMap.a by A106,FUNCT_1:49;
hence thesis by A99,A106,A107,A105,FUNCT_1:def 3;
end;
reconsider F = CircleMap|J as Function of R^1|J,TUC by Lm21;
CircleMap(R^1(1/2+n)) is open;
then
A108: F is open by TOPREALA:12;
f is one-to-one by A95,A99,Lm4,Th39;
hence thesis by A99,A100,A102,A101,A104,A108,TOPREALA:10,16;
end;