Volume 13, 2001

University of Bialystok

Copyright (c) 2001 Association of Mizar Users

### The abstract of the Mizar article:

### On the Simple Closed Curve Property of the Circle and the Fashoda Meet Theorem for It

**by****Yatsuka Nakamura**- Received August 20, 2001
- MML identifier: JGRAPH_3

- [ Mizar article, MML identifier index ]

environ vocabulary ARYTM, SQUARE_1, EUCLID, PCOMPS_1, RELAT_1, FUNCT_5, PRE_TOPC, MCART_1, ARYTM_1, ARYTM_3, RCOMP_1, COMPLEX1, FUNCT_1, BOOLE, SUBSET_1, COMPTS_1, ORDINAL2, TOPMETR, JORDAN2C, FUNCT_4, PARTFUN1, METRIC_1, TOPS_2, TOPREAL2, TOPREAL1, BORSUK_1, JGRAPH_3, SEQ_1; notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, EUCLID, RELAT_1, TOPS_2, FUNCT_1, STRUCT_0, PARTFUN1, TOPREAL1, TOPMETR, PCOMPS_1, COMPTS_1, METRIC_1, RCOMP_1, SQUARE_1, FUNCT_2, PSCOMP_1, PRE_TOPC, JGRAPH_1, JORDAN2C, FUNCT_4, WELLFND1, TOPREAL2, TOPGRP_1; constructors REAL_1, GOBOARD5, TOPS_2, RCOMP_1, PSCOMP_1, JORDAN2C, COMPTS_1, TOPREAL2, TOPGRP_1, CONNSP_1, TOPMETR, WELLFND1, TOPRNS_1; clusters XREAL_0, STRUCT_0, RELSET_1, FUNCT_1, EUCLID, PRE_TOPC, SQUARE_1, BORSUK_1, TOPREAL2, TOPREAL6, BORSUK_2, BORSUK_3, MEMBERED; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; begin ::Preliminaries reserve x,y,z,u,a for real number; theorem :: JGRAPH_3:1 x^2=y^2 implies x=y or x=-y; theorem :: JGRAPH_3:2 x^2=1 implies x=1 or x=-1; theorem :: JGRAPH_3:3 0<=x & x<=1 implies x^2<=x; theorem :: JGRAPH_3:4 a>=0 & (x-a)*(x+a)<=0 implies -a<=x & x<=a; theorem :: JGRAPH_3:5 x^2-1<=0 implies -1<=x & x<=1; theorem :: JGRAPH_3:6 x < y & x < z iff x < min(y,z); theorem :: JGRAPH_3:7 0<x implies x/3<x & x/4<x; theorem :: JGRAPH_3:8 (x>=1 implies sqrt x>=1) & (x>1 implies sqrt x>1); theorem :: JGRAPH_3:9 x<=y & z<=u implies ].y,z.[ c= ].x,u.[; theorem :: JGRAPH_3:10 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:11 for f being Function,B,C being set holds (f|B).:C = f.:(C /\ B); theorem :: JGRAPH_3:12 for X being TopStruct,Y being non empty TopStruct, f being map of X,Y, P being Subset of X holds f|P is map of X|P,Y; theorem :: JGRAPH_3:13 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 map of X,Y st D`={p0} & E`={f.p0} & X is_T2 & Y is_T2 & (for p being Point of X|D holds f.p<>f.p0)& (ex h being map of X|D,Y|E st h=f|D & h is continuous) & (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.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.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.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:14 for p being Point of TOP-REAL 2 st p<>0.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:15 for X being non empty TopSpace, f1 being map of X,R^1 st f1 is continuous & (for q being Point of X ex r being real number st f1.q=r & r>=0) holds ex g being map of X,R^1 st (for p being Point of X,r1 being real number st f1.p=r1 holds g.p=sqrt(r1)) & g is continuous; theorem :: JGRAPH_3:16 for X being non empty TopSpace, f1,f2 being map 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 map of X,R^1 st (for p being Point of X,r1,r2 being real number st f1.p=r1 & f2.p=r2 holds g.p=(r1/r2)^2) & g is continuous; theorem :: JGRAPH_3:17 for X being non empty TopSpace, f1,f2 being map 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 map of X,R^1 st (for p being Point of X,r1,r2 being real number st f1.p=r1 & f2.p=r2 holds g.p=1+(r1/r2)^2) & g is continuous; theorem :: JGRAPH_3:18 for X being non empty TopSpace, f1,f2 being map 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 map of X,R^1 st (for p being Point of X,r1,r2 being real number st f1.p=r1 & f2.p=r2 holds g.p=sqrt(1+(r1/r2)^2)) & g is continuous; theorem :: JGRAPH_3:19 for X being non empty TopSpace, f1,f2 being map 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 map of X,R^1 st (for p being Point of X,r1,r2 being real number st f1.p=r1 & f2.p=r2 holds g.p=r1/sqrt(1+(r1/r2)^2)) & g is continuous; theorem :: JGRAPH_3:20 for X being non empty TopSpace, f1,f2 being map 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 map of X,R^1 st (for p being Point of X,r1,r2 being real number st f1.p=r1 & f2.p=r2 holds g.p=r2/sqrt(1+(r1/r2)^2)) & g is continuous; theorem :: JGRAPH_3:21 for K1 being non empty Subset of TOP-REAL 2, f being map 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:22 for K1 being non empty Subset of TOP-REAL 2, f being map 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:23 for K1 being non empty Subset of TOP-REAL 2, f being map 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:24 for K1 being non empty Subset of TOP-REAL 2, f being map 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:25 for K0,B0 being Subset of TOP-REAL 2,f being map of (TOP-REAL 2)|K0,(TOP-REAL 2)|B0 st f=Sq_Circ|K0 & B0=(the carrier of TOP-REAL 2) \ {0.REAL 2} & K0={p:(p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1) & p<>0.REAL 2} holds f is continuous; theorem :: JGRAPH_3:26 for K0,B0 being Subset of TOP-REAL 2,f being map of (TOP-REAL 2)|K0,(TOP-REAL 2)|B0 st f=Sq_Circ|K0 & B0=(the carrier of TOP-REAL 2) \ {0.REAL 2} & K0={p:(p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p`2) & p<>0.REAL 2} holds f is continuous; scheme TopIncl { P[set] } : { p: P[p] & p<>0.REAL 2 } c= (the carrier of TOP-REAL 2) \ {0.REAL 2}; scheme TopInter { P[set] } : { p: P[p] & p<>0.REAL 2 } = { p7 where p7 is Point of TOP-REAL 2 : P[p7]} /\ ((the carrier of TOP-REAL 2) \ {0.REAL 2}); theorem :: JGRAPH_3:27 for B0 being Subset of TOP-REAL 2,K0 being Subset of (TOP-REAL 2)|B0,f being map of ((TOP-REAL 2)|B0)|K0,((TOP-REAL 2)|B0) st f=Sq_Circ|K0 & B0=(the carrier of TOP-REAL 2) \ {0.REAL 2} & K0={p:(p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1) & p<>0.REAL 2} holds f is continuous & K0 is closed; theorem :: JGRAPH_3:28 for B0 being Subset of TOP-REAL 2,K0 being Subset of (TOP-REAL 2)|B0,f being map of ((TOP-REAL 2)|B0)|K0,((TOP-REAL 2)|B0) st f=Sq_Circ|K0 & B0=(the carrier of TOP-REAL 2) \ {0.REAL 2} & K0={p:(p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p`2) & p<>0.REAL 2} holds f is continuous & K0 is closed; theorem :: JGRAPH_3:29 for D being non empty Subset of TOP-REAL 2 st D`={0.REAL 2} holds ex h being map of (TOP-REAL 2)|D,(TOP-REAL 2)|D st h=Sq_Circ|D & h is continuous; theorem :: JGRAPH_3:30 for D being non empty Subset of TOP-REAL 2 st D=(the carrier of TOP-REAL 2) \ {0.REAL 2} holds D`= {0.REAL 2}; theorem :: JGRAPH_3:31 ex h being map of TOP-REAL 2, TOP-REAL 2 st h=Sq_Circ & h is continuous; theorem :: JGRAPH_3:32 Sq_Circ is one-to-one; definition cluster Sq_Circ -> one-to-one; end; theorem :: JGRAPH_3:33 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:34 for P,Kb being Subset of TOP-REAL 2,f being map 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_homeomorphism holds P is_simple_closed_curve; theorem :: JGRAPH_3:35 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_simple_closed_curve & Kb is compact; theorem :: JGRAPH_3:36 for Cb being Subset of TOP-REAL 2 st Cb={p where p is Point of TOP-REAL 2: |.p.|=1} holds Cb is_simple_closed_curve; begin :: The Fashoda Meet Theorem for the Circle theorem :: JGRAPH_3:37 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:38 for p holds (p=0.REAL 2 implies Sq_Circ".p=0.REAL 2) & ( (p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1) & p<>0.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)& p<>0.REAL 2 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:39 Sq_Circ" is map of TOP-REAL 2,TOP-REAL 2; theorem :: JGRAPH_3:40 for p being Point of TOP-REAL 2 st p<>0.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:41 for X being non empty TopSpace, f1,f2 being map 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 map of X,R^1 st (for p being Point of X,r1,r2 being real number st f1.p=r1 & f2.p=r2 holds g.p=r1*sqrt(1+(r1/r2)^2)) & g is continuous; theorem :: JGRAPH_3:42 for X being non empty TopSpace, f1,f2 being map of X,R^1 st f1 is continuous & f2 is continuous & (for q being Point of X holds f2.q<>0) ex g being map of X,R^1 st (for p being Point of X,r1,r2 being real number st f1.p=r1 & f2.p=r2 holds g.p=r2*sqrt(1+(r1/r2)^2)) & g is continuous; theorem :: JGRAPH_3:43 for K1 being non empty Subset of TOP-REAL 2, f being map 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:44 for K1 being non empty Subset of TOP-REAL 2, f being map 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:45 for K1 being non empty Subset of TOP-REAL 2, f being map 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:46 for K1 being non empty Subset of TOP-REAL 2, f being map 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:47 for K0,B0 being Subset of TOP-REAL 2,f being map of (TOP-REAL 2)|K0,(TOP-REAL 2)|B0 st f=(Sq_Circ")|K0 & B0=(the carrier of TOP-REAL 2) \ {0.REAL 2} & K0={p:(p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1) & p<>0.REAL 2} holds f is continuous; theorem :: JGRAPH_3:48 for K0,B0 being Subset of TOP-REAL 2,f being map of (TOP-REAL 2)|K0,(TOP-REAL 2)|B0 st f=(Sq_Circ")|K0 & B0=(the carrier of TOP-REAL 2) \ {0.REAL 2} & K0={p:(p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p`2) & p<>0.REAL 2} holds f is continuous; theorem :: JGRAPH_3:49 for B0 being Subset of TOP-REAL 2,K0 being Subset of (TOP-REAL 2)|B0,f being map of ((TOP-REAL 2)|B0)|K0,((TOP-REAL 2)|B0) st f=(Sq_Circ")|K0 & B0=(the carrier of TOP-REAL 2) \ {0.REAL 2} & K0={p:(p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1) & p<>0.REAL 2} holds f is continuous & K0 is closed; theorem :: JGRAPH_3:50 for B0 being Subset of TOP-REAL 2,K0 being Subset of (TOP-REAL 2)|B0,f being map of ((TOP-REAL 2)|B0)|K0,((TOP-REAL 2)|B0) st f=(Sq_Circ")|K0 & B0=(the carrier of TOP-REAL 2) \ {0.REAL 2} & K0={p:(p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p`2) & p<>0.REAL 2} holds f is continuous & K0 is closed; theorem :: JGRAPH_3:51 for D being non empty Subset of TOP-REAL 2 st D`={0.REAL 2} holds ex h being map of (TOP-REAL 2)|D,(TOP-REAL 2)|D st h=(Sq_Circ")|D & h is continuous; theorem :: JGRAPH_3:52 ex h being map of TOP-REAL 2,TOP-REAL 2 st h=Sq_Circ" & h is continuous; canceled; theorem :: JGRAPH_3:54 Sq_Circ is map of TOP-REAL 2,TOP-REAL 2 & rng Sq_Circ = the carrier of TOP-REAL 2 & for f being map of TOP-REAL 2,TOP-REAL 2 st f=Sq_Circ holds f is_homeomorphism; theorem :: JGRAPH_3:55 for f,g being map 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;

Back to top