:: Some Properties of Circles on the Plane :: by Artur Korni{\l}owicz and Yasunari Shidama :: :: Received October 18, 2004 :: Copyright (c) 2004-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, RELAT_1, SIN_COS, EUCLID, CARD_1, STRUCT_0, TOPMETR, ARYTM_1, XXREAL_0, XXREAL_1, ARYTM_3, SUBSET_1, INT_1, PRE_TOPC, XBOOLE_0, ORDINAL2, SIN_COS6, JGRAPH_2, FUNCT_1, REAL_1, XCMPLX_0, FUNCT_2, TAXONOM2, SETFAM_1, TARSKI, ZFMISC_1, RCOMP_1, PARTFUN1, TMAP_1, CONNSP_2, FCONT_1, TOPS_1, TOPS_2, TOPREAL2, BORSUK_2, METRIC_1, MCART_1, JGRAPH_6, COMPLEX1, NAT_1, SUPINF_2, TOPREALA, T_0TOPSP, TOPREAL1, FINSEQ_1, SQUARE_1, FUNCOP_1, BORSUK_4, CARD_3, VALUED_1, TOPREALB, FUNCT_7; notations TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, ORDINAL1, FUNCT_1, RELSET_1, PARTFUN1, VALUED_1, NUMBERS, XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, SQUARE_1, INT_1, CARD_3, FINSEQ_1, FUNCT_4, RCOMP_1, FCONT_1, DOMAIN_1, FUNCT_2, FUNCOP_1, STRUCT_0, PRE_TOPC, TOPS_1, BORSUK_1, TSEP_1, TOPS_2, COMPTS_1, CONNSP_2, T_0TOPSP, TMAP_1, TOPREAL1, TOPREAL2, METRIC_1, TOPMETR, RLVECT_1, EUCLID, BORSUK_2, SIN_COS, JGRAPH_6, BORSUK_3, TAXONOM2, BORSUK_4, TOPREAL9, TOPALG_2, SIN_COS6, PSCOMP_1, TOPREALA, XXREAL_0; constructors REAL_1, SQUARE_1, CARD_3, RCOMP_1, FCONT_1, COMSEQ_3, SIN_COS, SIN_COS6, TOPS_1, TOPS_2, COMPTS_1, GRCAT_1, TMAP_1, MONOID_0, TOPREAL1, TOPREAL2, PSCOMP_1, TAXONOM2, BORSUK_2, BORSUK_3, BORSUK_4, JGRAPH_6, TOPALG_2, TOPREAL9, TOPREALA, XXREAL_2, FUNCOP_1, BINOP_2, FUNCT_4, NUMBERS; registrations SUBSET_1, FUNCT_1, RELSET_1, FUNCT_2, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, NAT_1, INT_1, MEMBERED, RCOMP_1, SIN_COS6, STRUCT_0, PRE_TOPC, TOPS_1, BORSUK_1, MONOID_0, EUCLID, TOPMETR, TOPREAL1, TOPREAL2, PSCOMP_1, TOPGRP_1, BORSUK_3, FCONT_1, TOPALG_3, TOPREAL9, TOPREALA, VALUED_0, SIN_COS, FUNCOP_1, MEASURE6, ORDINAL1, SQUARE_1, CARD_1; requirements NUMERALS, BOOLE, SUBSET, ARITHM, REAL; begin 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; cluster [.-1,1.] -> non empty; cluster ].1/2,3/2.[ -> non empty; end; registration cluster sin -> continuous; cluster cos -> continuous; cluster arcsin -> continuous; cluster arccos -> continuous; end; theorem :: TOPREALB:1 sin(a*r+b) = (sin*AffineMap(a,b)).r; theorem :: TOPREALB:2 cos(a*r+b) = (cos*AffineMap(a,b)).r; registration let a be non zero Real, b be Real; cluster AffineMap(a,b) -> onto one-to-one; end; definition let a, b be Real; func IntIntervals(a,b) -> set equals :: TOPREALB:def 1 the set of all ]. a+n, b+n .[ where n is Element of INT; end; theorem :: TOPREALB:3 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; end; theorem :: TOPREALB:4 b-a <= 1 implies IntIntervals(a,b) is mutually-disjoint; definition let a, b be Real; redefine func IntIntervals(a,b) -> Subset-Family of R^1; end; definition let a, b be Real; redefine func IntIntervals(a,b) -> open Subset-Family of R^1; end; begin :: Correspondence between REAL and R^1 definition let r be Real; func R^1(r) -> Point of R^1 equals :: TOPREALB:def 2 r; end; definition let A be Subset of REAL; func R^1(A) -> Subset of R^1 equals :: TOPREALB:def 3 A; end; registration let A be non empty Subset of REAL; cluster R^1(A) -> non empty; end; registration let A be open Subset of REAL; cluster R^1(A) -> open; end; registration let A be closed Subset of REAL; cluster R^1(A) -> closed; end; registration let A be open Subset of REAL; cluster R^1 | R^1(A) -> open; end; registration let A be closed Subset of REAL; cluster R^1 | R^1(A) -> closed; 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; end; registration let f be PartFunc of REAL,REAL; cluster R^1(f) -> onto; end; registration let f be one-to-one PartFunc of REAL,REAL; cluster R^1(f) -> one-to-one; end; theorem :: TOPREALB:5 R^1 | (R^1 [#]REAL) = R^1; theorem :: TOPREALB:6 for f being PartFunc of REAL,REAL st dom f = REAL holds R^1|(R^1 dom f) = R^1 ; theorem :: TOPREALB:7 for f being Function of REAL,REAL holds f is Function of R^1, R^1 | R^1(rng f); theorem :: TOPREALB:8 for f being Function of REAL,REAL holds f is Function of R^1, R^1; registration let f be continuous PartFunc of REAL,REAL; cluster R^1(f) -> continuous; end; registration let a be non zero Real, b be Real; cluster R^1(AffineMap(a,b)) -> open; end; begin :: Circles definition let S be SubSpace of TOP-REAL 2; attr S is being_simple_closed_curve means :: TOPREALB:def 5 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; end; registration let r be positive Real, x be Point of TOP-REAL 2; cluster Sphere(x,r) -> being_simple_closed_curve; 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 :: TOPREALB:def 6 (TOP-REAL n) | Sphere(x,r); 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; end; theorem :: TOPREALB:9 the carrier of Tcircle(x,r) = Sphere(x,r); registration let n be Nat, x be Point of TOP-REAL n, r be zero Real; cluster Tcircle(x,r) -> trivial; end; theorem :: TOPREALB:10 Tcircle(0.TOP-REAL 2,r) is SubSpace of Trectangle(-r,r,-r,r); registration let x be Point of TOP-REAL 2, r be positive Real; cluster Tcircle(x,r) -> being_simple_closed_curve; end; registration cluster being_simple_closed_curve strict for SubSpace of TOP-REAL 2; end; theorem :: TOPREALB:11 for S, T being being_simple_closed_curve SubSpace of TOP-REAL 2 holds S,T are_homeomorphic; :: 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); end; registration let n be non zero Nat; cluster Tunit_circle(n) -> non empty; end; theorem :: TOPREALB:12 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; theorem :: 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; theorem :: 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; theorem :: 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; 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; 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; theorem :: TOPREALB:18 Tunit_circle(2) is SubSpace of Trectangle(-1,1,-1,1); theorem :: TOPREALB:19 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; registration cluster Tunit_circle(2) -> being_simple_closed_curve; end; theorem :: TOPREALB:20 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; registration let x be Point of TOP-REAL 2, r be non negative Real; cluster Tcircle(x,r) -> pathwise_connected; end; :: Open unit circle definition func c[10] -> Point of Tunit_circle(2) equals :: TOPREALB:def 8 |[1,0]|; func c[-10] -> Point of Tunit_circle(2) equals :: TOPREALB:def 9 |[-1,0]|; end; definition let p be Point of Tunit_circle(2); func Topen_unit_circle(p) -> strict SubSpace of Tunit_circle(2) means :: TOPREALB:def 10 the carrier of it = (the carrier of Tunit_circle(2)) \ {p}; end; registration let p be Point of Tunit_circle(2); cluster Topen_unit_circle(p) -> non empty; end; theorem :: TOPREALB:21 for p being Point of Tunit_circle(2) holds p is not Point of Topen_unit_circle(p); theorem :: TOPREALB:22 for p being Point of Tunit_circle(2) holds Topen_unit_circle(p) = (Tunit_circle(2)) | (([#]Tunit_circle(2)) \ {p}); theorem :: TOPREALB:23 for p, q being Point of Tunit_circle(2) st p <> q holds q is Point of Topen_unit_circle(p); theorem :: 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]; theorem :: 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]; theorem :: TOPREALB:26 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; theorem :: 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; theorem :: 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; registration let p be Point of Tunit_circle(2); cluster Topen_unit_circle(p) -> open; end; theorem :: TOPREALB:29 for p being Point of Tunit_circle(2) holds Topen_unit_circle(p), I(01) are_homeomorphic; theorem :: TOPREALB:30 for p, q being Point of Tunit_circle(2) holds Topen_unit_circle(p), Topen_unit_circle(q) are_homeomorphic; begin :: Correspondence between the real line and circles definition func CircleMap -> Function of R^1, Tunit_circle(2) means :: TOPREALB:def 11 for x being Real holds it.x = |[ cos(2*PI*x), sin(2*PI*x) ]|; end; theorem :: TOPREALB:31 CircleMap.r = CircleMap.(r+i); theorem :: TOPREALB:32 CircleMap.i = c[10]; theorem :: TOPREALB:33 CircleMap"{c[10]} = INT; theorem :: TOPREALB:34 frac r = 1/2 implies CircleMap.r = |[-1,0]|; theorem :: TOPREALB:35 frac r = 1/4 implies CircleMap.r = |[0,1]|; theorem :: TOPREALB:36 frac r = 3/4 implies CircleMap.r = |[0,-1]|; theorem :: TOPREALB:37 for i, j being Integer holds CircleMap.r = |[ (cos*AffineMap(2*PI,2*PI *i)).r, (sin*AffineMap(2*PI,2*PI*j)).r ]|; registration cluster CircleMap -> continuous; end; theorem :: TOPREALB:38 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; registration cluster CircleMap -> onto; end; registration let r be Real; cluster CircleMap | [.r,r+1.[ -> one-to-one; end; registration let r be Real; cluster CircleMap | ].r,r+1.[ -> one-to-one; end; theorem :: TOPREALB:39 b-a <= 1 implies for d being set st d in IntIntervals(a,b) holds CircleMap|d is one-to-one; theorem :: TOPREALB:40 for d being set st d in IntIntervals(a,b) holds CircleMap.:d = CircleMap.:union IntIntervals(a,b); 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.[; end; theorem :: TOPREALB:41 CircleMap(R^1(a+i)) = CircleMap(R^1(a)) * (AffineMap(1,-i) | ].a +i,a+i+1.[); registration let r be Point of R^1; cluster CircleMap(r) -> one-to-one onto continuous; end; definition func Circle2IntervalR -> Function of Topen_unit_circle(c[10]), R^1 | R^1(].0 ,1.[) means :: TOPREALB:def 13 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)); end; definition func Circle2IntervalL -> Function of Topen_unit_circle(c[-10]), R^1 | R^1(]. 1/2,3/2.[) means :: TOPREALB:def 14 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)); end; theorem :: TOPREALB:42 (CircleMap(R^1(0)))" = Circle2IntervalR; theorem :: TOPREALB:43 (CircleMap(R^1(1/2)))" = Circle2IntervalL; registration cluster Circle2IntervalR -> one-to-one onto continuous; cluster Circle2IntervalL -> one-to-one onto continuous; end; registration let i be Integer; cluster CircleMap(R^1(i)) -> open; cluster CircleMap(R^1(1/2+i)) -> open; end; registration cluster Circle2IntervalR -> open; cluster Circle2IntervalL -> open; end; theorem :: TOPREALB:44 CircleMap(R^1(1/2)) is being_homeomorphism; 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) 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 );