:: On the Simple Closed Curve Property of the Circle and the :: Fashoda Meet Theorem for It :: by Yatsuka Nakamura :: :: Received August 20, 2001 :: Copyright (c) 2001-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, SQUARE_1, ARYTM_3, XXREAL_0, CARD_1, RELAT_1, STRUCT_0, EUCLID, PRE_TOPC, COMPLEX1, MCART_1, FUNCT_1, XBOOLE_0, TARSKI, SUBSET_1, ORDINAL2, RCOMP_1, SUPINF_2, ARYTM_1, TOPMETR, REAL_1, XXREAL_1, JORDAN2C, FUNCT_4, PARTFUN1, PCOMPS_1, METRIC_1, TOPS_2, TOPREAL2, TOPREAL1, VALUED_1, BORSUK_1, JGRAPH_3, FUNCT_2; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, RLVECT_1, EUCLID, RELAT_1, TOPS_2, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, DOMAIN_1, STRUCT_0, TOPREAL1, TOPMETR, COMPTS_1, METRIC_1, RCOMP_1, SQUARE_1, PCOMPS_1, PSCOMP_1, PRE_TOPC, FUNCT_4, TOPREAL2, XXREAL_0; constructors FUNCT_4, REAL_1, SQUARE_1, RCOMP_1, TOPS_2, COMPTS_1, TOPMETR, TOPREAL1, TOPREAL2, PSCOMP_1, FUNCSDOM, PCOMPS_1; registrations FUNCT_1, RELSET_1, FUNCT_2, NUMBERS, XXREAL_0, XREAL_0, SQUARE_1, MEMBERED, STRUCT_0, PRE_TOPC, BORSUK_1, EUCLID, TOPMETR, TOPREAL1, TOPREAL2, BORSUK_3, ORDINAL1; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; begin :: Preliminaries reserve x for Real; theorem :: JGRAPH_3:1 for p being Point of TOP-REAL 2 holds |.p.| = sqrt((p`1)^2+(p`2)^2) & |.p.|^2 = (p`1)^2+(p`2)^2; theorem :: JGRAPH_3:2 for f being Function,B,C being set holds (f|B).:C = f.:(C /\ B); theorem :: JGRAPH_3:3 for X,Y being non empty TopSpace, p0 being Point of X, D being non empty Subset of X, E being non empty Subset of Y, f being Function of X,Y st D`={p0} & E`={f.p0} & X is T_2 & Y is T_2 & (for p being Point of X|D holds f.p<>f.p0)& f|D is continuous Function of X|D,Y|E & (for V being Subset of Y st f.p0 in V & V is open ex W being Subset of X st p0 in W & W is open & f.:W c= V ) holds f is continuous; begin :: The Circle is a Simple Closed Curve reserve p,q for Point of TOP-REAL 2; definition func Sq_Circ -> Function of the carrier of TOP-REAL 2, the carrier of TOP-REAL 2 means :: JGRAPH_3:def 1 for p being Point of TOP-REAL 2 holds (p=0.TOP-REAL 2 implies it.p=p) & ((p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1)& p<>0. TOP-REAL 2 implies it.p=|[p`1/sqrt(1+(p`2/p`1)^2),p`2/sqrt(1+(p`2/p`1)^2)]|)& ( not(p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1)& p<>0.TOP-REAL 2 implies it.p =|[p`1/sqrt(1+(p`1/p`2)^2),p`2/sqrt(1+(p`1/p`2)^2)]|); end; theorem :: JGRAPH_3:4 for p being Point of TOP-REAL 2 st p<>0.TOP-REAL 2 holds ((p`1<= p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p`2)implies Sq_Circ.p=|[p`1/sqrt(1+(p`1/p`2 )^2),p`2/sqrt(1+(p`1/p`2)^2)]|) & (not(p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<= -p`2) implies Sq_Circ.p=|[p`1/sqrt(1+(p`2/p`1)^2),p`2/sqrt(1+(p`2/p`1)^2)]|); theorem :: JGRAPH_3:5 for X being non empty TopSpace, f1 being Function of X,R^1 st f1 is continuous & (for q being Point of X ex r being Real st f1.q=r & r>=0 ) holds ex g being Function of X,R^1 st (for p being Point of X,r1 being Real st f1.p=r1 holds g.p=sqrt(r1)) & g is continuous; theorem :: JGRAPH_3:6 for X being non empty TopSpace, f1,f2 being Function of X,R^1 st f1 is continuous & f2 is continuous & (for q being Point of X holds f2.q<>0) holds ex g being Function of X,R^1 st (for p being Point of X,r1,r2 being Real st f1.p=r1 & f2.p=r2 holds g.p=(r1/r2)^2) & g is continuous; theorem :: JGRAPH_3:7 for X being non empty TopSpace, f1,f2 being Function of X,R^1 st f1 is continuous & f2 is continuous & (for q being Point of X holds f2.q<>0) holds ex g being Function of X,R^1 st (for p being Point of X,r1,r2 being Real st f1.p=r1 & f2.p=r2 holds g.p=1+(r1/r2)^2) & g is continuous; theorem :: JGRAPH_3:8 for X being non empty TopSpace, f1,f2 being Function of X,R^1 st f1 is continuous & f2 is continuous & (for q being Point of X holds f2.q<>0) holds ex g being Function of X,R^1 st (for p being Point of X,r1,r2 being Real st f1.p=r1 & f2.p=r2 holds g.p=sqrt(1+(r1/r2)^2)) & g is continuous; theorem :: JGRAPH_3:9 for X being non empty TopSpace, f1,f2 being Function of X,R^1 st f1 is continuous & f2 is continuous & (for q being Point of X holds f2.q<>0) holds ex g being Function of X,R^1 st (for p being Point of X,r1,r2 being Real st f1.p=r1 & f2.p=r2 holds g.p=r1/sqrt(1+(r1/r2)^2)) & g is continuous; theorem :: JGRAPH_3:10 for X being non empty TopSpace, f1,f2 being Function of X,R^1 st f1 is continuous & f2 is continuous & (for q being Point of X holds f2.q<>0) holds ex g being Function of X,R^1 st (for p being Point of X,r1,r2 being Real st f1.p=r1 & f2.p=r2 holds g.p=r2/sqrt(1+(r1/r2)^2)) & g is continuous; theorem :: JGRAPH_3:11 for K1 being non empty Subset of TOP-REAL 2, f being Function of (TOP-REAL 2)|K1,R^1 st (for p being Point of TOP-REAL 2 st p in the carrier of (TOP-REAL 2)|K1 holds f.p=p`1/sqrt(1+(p`2/p`1)^2)) & (for q being Point of TOP-REAL 2 st q in the carrier of (TOP-REAL 2)|K1 holds q`1<>0 ) holds f is continuous; theorem :: JGRAPH_3:12 for K1 being non empty Subset of TOP-REAL 2, f being Function of (TOP-REAL 2)|K1,R^1 st (for p being Point of TOP-REAL 2 st p in the carrier of (TOP-REAL 2)|K1 holds f.p=p`2/sqrt(1+(p`2/p`1)^2)) & (for q being Point of TOP-REAL 2 st q in the carrier of (TOP-REAL 2)|K1 holds q`1<>0 ) holds f is continuous; theorem :: JGRAPH_3:13 for K1 being non empty Subset of TOP-REAL 2, f being Function of (TOP-REAL 2)|K1,R^1 st (for p being Point of TOP-REAL 2 st p in the carrier of (TOP-REAL 2)|K1 holds f.p=p`2/sqrt(1+(p`1/p`2)^2)) & (for q being Point of TOP-REAL 2 st q in the carrier of (TOP-REAL 2)|K1 holds q`2<>0 ) holds f is continuous; theorem :: JGRAPH_3:14 for K1 being non empty Subset of TOP-REAL 2, f being Function of (TOP-REAL 2)|K1,R^1 st (for p being Point of TOP-REAL 2 st p in the carrier of (TOP-REAL 2)|K1 holds f.p=p`1/sqrt(1+(p`1/p`2)^2)) & (for q being Point of TOP-REAL 2 st q in the carrier of (TOP-REAL 2)|K1 holds q`2<>0 ) holds f is continuous; theorem :: JGRAPH_3:15 for K0,B0 being Subset of TOP-REAL 2,f being Function of ( TOP-REAL 2)|K0,(TOP-REAL 2)|B0 st f=Sq_Circ|K0 & B0=NonZero TOP-REAL 2 & K0={p: (p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1) & p<>0.TOP-REAL 2} holds f is continuous; theorem :: JGRAPH_3:16 for K0,B0 being Subset of TOP-REAL 2,f being Function of ( TOP-REAL 2)|K0,(TOP-REAL 2)|B0 st f=Sq_Circ|K0 & B0=NonZero TOP-REAL 2 & K0={p: (p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p`2) & p<>0.TOP-REAL 2} holds f is continuous; scheme :: JGRAPH_3:sch 1 TopIncl { P[set] } : { p: P[p] & p<>0.TOP-REAL 2 } c= NonZero TOP-REAL 2; scheme :: JGRAPH_3:sch 2 TopInter { P[set] } : { p: P[p] & p<>0.TOP-REAL 2 } = { p7 where p7 is Point of TOP-REAL 2 : P[p7]} /\ (NonZero TOP-REAL 2); theorem :: JGRAPH_3:17 for B0 being Subset of TOP-REAL 2,K0 being Subset of (TOP-REAL 2 )|B0,f being Function of ((TOP-REAL 2)|B0)|K0,((TOP-REAL 2)|B0) st f=Sq_Circ|K0 & B0=NonZero TOP-REAL 2 & K0={p:(p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1) & p<>0.TOP-REAL 2} holds f is continuous & K0 is closed; theorem :: JGRAPH_3:18 for B0 being Subset of TOP-REAL 2,K0 being Subset of (TOP-REAL 2 )|B0,f being Function of ((TOP-REAL 2)|B0)|K0,((TOP-REAL 2)|B0) st f=Sq_Circ|K0 & B0=NonZero TOP-REAL 2 & K0={p:(p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p`2) & p<>0.TOP-REAL 2} holds f is continuous & K0 is closed; theorem :: JGRAPH_3:19 for D being non empty Subset of TOP-REAL 2 st D`={0.TOP-REAL 2} holds ex h being Function of (TOP-REAL 2)|D,(TOP-REAL 2)|D st h=Sq_Circ|D & h is continuous; theorem :: JGRAPH_3:20 for D being non empty Subset of TOP-REAL 2 st D=NonZero TOP-REAL 2 holds D`= {0.TOP-REAL 2}; theorem :: JGRAPH_3:21 ex h being Function of TOP-REAL 2, TOP-REAL 2 st h=Sq_Circ & h is continuous; theorem :: JGRAPH_3:22 Sq_Circ is one-to-one; registration cluster Sq_Circ -> one-to-one; end; theorem :: JGRAPH_3:23 for Kb,Cb being Subset of TOP-REAL 2 st Kb={q: -1=q`1 & -1<=q`2 & q`2<=1 or q`1=1 & -1<=q`2 & q`2<=1 or -1=q`2 & -1<=q`1 & q`1<=1 or 1=q`2 & -1 <=q`1 & q`1<=1}& Cb={p2 where p2 is Point of TOP-REAL 2: |.p2.|=1} holds Sq_Circ.:Kb=Cb; theorem :: JGRAPH_3:24 for P,Kb being Subset of TOP-REAL 2,f being Function of ( TOP-REAL 2)|Kb,(TOP-REAL 2)|P st Kb={q: -1=q`1 & -1<=q`2 & q`2<=1 or q`1=1 & -1 <=q`2 & q`2<=1 or -1=q`2 & -1<=q`1 & q`1<=1 or 1=q`2 & -1<=q`1 & q`1<=1} & f is being_homeomorphism holds P is being_simple_closed_curve; theorem :: JGRAPH_3:25 for Kb being Subset of TOP-REAL 2 st Kb={q: -1=q`1 & -1<=q`2 & q `2<=1 or q`1=1 & -1<=q`2 & q`2<=1 or -1=q`2 & -1<=q`1 & q`1<=1 or 1=q`2 & -1<=q `1 & q`1<=1} holds Kb is being_simple_closed_curve & Kb is compact; theorem :: JGRAPH_3:26 for Cb being Subset of TOP-REAL 2 st Cb={p where p is Point of TOP-REAL 2: |.p.|=1} holds Cb is being_simple_closed_curve; begin :: The Fashoda Meet Theorem for the Circle theorem :: JGRAPH_3:27 for K0,C0 being Subset of TOP-REAL 2 st K0={p: -1<=p`1 & p`1<=1 & -1<= p`2 & p`2<=1} & C0={p1 where p1 is Point of TOP-REAL 2: |.p1.|<=1} holds Sq_Circ"(C0) c= K0; theorem :: JGRAPH_3:28 for p holds (p=0.TOP-REAL 2 implies Sq_Circ".p=0.TOP-REAL 2) & ( (p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1) & p<>0.TOP-REAL 2 implies Sq_Circ".p=|[p`1*sqrt(1+(p`2/p`1)^2),p`2*sqrt(1+(p`2/p`1)^2)]|)& (not(p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1) implies Sq_Circ".p=|[p`1*sqrt(1+(p`1/p`2) ^2),p`2*sqrt(1+(p`1/p`2)^2)]|); theorem :: JGRAPH_3:29 Sq_Circ" is Function of TOP-REAL 2,TOP-REAL 2; theorem :: JGRAPH_3:30 for p being Point of TOP-REAL 2 st p<>0.TOP-REAL 2 holds ((p`1<= p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p`2) implies (Sq_Circ").p=|[p`1*sqrt(1+(p`1 /p`2)^2),p`2*sqrt(1+(p`1/p`2)^2)]|) & (not(p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p `1<=-p`2) implies (Sq_Circ").p=|[p`1*sqrt(1+(p`2/p`1)^2),p`2*sqrt(1+(p`2/p`1)^2 )]|); theorem :: JGRAPH_3:31 for X being non empty TopSpace, f1,f2 being Function of X,R^1 st f1 is continuous & f2 is continuous & (for q being Point of X holds f2.q<>0) holds ex g being Function of X,R^1 st (for p being Point of X,r1,r2 being Real st f1.p=r1 & f2.p=r2 holds g.p=r1*sqrt(1+(r1/r2)^2)) & g is continuous; theorem :: JGRAPH_3:32 for X being non empty TopSpace, f1,f2 being Function of X,R^1 st f1 is continuous & f2 is continuous & (for q being Point of X holds f2.q<>0) ex g being Function of X,R^1 st (for p being Point of X,r1,r2 being Real st f1.p=r1 & f2.p=r2 holds g.p=r2*sqrt(1+(r1/r2)^2)) & g is continuous; theorem :: JGRAPH_3:33 for K1 being non empty Subset of TOP-REAL 2, f being Function of (TOP-REAL 2)|K1,R^1 st (for p being Point of TOP-REAL 2 st p in the carrier of (TOP-REAL 2)|K1 holds f.p=p`1*sqrt(1+(p`2/p`1)^2)) & (for q being Point of TOP-REAL 2 st q in the carrier of (TOP-REAL 2)|K1 holds q`1<>0 ) holds f is continuous; theorem :: JGRAPH_3:34 for K1 being non empty Subset of TOP-REAL 2, f being Function of (TOP-REAL 2)|K1,R^1 st (for p being Point of TOP-REAL 2 st p in the carrier of (TOP-REAL 2)|K1 holds f.p=p`2*sqrt(1+(p`2/p`1)^2)) & (for q being Point of TOP-REAL 2 st q in the carrier of (TOP-REAL 2)|K1 holds q`1<>0) holds f is continuous; theorem :: JGRAPH_3:35 for K1 being non empty Subset of TOP-REAL 2, f being Function of (TOP-REAL 2)|K1,R^1 st (for p being Point of TOP-REAL 2 st p in the carrier of (TOP-REAL 2)|K1 holds f.p=p`2*sqrt(1+(p`1/p`2)^2)) & (for q being Point of TOP-REAL 2 st q in the carrier of (TOP-REAL 2)|K1 holds q`2<>0 ) holds f is continuous; theorem :: JGRAPH_3:36 for K1 being non empty Subset of TOP-REAL 2, f being Function of (TOP-REAL 2)|K1,R^1 st (for p being Point of TOP-REAL 2 st p in the carrier of (TOP-REAL 2)|K1 holds f.p=p`1*sqrt(1+(p`1/p`2)^2)) & (for q being Point of TOP-REAL 2 st q in the carrier of (TOP-REAL 2)|K1 holds q`2<>0 ) holds f is continuous; theorem :: JGRAPH_3:37 for K0,B0 being Subset of TOP-REAL 2,f being Function of ( TOP-REAL 2)|K0,(TOP-REAL 2)|B0 st f=(Sq_Circ")|K0 & B0=NonZero TOP-REAL 2 & K0= {p:(p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1) & p<>0.TOP-REAL 2} holds f is continuous; theorem :: JGRAPH_3:38 for K0,B0 being Subset of TOP-REAL 2,f being Function of ( TOP-REAL 2)|K0,(TOP-REAL 2)|B0 st f=(Sq_Circ")|K0 & B0=NonZero TOP-REAL 2 & K0= {p:(p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p`2) & p<>0.TOP-REAL 2} holds f is continuous; theorem :: JGRAPH_3:39 for B0 being Subset of TOP-REAL 2,K0 being Subset of (TOP-REAL 2 )|B0,f being Function of ((TOP-REAL 2)|B0)|K0,((TOP-REAL 2)|B0) st f=(Sq_Circ") |K0 & B0=NonZero TOP-REAL 2 & K0={p:(p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p `1) & p<>0.TOP-REAL 2} holds f is continuous & K0 is closed; theorem :: JGRAPH_3:40 for B0 being Subset of TOP-REAL 2,K0 being Subset of (TOP-REAL 2 )|B0,f being Function of ((TOP-REAL 2)|B0)|K0,((TOP-REAL 2)|B0) st f=(Sq_Circ") |K0 & B0=NonZero TOP-REAL 2 & K0={p:(p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p `2) & p<>0.TOP-REAL 2} holds f is continuous & K0 is closed; theorem :: JGRAPH_3:41 for D being non empty Subset of TOP-REAL 2 st D`={0.TOP-REAL 2} holds ex h being Function of (TOP-REAL 2)|D,(TOP-REAL 2)|D st h=(Sq_Circ")|D & h is continuous; theorem :: JGRAPH_3:42 ex h being Function of TOP-REAL 2,TOP-REAL 2 st h=Sq_Circ" & h is continuous; theorem :: JGRAPH_3:43 Sq_Circ is Function of TOP-REAL 2,TOP-REAL 2 & rng Sq_Circ = the carrier of TOP-REAL 2 & for f being Function of TOP-REAL 2,TOP-REAL 2 st f= Sq_Circ holds f is being_homeomorphism; theorem :: JGRAPH_3:44 for f,g being Function of I[01],TOP-REAL 2, C0,KXP,KXN,KYP,KYN being Subset of TOP-REAL 2, O,I being Point of I[01] st O=0 & I=1 & f is continuous one-to-one & g is continuous one-to-one & C0={p: |.p.|<=1}& KXP={q1 where q1 is Point of TOP-REAL 2: |.q1.|=1 & q1`2<=q1`1 & q1`2>=-q1`1} & KXN={q2 where q2 is Point of TOP-REAL 2: |.q2.|=1 & q2`2>=q2`1 & q2`2<=-q2`1} & KYP={q3 where q3 is Point of TOP-REAL 2: |.q3.|=1 & q3`2>=q3`1 & q3`2>=-q3`1} & KYN={q4 where q4 is Point of TOP-REAL 2: |.q4.|=1 & q4`2<=q4`1 & q4`2<=-q4`1} & f.O in KXN & f.I in KXP & g.O in KYN & g.I in KYP & rng f c= C0 & rng g c= C0 holds rng f meets rng g;