:: Some Properties of Circles on the Plane :: by Artur Korni{\l}owicz and Yasunari Shidama :: :: Received October 18, 2004 :: Copyright (c) 2004-2012 Association of Mizar Users begin 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 real negative number ; reconsider p1 = 1 as real positive number ; set CIT = Closed-Interval-TSpace ((- 1),1); set cCIT = the carrier of (Closed-Interval-TSpace ((- 1),1)); Lm2: the carrier of (Closed-Interval-TSpace ((- 1),1)) = [.(- 1),1.] by TOPMETR:18; Lm3: 1 - 0 <= 1 ; Lm4: (3 / 2) - (1 / 2) <= 1 ; registration clusterK108(0,1) -> non empty ; coherence not ].0,1.[ is empty ; clusterK105((- 1),1) -> non empty ; coherence not [.(- 1),1.] is empty ; clusterK108((1 / 2),(3 / 2)) -> non empty ; coherence not ].(1 / 2),(3 / 2).[ is empty proofend; 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 for Y being non empty SubSpace of X for Z being non empty SubSpace of Y for p being Point of Z holds p is Point of X proofend; Lm9: for X being TopSpace for Y being SubSpace of X for Z being SubSpace of Y for A being Subset of Z holds A is Subset of X proofend; registration cluster sin -> continuous ; coherence sin is continuous ; cluster cos -> continuous ; coherence cos is continuous ; cluster arcsin -> continuous ; coherence arcsin is continuous by RELAT_1:69, SIN_COS6:63, SIN_COS6:84; cluster arccos -> continuous ; coherence arccos is continuous by RELAT_1:69, SIN_COS6:86, SIN_COS6:107; end; theorem Th1: :: TOPREALB:1 for a, r, b being real number holds sin ((a * r) + b) = (sin * (AffineMap (a,b))) . r proofend; theorem Th2: :: TOPREALB:2 for a, r, b being real number holds cos ((a * r) + b) = (cos * (AffineMap (a,b))) . r proofend; registration let a be non zero real number ; let b be real number ; cluster AffineMap (a,b) -> one-to-one onto ; coherence ( AffineMap (a,b) is onto & AffineMap (a,b) is one-to-one ) proofend; end; definition let a, b be real number ; func IntIntervals (a,b) -> set equals :: TOPREALB:def 1 { ].(a + n),(b + n).[ where n is Element of INT : verum } ; coherence { ].(a + n),(b + n).[ where n is Element of INT : verum } is set ; end; :: deftheorem defines IntIntervals TOPREALB:def_1_:_ for a, b being real number holds IntIntervals (a,b) = { ].(a + n),(b + n).[ where n is Element of INT : verum } ; theorem :: TOPREALB:3 for a, b being real number 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 number ; cluster IntIntervals (a,b) -> non empty ; coherence not IntIntervals (a,b) is empty proofend; end; theorem :: TOPREALB:4 for b, a being real number st b - a <= 1 holds IntIntervals (a,b) is mutually-disjoint proofend; definition let a, b be real number ; :: original:IntIntervals redefine func IntIntervals (a,b) -> Subset-Family of R^1; coherence IntIntervals (a,b) is Subset-Family of R^1 proofend; end; definition let a, b be real number ; :: original:IntIntervals redefine func IntIntervals (a,b) -> open Subset-Family of R^1; coherence IntIntervals (a,b) is open Subset-Family of R^1 proofend; end; begin definition let r be real number ; func R^1 r -> Point of R^1 equals :: TOPREALB:def 2 r; coherence r is Point of R^1 by TOPMETR:17, XREAL_0:def_1; end; :: deftheorem defines R^1 TOPREALB:def_2_:_ for r being real number holds R^1 r = r; definition let A be Subset of REAL; func R^1 A -> Subset of R^1 equals :: TOPREALB:def 3 A; coherence A is Subset of R^1 by TOPMETR:17; end; :: deftheorem defines R^1 TOPREALB:def_3_:_ for A being Subset of REAL holds R^1 A = A; registration let A be non empty Subset of REAL; cluster R^1 A -> non empty ; coherence not R^1 A is empty ; end; registration let A be open Subset of REAL; cluster R^1 A -> open ; coherence R^1 A is open by BORSUK_5:39; end; registration let A be closed Subset of REAL; cluster R^1 A -> closed ; coherence R^1 A is closed by JORDAN5A:23; end; registration let A be open Subset of REAL; clusterR^1 | (R^1 A) -> open ; coherence R^1 | (R^1 A) is open proofend; end; registration let A be closed Subset of REAL; clusterR^1 | (R^1 A) -> closed ; coherence R^1 | (R^1 A) is closed proofend; 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 :: TOPREALB:def 4 f; coherence f is Function of (R^1 | (R^1 (dom f))),(R^1 | (R^1 (rng f))) proofend; end; :: deftheorem defines R^1 TOPREALB:def_4_:_ for f being PartFunc of REAL,REAL holds R^1 f = f; registration let f be PartFunc of REAL,REAL; cluster R^1 f -> onto ; coherence R^1 f is onto proofend; end; registration let f be one-to-one PartFunc of REAL,REAL; cluster R^1 f -> one-to-one ; coherence R^1 f is one-to-one ; end; theorem Th5: :: TOPREALB:5 R^1 | (R^1 ([#] REAL)) = R^1 proofend; theorem Th6: :: TOPREALB:6 for f being PartFunc of REAL,REAL st dom f = REAL holds R^1 | (R^1 (dom f)) = R^1 proofend; theorem Th7: :: TOPREALB:7 for f being Function of REAL,REAL holds f is Function of R^1,(R^1 | (R^1 (rng f))) proofend; theorem Th8: :: TOPREALB:8 for f being Function of REAL,REAL holds f is Function of R^1,R^1 proofend; Lm10: sin is Function of R^1,R^1 proofend; Lm11: cos is Function of R^1,R^1 proofend; registration let f be continuous PartFunc of REAL,REAL; cluster R^1 f -> continuous ; coherence R^1 f is continuous proofend; end; set A = R^1 ].0,1.[; Lm12: now__::_thesis:_for_a_being_non_zero_real_number_ for_b_being_real_number_holds_ (_R^1_=_R^1_|_(R^1_(dom_(AffineMap_(a,b))))_&_R^1_=_R^1_|_(R^1_(rng_(AffineMap_(a,b))))_) let a be non zero real number ; ::_thesis: for b being real number holds ( R^1 = R^1 | (R^1 (dom (AffineMap (a,b)))) & R^1 = R^1 | (R^1 (rng (AffineMap (a,b)))) ) let b be real number ; ::_thesis: ( R^1 = R^1 | (R^1 (dom (AffineMap (a,b)))) & R^1 = R^1 | (R^1 (rng (AffineMap (a,b)))) ) 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; ::_thesis: verum end; registration let a be non zero real number ; let b be real number ; cluster R^1 (AffineMap (a,b)) -> open ; coherence R^1 (AffineMap (a,b)) is open proofend; end; begin definition let S be SubSpace of TOP-REAL 2; attrS is being_simple_closed_curve means :Def5: :: TOPREALB:def 5 the carrier of S is Simple_closed_curve; end; :: deftheorem Def5 defines being_simple_closed_curve TOPREALB:def_5_:_ for S being SubSpace of TOP-REAL 2 holds ( S is being_simple_closed_curve iff the carrier of S is Simple_closed_curve ); registration cluster being_simple_closed_curve -> non empty compact pathwise_connected for SubSpace of TOP-REAL 2; coherence for b1 being SubSpace of TOP-REAL 2 st b1 is being_simple_closed_curve holds ( not b1 is empty & b1 is pathwise_connected & b1 is compact ) proofend; end; registration let r be real positive number ; let x be Point of (TOP-REAL 2); cluster Sphere (x,r) -> being_simple_closed_curve ; coherence Sphere (x,r) is being_simple_closed_curve proofend; end; definition let n be Nat; let x be Point of (TOP-REAL n); let r be real number ; func Tcircle (x,r) -> SubSpace of TOP-REAL n equals :: TOPREALB:def 6 (TOP-REAL n) | (Sphere (x,r)); coherence (TOP-REAL n) | (Sphere (x,r)) is SubSpace of TOP-REAL n ; end; :: deftheorem defines Tcircle TOPREALB:def_6_:_ for n being Nat for x being Point of (TOP-REAL n) for r being real number holds Tcircle (x,r) = (TOP-REAL n) | (Sphere (x,r)); registration let n be non empty Nat; let x be Point of (TOP-REAL n); let r be real non negative number ; cluster Tcircle (x,r) -> non empty strict ; coherence ( Tcircle (x,r) is strict & not Tcircle (x,r) is empty ) ; end; theorem Th9: :: TOPREALB:9 for n being Element of NAT for r being real number for x being Point of (TOP-REAL n) holds the carrier of (Tcircle (x,r)) = Sphere (x,r) proofend; registration let n be Nat; let x be Point of (TOP-REAL n); let r be empty real number ; cluster Tcircle (x,r) -> trivial ; coherence Tcircle (x,r) is trivial proofend; end; theorem Th10: :: TOPREALB:10 for r being real number holds Tcircle ((0. (TOP-REAL 2)),r) is SubSpace of Trectangle ((- r),r,(- r),r) proofend; registration let x be Point of (TOP-REAL 2); let r be real positive number ; cluster Tcircle (x,r) -> being_simple_closed_curve ; coherence Tcircle (x,r) is being_simple_closed_curve proofend; end; registration cluster strict TopSpace-like V221() V222() being_simple_closed_curve for SubSpace of TOP-REAL 2; existence ex b1 being SubSpace of TOP-REAL 2 st ( b1 is being_simple_closed_curve & b1 is strict ) proofend; end; theorem :: TOPREALB:11 for S, T being being_simple_closed_curve SubSpace of TOP-REAL 2 holds S,T are_homeomorphic proofend; :: Unit circle definition let n be Nat; func Tunit_circle n -> SubSpace of TOP-REAL n equals :: TOPREALB:def 7 Tcircle ((0. (TOP-REAL n)),1); coherence Tcircle ((0. (TOP-REAL n)),1) is SubSpace of TOP-REAL n ; end; :: deftheorem defines Tunit_circle TOPREALB:def_7_:_ for n being Nat holds Tunit_circle n = Tcircle ((0. (TOP-REAL n)),1); set TUC = Tunit_circle 2; set cS1 = the carrier of (Tunit_circle 2); Lm13: the carrier of (Tunit_circle 2) = Sphere (|[0,0]|,1) by Th9, EUCLID:54; registration let n be non empty Nat; cluster Tunit_circle n -> non empty ; coherence not Tunit_circle n is empty ; end; theorem Th12: :: TOPREALB:12 for n being non empty Element of NAT for x being Point of (TOP-REAL n) st x is Point of (Tunit_circle n) holds |.x.| = 1 proofend; theorem Th13: :: TOPREALB:13 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 ) proofend; theorem Th14: :: TOPREALB:14 for x being Point of (TOP-REAL 2) st x is Point of (Tunit_circle 2) & x `1 = 1 holds x `2 = 0 proofend; theorem Th15: :: TOPREALB:15 for x being Point of (TOP-REAL 2) st x is Point of (Tunit_circle 2) & x `1 = - 1 holds x `2 = 0 proofend; theorem :: TOPREALB:16 for x being Point of (TOP-REAL 2) st x is Point of (Tunit_circle 2) & x `2 = 1 holds x `1 = 0 proofend; theorem :: TOPREALB:17 for x being Point of (TOP-REAL 2) st x is Point of (Tunit_circle 2) & x `2 = - 1 holds x `1 = 0 proofend; set TREC = Trectangle (p0,p1,p0,p1); theorem :: TOPREALB:18 Tunit_circle 2 is SubSpace of Trectangle ((- 1),1,(- 1),1) by Th10; theorem Th19: :: TOPREALB:19 for n being non empty Element of NAT for r being real positive number for x being Point of (TOP-REAL n) for f being Function of (Tunit_circle n),(Tcircle (x,r)) st ( for a being Point of (Tunit_circle n) for b being Point of (TOP-REAL n) st a = b holds f . a = (r * b) + x ) holds f is being_homeomorphism proofend; registration cluster Tunit_circle 2 -> being_simple_closed_curve ; coherence Tunit_circle 2 is being_simple_closed_curve ; end; Lm14: for n being non empty Element of NAT for r being real positive number for x being Point of (TOP-REAL n) holds Tunit_circle n, Tcircle (x,r) are_homeomorphic proofend; theorem :: TOPREALB:20 for n being non empty Element of NAT for r, s being real positive number for x, y being Point of (TOP-REAL n) holds Tcircle (x,r), Tcircle (y,s) are_homeomorphic proofend; registration let x be Point of (TOP-REAL 2); let r be real non negative number ; cluster Tcircle (x,r) -> pathwise_connected ; coherence Tcircle (x,r) is pathwise_connected proofend; end; :: Open unit circle definition func c[10] -> Point of (Tunit_circle 2) equals :: TOPREALB:def 8 |[1,0]|; coherence |[1,0]| is Point of (Tunit_circle 2) proofend; func c[-10] -> Point of (Tunit_circle 2) equals :: TOPREALB:def 9 |[(- 1),0]|; coherence |[(- 1),0]| is Point of (Tunit_circle 2) proofend; end; :: deftheorem defines c[10] TOPREALB:def_8_:_ c[10] = |[1,0]|; :: deftheorem defines c[-10] TOPREALB:def_9_:_ c[-10] = |[(- 1),0]|; 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: :: TOPREALB:def 10 the carrier of it = the carrier of (Tunit_circle 2) \ {p}; existence ex b1 being strict SubSpace of Tunit_circle 2 st the carrier of b1 = the carrier of (Tunit_circle 2) \ {p} proofend; uniqueness for b1, b2 being strict SubSpace of Tunit_circle 2 st the carrier of b1 = the carrier of (Tunit_circle 2) \ {p} & the carrier of b2 = the carrier of (Tunit_circle 2) \ {p} holds b1 = b2 by TSEP_1:5; end; :: deftheorem Def10 defines Topen_unit_circle TOPREALB:def_10_:_ for p being Point of (Tunit_circle 2) for b2 being strict SubSpace of Tunit_circle 2 holds ( b2 = Topen_unit_circle p iff the carrier of b2 = the carrier of (Tunit_circle 2) \ {p} ); registration let p be Point of (Tunit_circle 2); cluster Topen_unit_circle p -> non empty strict ; coherence not Topen_unit_circle p is empty proofend; end; theorem Th21: :: TOPREALB:21 for p being Point of (Tunit_circle 2) holds p is not Point of (Topen_unit_circle p) proofend; theorem Th22: :: TOPREALB:22 for p being Point of (Tunit_circle 2) holds Topen_unit_circle p = (Tunit_circle 2) | (([#] (Tunit_circle 2)) \ {p}) proofend; theorem Th23: :: TOPREALB:23 for p, q being Point of (Tunit_circle 2) st p <> q holds q is Point of (Topen_unit_circle p) proofend; theorem Th24: :: TOPREALB:24 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] proofend; theorem Th25: :: TOPREALB:25 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] proofend; set TOUC = Topen_unit_circle c[10]; set TOUCm = Topen_unit_circle c[-10]; set X = the carrier of (Topen_unit_circle c[10]); set Xm = the carrier of (Topen_unit_circle c[-10]); 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: the carrier of (Topen_unit_circle c[10]) = [#] (Topen_unit_circle c[10]) ; Lm17: the carrier of (Topen_unit_circle c[-10]) = [#] (Topen_unit_circle c[-10]) ; theorem Th26: :: TOPREALB:26 for p being Point of (Tunit_circle 2) for 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 ) proofend; theorem Th27: :: TOPREALB:27 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 ) proofend; theorem Th28: :: TOPREALB:28 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 ) proofend; registration let p be Point of (Tunit_circle 2); cluster Topen_unit_circle p -> strict open ; coherence Topen_unit_circle p is open proofend; end; theorem :: TOPREALB:29 for p being Point of (Tunit_circle 2) holds Topen_unit_circle p, I(01) are_homeomorphic proofend; theorem :: TOPREALB:30 for p, q being Point of (Tunit_circle 2) holds Topen_unit_circle p, Topen_unit_circle q are_homeomorphic proofend; begin definition func CircleMap -> Function of R^1,(Tunit_circle 2) means :Def11: :: TOPREALB:def 11 for x being real number holds it . x = |[(cos ((2 * PI) * x)),(sin ((2 * PI) * x))]|; existence ex b1 being Function of R^1,(Tunit_circle 2) st for x being real number holds b1 . x = |[(cos ((2 * PI) * x)),(sin ((2 * PI) * x))]| proofend; uniqueness for b1, b2 being Function of R^1,(Tunit_circle 2) st ( for x being real number holds b1 . x = |[(cos ((2 * PI) * x)),(sin ((2 * PI) * x))]| ) & ( for x being real number holds b2 . x = |[(cos ((2 * PI) * x)),(sin ((2 * PI) * x))]| ) holds b1 = b2 proofend; end; :: deftheorem Def11 defines CircleMap TOPREALB:def_11_:_ for b1 being Function of R^1,(Tunit_circle 2) holds ( b1 = CircleMap iff for x being real number holds b1 . x = |[(cos ((2 * PI) * x)),(sin ((2 * PI) * x))]| ); Lm18: dom CircleMap = REAL by FUNCT_2:def_1, TOPMETR:17; theorem Th31: :: TOPREALB:31 for i being Integer for r being real number holds CircleMap . r = CircleMap . (r + i) proofend; theorem Th32: :: TOPREALB:32 for i being Integer holds CircleMap . i = c[10] proofend; theorem Th33: :: TOPREALB:33 CircleMap " {c[10]} = INT proofend; Lm19: CircleMap . (1 / 2) = |[(- 1),0]| proofend; theorem Th34: :: TOPREALB:34 for r being real number st frac r = 1 / 2 holds CircleMap . r = |[(- 1),0]| proofend; theorem :: TOPREALB:35 for r being real number st frac r = 1 / 4 holds CircleMap . r = |[0,1]| proofend; theorem :: TOPREALB:36 for r being real number st frac r = 3 / 4 holds CircleMap . r = |[0,(- 1)]| proofend; Lm20: for r being real number holds CircleMap . r = |[((cos * (AffineMap ((2 * PI),0))) . r),((sin * (AffineMap ((2 * PI),0))) . r)]| proofend; theorem :: TOPREALB:37 for r being real number for i, j being Integer holds CircleMap . r = |[((cos * (AffineMap ((2 * PI),((2 * PI) * i)))) . r),((sin * (AffineMap ((2 * PI),((2 * PI) * j)))) . r)]| proofend; registration cluster CircleMap -> continuous ; coherence CircleMap is continuous proofend; end; Lm21: for A being Subset of R^1 holds CircleMap | A is Function of (R^1 | A),(Tunit_circle 2) proofend; Lm22: for r being real number st - 1 <= r & r <= 1 holds ( 0 <= (arccos r) / (2 * PI) & (arccos r) / (2 * PI) <= 1 / 2 ) proofend; theorem Th38: :: TOPREALB:38 for A being Subset of R^1 for f being Function of (R^1 | A),(Tunit_circle 2) st [.0,1.[ c= A & f = CircleMap | A holds f is onto proofend; registration cluster CircleMap -> onto ; coherence CircleMap is onto proofend; end; Lm23: CircleMap | [.0,1.[ is one-to-one proofend; registration let r be real number ; clusterK69(CircleMap,[.r,(r + 1).[) -> one-to-one ; coherence CircleMap | [.r,(r + 1).[ is one-to-one proofend; end; registration let r be real number ; clusterK69(CircleMap,].r,(r + 1).[) -> one-to-one ; coherence CircleMap | ].r,(r + 1).[ is one-to-one proofend; end; theorem Th39: :: TOPREALB:39 for b, a being real number st b - a <= 1 holds for d being set st d in IntIntervals (a,b) holds CircleMap | d is one-to-one proofend; theorem Th40: :: TOPREALB:40 for a, b being real number for d being set st d in IntIntervals (a,b) holds CircleMap .: d = CircleMap .: (union (IntIntervals (a,b))) proofend; 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 :: TOPREALB:def 12 CircleMap | ].r,(r + 1).[; coherence CircleMap | ].r,(r + 1).[ is Function of (R^1 | (R^1 ].r,(r + 1).[)),(Topen_unit_circle (CircleMap . r)) proofend; end; :: deftheorem defines CircleMap TOPREALB:def_12_:_ for r being Point of R^1 holds CircleMap r = CircleMap | ].r,(r + 1).[; Lm24: for a, r being real number holds rng ((AffineMap (1,(- a))) | ].(r + a),((r + a) + 1).[) = ].r,(r + 1).[ proofend; theorem Th41: :: TOPREALB:41 for i being Integer for a being real number holds CircleMap (R^1 (a + i)) = (CircleMap (R^1 a)) * ((AffineMap (1,(- i))) | ].(a + i),((a + i) + 1).[) proofend; registration let r be Point of R^1; cluster CircleMap r -> one-to-one onto continuous ; coherence ( CircleMap r is one-to-one & CircleMap r is onto & CircleMap r is continuous ) proofend; end; definition func Circle2IntervalR -> Function of (Topen_unit_circle c[10]),(R^1 | (R^1 ].0,1.[)) means :Def13: :: TOPREALB:def 13 for p being Point of (Topen_unit_circle c[10]) ex x, y being real number st ( p = |[x,y]| & ( y >= 0 implies it . p = (arccos x) / (2 * PI) ) & ( y <= 0 implies it . p = 1 - ((arccos x) / (2 * PI)) ) ); existence ex b1 being Function of (Topen_unit_circle c[10]),(R^1 | (R^1 ].0,1.[)) st for p being Point of (Topen_unit_circle c[10]) ex x, y being real number st ( p = |[x,y]| & ( y >= 0 implies b1 . p = (arccos x) / (2 * PI) ) & ( y <= 0 implies b1 . p = 1 - ((arccos x) / (2 * PI)) ) ) proofend; uniqueness for b1, b2 being Function of (Topen_unit_circle c[10]),(R^1 | (R^1 ].0,1.[)) st ( for p being Point of (Topen_unit_circle c[10]) ex x, y being real number st ( p = |[x,y]| & ( y >= 0 implies b1 . p = (arccos x) / (2 * PI) ) & ( y <= 0 implies b1 . p = 1 - ((arccos x) / (2 * PI)) ) ) ) & ( for p being Point of (Topen_unit_circle c[10]) ex x, y being real number st ( p = |[x,y]| & ( y >= 0 implies b2 . p = (arccos x) / (2 * PI) ) & ( y <= 0 implies b2 . p = 1 - ((arccos x) / (2 * PI)) ) ) ) holds b1 = b2 proofend; end; :: deftheorem Def13 defines Circle2IntervalR TOPREALB:def_13_:_ for b1 being Function of (Topen_unit_circle c[10]),(R^1 | (R^1 ].0,1.[)) holds ( b1 = Circle2IntervalR iff for p being Point of (Topen_unit_circle c[10]) ex x, y being real number st ( p = |[x,y]| & ( y >= 0 implies b1 . p = (arccos x) / (2 * PI) ) & ( y <= 0 implies b1 . p = 1 - ((arccos x) / (2 * PI)) ) ) ); 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: :: TOPREALB:def 14 for p being Point of (Topen_unit_circle c[-10]) ex x, y being real number 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 ex b1 being Function of (Topen_unit_circle c[-10]),(R^1 | (R^1 ].(1 / 2),(3 / 2).[)) st for p being Point of (Topen_unit_circle c[-10]) ex x, y being real number st ( p = |[x,y]| & ( y >= 0 implies b1 . p = 1 + ((arccos x) / (2 * PI)) ) & ( y <= 0 implies b1 . p = 1 - ((arccos x) / (2 * PI)) ) ) proofend; uniqueness for b1, b2 being Function of (Topen_unit_circle c[-10]),(R^1 | (R^1 ].(1 / 2),(3 / 2).[)) st ( for p being Point of (Topen_unit_circle c[-10]) ex x, y being real number st ( p = |[x,y]| & ( y >= 0 implies b1 . p = 1 + ((arccos x) / (2 * PI)) ) & ( y <= 0 implies b1 . p = 1 - ((arccos x) / (2 * PI)) ) ) ) & ( for p being Point of (Topen_unit_circle c[-10]) ex x, y being real number st ( p = |[x,y]| & ( y >= 0 implies b2 . p = 1 + ((arccos x) / (2 * PI)) ) & ( y <= 0 implies b2 . p = 1 - ((arccos x) / (2 * PI)) ) ) ) holds b1 = b2 proofend; end; :: deftheorem Def14 defines Circle2IntervalL TOPREALB:def_14_:_ for b1 being Function of (Topen_unit_circle c[-10]),(R^1 | (R^1 ].(1 / 2),(3 / 2).[)) holds ( b1 = Circle2IntervalL iff for p being Point of (Topen_unit_circle c[-10]) ex x, y being real number st ( p = |[x,y]| & ( y >= 0 implies b1 . p = 1 + ((arccos x) / (2 * PI)) ) & ( y <= 0 implies b1 . p = 1 - ((arccos x) / (2 * PI)) ) ) ); set C = Circle2IntervalR ; set Cm = Circle2IntervalL ; theorem Th42: :: TOPREALB:42 (CircleMap (R^1 0)) " = Circle2IntervalR proofend; theorem Th43: :: TOPREALB:43 (CircleMap (R^1 (1 / 2))) " = Circle2IntervalL proofend; set A = ].0,1.[; set Q = [.(- 1),1.[; set E = ].0,PI.]; set j = 1 / (2 * PI); reconsider Q = [.(- 1),1.[, E = ].0,PI.] 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 ].0,1.[)) = R^1 ].0,1.[ by PRE_TOPC:8; set Af = (AffineMap ((1 / (2 * PI)),0)) | (R^1 E); dom (AffineMap ((1 / (2 * PI)),0)) = the carrier of R^1 by FUNCT_2:def_1, TOPMETR:17; then Lm28: dom ((AffineMap ((1 / (2 * PI)),0)) | (R^1 E)) = R^1 E by RELAT_1:62; rng ((AffineMap ((1 / (2 * PI)),0)) | (R^1 E)) c= ].0,1.[ proofend; then reconsider Af = (AffineMap ((1 / (2 * PI)),0)) | (R^1 E) as Function of (R^1 | (R^1 E)),(R^1 | (R^1 ].0,1.[)) by Lm26, Lm27, Lm28, FUNCT_2:2; Lm29: R^1 (AffineMap ((1 / (2 * PI)),0)) = AffineMap ((1 / (2 * PI)),0) ; Lm30: dom (AffineMap ((1 / (2 * PI)),0)) = REAL by FUNCT_2:def_1; Lm31: rng (AffineMap ((1 / (2 * PI)),0)) = REAL by FCONT_1:55; R^1 | ([#] R^1) = R^1 by TSEP_1:3; then reconsider Af = Af as continuous Function of (R^1 | (R^1 E)),(R^1 | (R^1 ].0,1.[)) by Lm29, Lm30, Lm31, TOPMETR:17, TOPREALA:8; set L = (R^1 (AffineMap ((- 1),1))) | (R^1 ].0,1.[); Lm32: dom (AffineMap ((- 1),1)) = REAL by FUNCT_2:def_1; then Lm33: dom ((R^1 (AffineMap ((- 1),1))) | (R^1 ].0,1.[)) = ].0,1.[ by RELAT_1:62; rng ((R^1 (AffineMap ((- 1),1))) | (R^1 ].0,1.[)) c= ].0,1.[ proofend; then reconsider L = (R^1 (AffineMap ((- 1),1))) | (R^1 ].0,1.[) as Function of (R^1 | (R^1 ].0,1.[)),(R^1 | (R^1 ].0,1.[)) 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 = L as continuous Function of (R^1 | (R^1 ].0,1.[)),(R^1 | (R^1 ].0,1.[)) 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, SIN_COS6:86; set c = ac | (R^1 Q); Lm36: dom (ac | (R^1 Q)) = Q by RELAT_1:62, SIN_COS6:86, XXREAL_1:35; Lm37: rng (ac | (R^1 Q)) c= E proofend; then reconsider c = ac | (R^1 Q) 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 (Topen_unit_circle c[10]) st aX1 = { q where q is Point of (TOP-REAL 2) : ( q in the carrier of (Topen_unit_circle c[10]) & 0 <= q `2 ) } holds Circle2IntervalR | ((Topen_unit_circle c[10]) | aX1) is continuous proofend; Lm43: for aX1 being Subset of (Topen_unit_circle c[10]) st aX1 = { q where q is Point of (TOP-REAL 2) : ( q in the carrier of (Topen_unit_circle c[10]) & 0 >= q `2 ) } holds Circle2IntervalR | ((Topen_unit_circle c[10]) | aX1) is continuous proofend; Lm44: for p being Point of (Topen_unit_circle c[10]) st p = c[-10] holds Circle2IntervalR is_continuous_at p proofend; set h1 = REAL --> 1; reconsider h1 = REAL --> 1 as PartFunc of REAL,REAL ; Lm45: Circle2IntervalR is continuous proofend; set A = ].(1 / 2),((1 / 2) + p1).[; set Q = ].(- 1),1.]; set E = [.0,PI.[; reconsider Q = ].(- 1),1.], E = [.0,PI.[ 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 ].(1 / 2),((1 / 2) + p1).[)) = R^1 ].(1 / 2),((1 / 2) + p1).[ by PRE_TOPC:8; set Af = (AffineMap ((- (1 / (2 * PI))),1)) | (R^1 E); dom (AffineMap ((- (1 / (2 * PI))),1)) = the carrier of R^1 by FUNCT_2:def_1, TOPMETR:17; then Lm49: dom ((AffineMap ((- (1 / (2 * PI))),1)) | (R^1 E)) = R^1 E by RELAT_1:62; rng ((AffineMap ((- (1 / (2 * PI))),1)) | (R^1 E)) c= ].(1 / 2),((1 / 2) + p1).[ proofend; then reconsider Af = (AffineMap ((- (1 / (2 * PI))),1)) | (R^1 E) as Function of (R^1 | (R^1 E)),(R^1 | (R^1 ].(1 / 2),((1 / 2) + p1).[)) by Lm47, Lm48, Lm49, FUNCT_2:2; Lm50: R^1 (AffineMap ((- (1 / (2 * PI))),1)) = AffineMap ((- (1 / (2 * PI))),1) ; Lm51: dom (AffineMap ((- (1 / (2 * PI))),1)) = REAL by FUNCT_2:def_1; rng (AffineMap ((- (1 / (2 * PI))),1)) = REAL by FCONT_1:55; then reconsider Af = Af as continuous Function of (R^1 | (R^1 E)),(R^1 | (R^1 ].(1 / 2),((1 / 2) + p1).[)) by Lm35, Lm50, Lm51, TOPMETR:17, TOPREALA:8; set Af1 = (AffineMap ((1 / (2 * PI)),1)) | (R^1 E); dom (AffineMap ((1 / (2 * PI)),1)) = the carrier of R^1 by FUNCT_2:def_1, TOPMETR:17; then Lm52: dom ((AffineMap ((1 / (2 * PI)),1)) | (R^1 E)) = R^1 E by RELAT_1:62; rng ((AffineMap ((1 / (2 * PI)),1)) | (R^1 E)) c= ].(1 / 2),((1 / 2) + p1).[ proofend; then reconsider Af1 = (AffineMap ((1 / (2 * PI)),1)) | (R^1 E) as Function of (R^1 | (R^1 E)),(R^1 | (R^1 ].(1 / 2),((1 / 2) + p1).[)) by Lm47, Lm48, Lm52, FUNCT_2:2; Lm53: R^1 (AffineMap ((1 / (2 * PI)),1)) = AffineMap ((1 / (2 * PI)),1) ; Lm54: dom (AffineMap ((1 / (2 * PI)),1)) = REAL by FUNCT_2:def_1; rng (AffineMap ((1 / (2 * PI)),1)) = REAL by FCONT_1:55; then reconsider Af1 = Af1 as continuous Function of (R^1 | (R^1 E)),(R^1 | (R^1 ].(1 / 2),((1 / 2) + p1).[)) by Lm35, Lm53, Lm54, TOPMETR:17, TOPREALA:8; set c = ac | (R^1 Q); Lm55: dom (ac | (R^1 Q)) = Q by RELAT_1:62, SIN_COS6:86, XXREAL_1:36; Lm56: rng (ac | (R^1 Q)) c= E proofend; then reconsider c = ac | (R^1 Q) 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 (Topen_unit_circle c[-10]) st aX1 = { q where q is Point of (TOP-REAL 2) : ( q in the carrier of (Topen_unit_circle c[-10]) & 0 <= q `2 ) } holds Circle2IntervalL | ((Topen_unit_circle c[-10]) | aX1) is continuous proofend; Lm60: for aX1 being Subset of (Topen_unit_circle c[-10]) st aX1 = { q where q is Point of (TOP-REAL 2) : ( q in the carrier of (Topen_unit_circle c[-10]) & 0 >= q `2 ) } holds Circle2IntervalL | ((Topen_unit_circle c[-10]) | aX1) is continuous proofend; Lm61: for p being Point of (Topen_unit_circle c[-10]) st p = c[10] holds Circle2IntervalL is_continuous_at p proofend; Lm62: Circle2IntervalL is continuous proofend; registration cluster Circle2IntervalR -> one-to-one onto continuous ; coherence ( Circle2IntervalR is one-to-one & Circle2IntervalR is onto & Circle2IntervalR is continuous ) by Lm45, Th42, GRCAT_1:41; cluster Circle2IntervalL -> one-to-one onto continuous ; coherence ( Circle2IntervalL is one-to-one & Circle2IntervalL is onto & Circle2IntervalL is continuous ) by Lm62, Th43, GRCAT_1:41; end; Lm63: CircleMap (R^1 0) is open proofend; 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 CircleMap (R^1 i) is open proofend; cluster CircleMap (R^1 ((1 / 2) + i)) -> open ; coherence CircleMap (R^1 ((1 / 2) + i)) is open proofend; end; registration cluster Circle2IntervalR -> open ; coherence Circle2IntervalR is open proofend; cluster Circle2IntervalL -> open ; coherence Circle2IntervalL is open by Lm19, Th43, TOPREALA:13; end; theorem :: TOPREALB:44 CircleMap (R^1 (1 / 2)) is being_homeomorphism proofend; theorem :: TOPREALB:45 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) holds 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)) holds for f being Function of (R^1 | d),((Tunit_circle 2) | U) st f = CircleMap | d holds f is being_homeomorphism ) ) ) ) ) ) proofend;