:: Some Properties of Circles on the Plane :: by Artur Korni{\l}owicz and Yasunari Shidama :: :: Received October 18, 2004 :: Copyright (c) 2004-2016 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, ZFMISC_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, BORSUK_1, SETFAM_1; equalities XBOOLE_0, TMAP_1, STRUCT_0, TOPREALA, SQUARE_1, TOPREAL9, SUBSET_1, ALGSTR_0, ORDINAL1; 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; 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; 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 by FUNCOP_1:7 .= 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 by FUNCOP_1:7 .= 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 by SQUARE_1:22; 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 by SQUARE_1:22; 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 by SQUARE_1:22; 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; dom (Af*(c*f)) = the carrier of (TOP-REAL 2)|B by FUNCT_2:def 1; then A19: (Af*(c*f)).a in rng (Af*(c*f)) by A13,FUNCT_1:def 3; reconsider r = (Af*(c*f)).a as Real; 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,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 by FUNCOP_1:13 .= 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 by FUNCOP_1:13 .= 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 by FUNCOP_1:13 .= 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;